eventb-rossi/Event-B Animate
Model-check Event-B models using the ProB 2.0 model checker
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Activelast commit Jul 9, 2026
- License
- Apache 2.0
Pinned Snippet
uses: eventb-rossi/eventb-animate@e8919f24c8087c066abcbca31bea9cbc06ff74a9 # v6.0tags can be moved; commit SHAs can't. why a SHA?
Inputs
| name | description | required | default |
|---|---|---|---|
| model-path | Path to the Event-B model (.bum file, .zip archive, or directory) | yes | — |
| command | Subcommand to run: "check" (model-check, the default), "replay", "wd", "po", or "cbc" | no | check |
| size | Default size for ProB sets (check, wd, cbc, and po --disprove) | no | "" |
| states | Bound model-checking to at most N explored states; omit for exhaustive (check command) | no | "" |
| save | Save the counterexample trace to a JSON file when a violation is found (check and cbc commands) | no | "" |
| json-report | Write a machine-readable JSON report of the run to this path | no | "" |
| junit-report | Write a JUnit XML report to this path (one testcase per checked property) | no | "" |
| markdown-report | Write a human-readable Markdown report of the run to this path | no | "" |
| trace | Path to JSON trace file (replay command, required when command is "replay") | no | "" |
| args | Extra arguments appended to the assembled command | no | "" |
| version | Release version tag to use (e.g., "v5.1"). Defaults to latest release. | no | latest |
| java-version | Java version to use (must be 21 or later) | no | 21 |
Outputs
no outputs