Closed grayswandyr closed 5 months ago
Have you tested it at nmacedo/org.alloytools.alloy@de0bd2f200e9b9b43e2b0b526942973a165bed4c ? It was buggy but should be fixed, I'm getting this:
some disj _S1,_S0,_S3,_S2 : univ + (univ)' {
// configuration
Int = none
seq/Int = none
String = none
this/S = _S0 + _S1 + _S2 + _S3
{
// state 0
univ = _S0 + _S1 + _S2 + _S3
(this/S <: r) = _S0 -> _S3 + _S1 -> _S1 + _S2 -> _S0 + _S3 -> _S0
};
{
// state 1
univ = _S0 + _S1 + _S2 + _S3
(this/S <: r) = _S0 -> _S2 + _S1 -> _S2 + _S2 -> _S2 + _S3 -> _S1
}
// enforce loop
after always {
({
// state 1
univ = _S0 + _S1 + _S2 + _S3
(this/S <: r) = _S0 -> _S2 + _S1 -> _S2 + _S2 -> _S2 + _S3 -> _S1
}) implies after ({
// state 1
univ = _S0 + _S1 + _S2 + _S3
(this/S <: r) = _S0 -> _S2 + _S1 -> _S2 + _S2 -> _S2 + _S3 -> _S1
})
}
}
My bad I was testing another commit. Looks good indeed, thanks.
"Export to predicate" (in the Visualizer) issues a wrong predicate. E.g. for the following model, after hitting "fork" then "next state" several times:
here is the returned predicate, where
r
isn't constrained at all: