Issy should not allow symbolic games that use location domains with more than current-step program variables.
For example, it should reject
state int x
game Safety from l {
loc l 1 with [x' = 0] // <- this is bad
from l to l with true
}
and
input int i
state int x
game Safety from l {
loc l 1 with [i > 0] // <- this is bad
from l to l with true
}
Issy should not allow symbolic games that use location domains with more than current-step program variables.
For example, it should reject
and