verify: I: check: deadlock: ok
verify: I: check: unreachable: ok
verify: I: check: livelock: ok
verify: I: check: deterministic: fail
error: interface I is unobservably non-deterministic
model: I
start
return
tick
tick
<non-deterministic>
verify: demon1_cascading_invariant: check: deterministic: ok
verify: demon1_cascading_invariant: check: illegal: ok
verify: demon1_cascading_invariant: check: deadlock: fail
error: deadlock in model demon1_cascading_invariant
model: demon1_cascading_invariant
p.start
p.return
<deadlock>
verify: demon1_cascading_invariant: check: unreachable: skip
verify: demon1_cascading_invariant: check: livelock: ok
verify: demon1_cascading_invariant: check: compliance: skip
