Analysis, Witnesses, Traces
Witnesses
Witnesses1 are something that many model-checkers support. They are not proofs per se, but more akin to things like examples, counter-examples, or execution traces. MCMAS supports this too, at least for certain types of formulae. See the official user-manual2 for details about what kinds of logical expressions are supported. Default behaviour for mcmas involves output of .info files that are not necessarily very friendly for downstream use-cases but in py-mcmas, witness output is available as structured data.
Static Analysis
We've seen that witnesses require that specifications should actually be simulated, but py-mcmas also provides some limited facilities for static-analysis of specifications or partial specifications. The focus is on stuff that amounts to specification metadata simple extraction of symbols and other .