Wrong verdict on simple example with Xs

[shaunazzopardi]

Hey,

On the latest version of Strix (21.0.0), I am getting a realisable verdict on the following .tlsf file:

INFO {
	TITLE:       ""
	DESCRIPTION: ""
	SEMANTICS:   Mealy
	TARGET:      Mealy
}
MAIN {
	INPUTS { 
		x;
		y;
		z;
	}
	OUTPUTS { 
	}
	ASSUMPTIONS {
		X(x || y);
		X(!x && y)
	}
	GUARANTEES { 
		z
	}
}

It seems to me this should be umrealisable (the environment can always choose to make !x && y true in the next state, satisfying both assumptions).

To identify the source of the error I tried small modifications, e.g., remove the Xs from the assumptions, join the two assumptions into one (X((x || y) && !x && y)) turning the Xs into Gs, or changing the guarantee to false. Strix gives the correct verdict in all these cases.

It seems the issue is with how X is dealt with internally. Note the issue also disappears if the X is propagated in the first assumption, i.e. to (X(x)) || (X(y)).