MoChA 0.1.0

First stable release of MoChA, a teaching library for model checking.

• Labelled transition systems and finite, Büchi, and generalized Büchi automata.
• Reachability, invariant, persistence, and LTL model checking.
• LTL parsing, normal-form transformations, and automata construction.
• Algorithm traces exposing intermediate steps for teaching.
• Validated JSON import and export for string-valued transition systems.
• Optional Graphviz visualisation.

Requires Python 3.11 or later. Image rendering additionally requires the Graphviz executables.

MoChA 0.1.0rc1

First release candidate of MoChA, a teaching library for model checking.

• Labelled transition systems and finite, Büchi, and generalized Büchi automata.
• Reachability, invariant, persistence, and LTL model checking.
• LTL parsing, normal-form transformations, and automata construction.
• Algorithm traces exposing intermediate steps for teaching.
• Validated JSON import and export for string-valued transition systems.
• Optional Graphviz visualisation.

Requires Python 3.11 or later. Image rendering additionally requires the Graphviz executables.