CLTSA (Counting Fluents Labelled Transition System Analyser) is an extension of LTSA (Labelled Transition System Analyser) that incorporates counting fluents, a useful mechanism to capture properties related to counting events. The tool supports a superset of FSP, that allows one to define properties involving counting fluents, which the tool can also model check.

Check out the tool demo!

DynAlloy is a formal specification language that extends Alloy (a formal specification language based on first-orded logic and relational operations including transitive closure), by incorporating actions and programs, to better describe state change and properties of state changing situations. DynAlloy Analyzer is a tool for DynAlloy specification, built over Alloy Analyzer, that supports fully automated and efficient analysis of DynAlloy specifications, resorting to SAT solving.

Check out the tool demo!