LTL Model checking error
If you check OBS2 against TEST you get a counterexample that does not violate the property
// MUSEO
CONTROL = (open -> ticket->entry-> close -> exit -> CONTROL).
||Test = CONTROL.
assert OBS2 = [](close -> (!(exit) U open))
Trace to terminal set of states: open ticket entry close exit open ticket entry close Cycle in terminal set: exit open ticket entry close
The right output is
open ticket entry close exit