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)).
Hey,
On the latest version of Strix (21.0.0), I am getting a realisable verdict on the following .tlsf file:
It seems to me this should be umrealisable (the environment can always choose to make
!x && ytrue 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)).