Model Checking TLR* Guarantee Formulas on Infinite Systems

Author: Óscar Martín.     Directors: Alberto Verdejo, Narciso Martí-Oliet

This is a companion site to the master thesis “Model Checking TLR* Guarantee Formulas on Infinite Systems.”

Links:

Instructions to run the model checker:

  1. The Maude system must be installed. It is available for download here.
  2. Unzip ismc.zip.
  3. Run Maude.
  4. For running the module "counting.maude", it must be loaded directly on Maude: "load counting.maude ."
  5. For running the model checker, in Maude's command line, type "load loads.maude ." Now the model checker is available.
  6. Unzip any of the example files.
  7. In Maude's command line, type "(load module-name.maude .)" for any of the example modules.
  8. In Maude's command line, type any model-checking command, as described in the master thesis. Some possible commands are written at the bottom of each file, commented out.