Assertion | States | Transitions | Result |
---|---|---|---|
timed EnvironmentalSensing is deadlock free (r1) [FAILURESDIVERGENCES] | 109 | 520 | false |
timed EnvironmentalSensing terminates (r2) | 113 | 524 | true |
timed Movement is refined by Spec2 (r3) [FAILURESDIVERGENCES] | 1 | 1 | true |