Event-B Animate v7.1

[7.1] - 2026-10-08

Dependencies

• Bump com.diffplug.spotless from 8.10.1 to 8.10.2
• Bump com.fasterxml.jackson.core:jackson-databind
• Bump com.diffplug.spotless from 8.10.2 to 8.10.3
• Bump gradle-wrapper from 9.7.1 to 9.8.0
• Bump com.github.spotbugs from 6.5.11 to 6.5.12
• Bump ch.qos.logback:logback-classic from 1.6.3 to 1.6.4
• Bump ch.qos.logback:logback-classic from 1.6.4 to 1.6.5
• Bump com.networknt:json-schema-validator

Build

• Ship only the Windows probcli in the Windows artifacts
• Drop TLA+, TLC, Alloy core and Velocity from the fat jar
• Depend on prob-java instead of de.prob2.kernel

CI/CD

• Install the per-platform jar, falling back to the universal one
• Stop building and uploading the fat jar in Build and Test

Miscellaneous

• Publish per-platform jars alongside the universal one
• Bundle only the JDK modules the app uses in the Windows runtime
• Derive JDK modules with jdeps and smoke test the Windows app image
• Publish only the per-platform jars

Event-B Animate v7.0

[7.0] - 2026-09-03

Features

• Reserve exit 1 for a violation, giving failures their own codes

Bug Fixes

• Realign the setup action's Java pin and gate releases on the check
• Derive the output name when only a model is given
• Derive the report format instead of pinning v3

Event-B Animate v6.6

[6.6] - 2026-09-02

Dependencies

• Bump com.github.spotbugs from 6.5.10 to 6.5.11
• Bump com.fasterxml.jackson.core:jackson-databind
• Bump com.networknt:json-schema-validator
• Bump gradle-wrapper from 9.7.0 to 9.7.1
• Bump com.diffplug.spotless from 8.9.0 to 8.10.0
• Bump com.diffplug.spotless from 8.10.0 to 8.10.1
• Bump actions/setup-java from 5 to 6
• Bump de.hhu.stups:de.prob2.kernel from 4.15.1 to 4.16.1

Event-B Animate v6.5

[6.5] - 2026-08-22

Features

• Emit structured state bindings in JSON counterexamples
• Emit structured counterexample bindings for disproved POs

Dependencies

• Bump com.github.spotbugs from 6.5.9 to 6.5.10
• Bump gradle-wrapper from 9.6.1 to 9.7.0
• Bump actions/cache from 4 to 6
• Bump ch.qos.logback:logback-classic from 1.6.1 to 1.6.3

Event-B Animate v6.4

[6.4] - 2026-08-08

Features

• Add setup action for CLI workflows
• Cache the release jar keyed on the resolved tag

Bug Fixes

• Verify the downloaded jar against the release manifest
• Fetch tags so the version check sees released tags

Dependencies

• Bump com.diffplug.spotless from 8.8.0 to 8.9.0
• Bump ch.qos.logback:logback-classic from 1.5.38 to 1.6.1

CI/CD

• Test the CI wrappers on ubuntu and macOS

Event-B Animate v6.3

[6.3] - 2026-07-26

Bug Fixes

• Require model-path in the GitHub Action
• Keep the jar download when a consumer sets before_script

Documentation

• Document the Markdown report input and variable

Testing

• Bridge Jackson versions in schema validation

Dependencies

• Bump com.gradleup.shadow from 9.5.1 to 9.6.1
• Bump com.networknt:json-schema-validator

CI/CD

• Publish only versioned jar
• Add complete artifact recovery
• Build only main, tags, and pull requests
• Apply least-privilege permissions, timeouts, and upload guards
• Serialize releases and pass the app version via the environment

Event-B Animate v6.2

[6.2] - 2026-07-21

Features

• Expose built-in check completion and statistics
• Classify LTL check completion
• Classify symbolic check completion
• Classify LTSmin check completion

Bug Fixes

• Bound and reap external checks
• Normalize search counters after preflight

Documentation

• Publish and validate the v3 contract

Build

• Verify shaded service providers

CI/CD

• Verify and publish release artifacts

Event-B Animate v6.1

[6.1] - 2026-07-19

