Closed Rorck closed 8 months ago
It would be nice to support state invariants.
Something like:
timeout t1 state S1 { invariant timeout t1 + 1000 }
Basic invariants, i.e., boolean expressions without references to timeouts, are now supported in 7b4cf59.
Clock references are now supported in af316e2b031cabd8cad3d88c2e2cdd3e48ff7c61.
It would be nice to support state invariants.
Something like: