tlc4b
Model-check classical B specifications by translating them to TLA+
TLC4B model-checks classical B specifications by translating them to TLA+ and running the TLC model checker: invariant and assertion checking, deadlock detection, and counter-example traces mapped back to B.
homepage ↗ github: hhu-stups/tlc4b
Available in
| Overlay | Newest | Ebuilds | Last activity | |
|---|---|---|---|---|
| eventb-rossi GitHub ↗ | 1.2.3 | 1 | 31 h | details › |