Features

• Add LTSmin model-checking backends

Bug Fixes

• Disable hash symmetry for sequential LTSmin

Dependencies

• Bump com.gradleup.shadow from 9.4.3 to 9.5.1
• Bump com.fasterxml.jackson.core:jackson-databind
• Bump com.github.spotbugs from 6.5.8 to 6.5.9
• Bump ch.qos.logback:logback-classic from 1.5.37 to 1.5.38

Event-B Animate v6.0

[6.0] - 2026-07-07

Features

• Build self-contained Windows installer and portable ZIP
• Model-check by default and remove random animation
• Add -p/--pref to pass arbitrary ProB preferences
• Add --time-limit to bound model-checking in wall-clock time
• Add --stop-at-full-coverage to end the check once all events ran
• Add --assertions and --no-deadlock/--no-invariant check toggles
• Add --goal to search for a reachable state
• Add --search-strategy to choose the exploration order
• Add --progress to report model-checking liveness
• Add --ltl/--ltl-file to check temporal properties
• Add info --prefs to list ProB preferences
• Add wd subcommand checking well-definedness obligations
• Add --json machine-readable run reports
• Add --junit XML test reports
• Surface the JUnit/JSON reports in the CI templates
• Exit 2 for undischarged wd obligations, reserving exit 1 for disproofs
• Add po subcommand gating on the Rodin proof status
• Add cbc subcommand proving per-event invariant preservation
• Add cbc --deadlock search with an optional --where constraint
• Add cbc feasibility and redundant-invariant advisories
• Allow the wd, po and cbc commands in the CI templates
• Add po --disprove to hunt counterexamples for open obligations
• Add --symbolic invariant model checking (bmc, ic3, kinduction, tinduction)
• Add --markdown human-readable run reports
• Add replay --refine to adapt traces across Event-B refinements
• Add testgen operation-coverage test generation
• Add --eval to report formula values in counterexample states
• Add eval subcommand to evaluate formulas across the state space

Bug Fixes

• Log expected CLI errors without stack traces
• Reuse persistent ProB home to avoid Windows temp-dir leak
• Validate check flags up front and report them as usage errors
• Report mid-check ProB failures as incomplete, not violations
• Fail the po gate on broken (stale) Rodin proofs

Refactoring

• Drop the --check post-conversion validation flag
• Drop the -b/--bmodel prolog dump flag
• Derive the model-checking stop condition from the checker result
• Drop the dead state-bound ternary in the LTL checker call
• Thread command results through RunReport and a shared TraceWriter
• Let commands pass their own trace-save target to withSavedTrace
• Add shared Animate.incomplete and notAMachine report helpers
• Collapse the report write-guard in emitReports
• Derive the enabled-check names and properties from one table
• Centralize the Rodin schema names in RodinNames
• Derive the machine name one way
• Unify report writer formatting
• Tidy the command classes' boilerplate

Documentation

• Reframe as a model-checker and update CI wrappers
• Cover all check modes in the exit-code contract and help text
• Simplify README installation and drop LICENSE/Requirements sections
• Note cbc scales to small machines and is not wall-clock bounded

Dependencies

• Bump ch.qos.logback:logback-classic from 1.5.35 to 1.5.37
• Bump com.gradleup.shadow from 9.4.2 to 9.4.3
• Bump gradle-wrapper from 9.6.0 to 9.6.1
• Bump com.diffplug.spotless from 8.7.0 to 8.8.0

Event-B Animate v5.1

[5.1] - 2026-06-25

Features

• Support multi-project Rodin archives

Refactoring

• Rename installGitHooks task to setupGitHooks

Documentation

• Add installation instructions for package managers

Dependencies

• Bump com.github.spotbugs from 6.5.5 to 6.5.6
• Bump com.diffplug.spotless from 8.6.0 to 8.7.0
• Bump actions/checkout from 6 to 7
• Bump com.github.spotbugs from 6.5.6 to 6.5.8
• Bump ch.qos.logback:logback-classic from 1.5.34 to 1.5.35
• Bump gradle-wrapper from 9.5.1 to 9.6.0

CI/CD

• Notify packaging repos on release via repository_dispatch