Version 0.6.0: Parametric systems and μ-calculus Properties

More options for verification.

Once again, I have released a new version of machine-check, 0.6.0.

For this version, I was focused on extending properties to μ-calculus and introducing parametric systems. The μ-calculus initially seemed quite simple to implement, but the slowdown compared to the previous Computation Tree Logic was untenable.

Things quickly turned to hellish when I tried to implement incremental model-checking that would make things faster. After a lot of trial and error, I am pleased to say the new implementation performs roughly on par with the previous CTL checking and gives a lot more space for improvement, which allowed me to implement parametric verification relatively quickly.

The parametric verification brought some breaking changes, but I prepared a book page for straightforward migration. The book now also details parametric systems and μ-calculus as new chapters. While the current examples are fairly simple, I feel a lot of potential has been unlocked by this.

Important changes in version 0.6.0

• Parametric systems are now supported, with some breaking changes to system specifications.
• μ-calculus verification is now supported through the new lfp! and gfp! operators.
• The machine_check::Input and machine_check::State marker traits are now blanket-implemented, not polluting systems anymore. Good riddance.

I am happy to say that despite the complete change in the underlying model-checking engine, the underlying behaviour of model-checking CTL has not changed, and state spaces are refined exactly as they were in 0.5.0.

What's next

I have decided to raise the Minimum Supported Rust Version to 1.88.0 in the next release of machine-check. This will allow using the 2024 Rust edition and, importantly, the if-let chains which nicely simplify some constructs. The current support for Rust 1.83.0 also blocks machine-check from using some crates that would be useful, for example crates with icons that could replace the Unicode dingbats used for the GUI property results. I noticed that they are especially badly visible on Windows 11, and put a dark grey background behind them for now to at temporarily improve this (apologies for the ugliness).

I have worked on the processing of the properties using the system translations, but it is tricky to do this without problems and potential regressions, so I have postponed this until the next version. It should immediately help with long system build times and also allow easy implementation of other abstraction and refinement domains. I also want to look more at equality/hierarchy comparisons between two systems: the separate notions of systems and properties have been converging within machine-check for a time now.

The next release will breaking, raising the MSRV and potentially changing systems and/or properties, although I assume not significantly.

Until next time!