eventb
Installation
SKILL.md
Developing Event-B models
An Event-B model is a discrete transition system. A CONTEXT holds fixed sets,
constants, and axioms; a MACHINE holds variables, invariants, and guarded events.
This skill checks reachable behaviour with ProB and gates well-definedness. It does
not author interactive Rodin proofs.
1. Check the required tools
Require rossi 0.2.0+ and eventb-animate 6.4+. Check them; never install or
upgrade them yourself. If either is absent or older, stop and ask the user to do it.
command -v rossi eventb-animate
rossi --version
eventb-animate --version