PLASMA Lab can check unbounded properties from the A-BLTL logic. The algorithm that is used involved a reachability check of the underlying finite automata model. To do this PLASMA Lab calls the PRISM model-checker. We explain below how to configure PLASMA Lab in order to use this functionality:
- Step 1: install PRISM in your system.
- Step 2: download the script prism_reach.
- Step 3: in the script edit the line with the path to PRISM
- Step 4: launch PLASMA Lab with the option ‘-Dprism_reach=path’ where ‘path’ is the path to the script.
