Skip to content

Model-checker updates

Alessandro Tempia Calvino requested to merge alessandro_branch into master

Updates:

  • Documentation: state-space reduction, internal action loop, re-initialization, safety and liveness, and verification traces
  • Implementation of internal action loops
  • Improvements of leadsTo verification using bounds (it can solve false pragmas faster and on infinite graphs)
  • Added expected result in safety/liveness queries: T or F in front of the pragma
  • Verification traces for internal action loops
  • Added word size representation selection box in the model-checking window (32, 16, 8 bits)
  • Updated options for model-checking command in CLI
  • Added #states and #transitions in the name of verification traces
  • Minor fixes

Merge request reports