Trustworthy Intelligent Systems

IscasMC for Quantum Markov Chains Download Page

In this page it is possible to download the command-line version of IscasMC. We provide it as a JAR file, so that it can be directly used without having to compile it. Note that for this version content not related to Quantum Markov chain model checking has been removed.

IscasMC requires at least Java 8 to run. Previous versions will not work. After having installed Java (see the Java download page for details), please find out how to start Java from the command-line. Usually, after having opened a terminal window, one can do so using

java

Please check the Java version which is actually started by this command by using

java -version

Brief usage instructions

IscasMC can then be started using java -jar iscasmc-for-qmc.jar. Doing so should result in a message like

Type "<iscasmc> help" for usage description

i.e., to get the usage description, type

java -jar iscasmc-for-qmc.jar help

The command used more frequently is “check”. It requires two command parameters, namely the model and the property files. These two files should be written in terms of the input language of the probabilistic model checker PRISM.

The model checking process can then be started using

java -jar iscasmc-for-qmc.jar check <model> <property> --ltl2ba-spot-ltl2tgba-cmd <spot-location>

In addition to the command and its parameters, optional program options may be specified. These options specify the way in which the given task, e.g., the model checking, is performed, specify the place an external tool is located, etc. Each of these options starts with “–”. For an overview of these options, please use the “help” command. Notice that options and also commands and parameters are subject to change, as the tool is still actively developed.

The default memory limit of the Java virtual machine running the tool might not suffice for all analyses to perform. To see how to increase the memory available to the virtual machine, please check the Java documentation, or other support pages like for instance this administration guide.

Note for the extension to Quantum Markov chains

IscasMC has been extended to support the analysis of Quantum Markov chains. When you check a Quantum Markov chain, please make sure to use the options

--input-type prism-qmc --plugin iscasmc-qmc-plugin.jar

that enables the analysis of this kind of models. This means that, to check the loop model given below, the full command to be used is

java -jar iscasmc-for-qmc.jar check qmc-loop.prism qmc-loop.props --input-type prism-qmc --plugin iscasmc-qmc-plugin.jar

Download IscasMC and Quantum Markov chain example models