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:
- The Maude system must be installed. It is available for download here.
- Unzip ismc.zip.
- Run Maude.
- For running the module "counting.maude", it must be loaded directly on Maude: "load counting.maude ."
- For running the model checker, in Maude's command line, type "load loads.maude ." Now the model checker is available.
- Unzip any of the example files.
- In Maude's command line, type "(load module-name.maude .)" for any of the example modules.
- 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.