This page lists tools that can convert models to, between, and from JANI. Please contact if you would like to have your own conversion tool added to this page. If problems occur while using one of the mentioned tools, please contact the respective tool authors.
All models in the Quantitative Verification Benchmark Set need to be available in the JANI model format. The following conversions from other modelling formalisms are available in tools:
Conversion of input models given in the Galileo Language is supported by the DFTRES tool.
For example, the Galileo model file mcs.1-1-10-false.dft can be converted into a JANI file using DFTRES with the following command:
java -jar DFTRES.jar --export-jani mcs.1-1-10-false.jani -a -r 1 mcs.1-1-10-false.dft
The properties specified in the JANI file are determined by the options specified to DFTRES, namely -a for availability and -r T for reliability up to time T.
The Galileo conversion of DFTRES requires a working installation of DFTCalc and its dependencies.
GSPN given in GreatSPN project files can be converted into JANI using Storm-gspn, which is part of Storm.
For example, the GreatSPN file readers-writers.pnpro, the capacities file readers-writers.capacities, and the property file readers-writers.csl can be converted into a JANI file using Storm-gspn version 1.2.4 with the following command:
storm-gspn --gspnfile readers-writers.pnpro --capacitiesfile readers-writers.capacities --prop readers-writers.csl --constants K=35 --to-jani readers-writers-35.jani
Here, the capacities file specifies upper bounds for the number of tokens in each place to guarantee a finite Markov model. The property file contains properties using the syntax of PRISM properties. The option --constants specifies values for constants/templates occurring in the GreatSPN file. In addition, the following options can be used:
Conversion of input models given in the Modest language is supported by moconv, which is part of the Modest Toolset.
For example, the Modest model file beb.3.modest can be converted into a JANI file using moconv with the following command:
moconv.exe beb.3.modest -O beb.3-4.jani -E "K=4" --unroll-distrs
Several additional conversions can be performed by specifying options to moconv (such as replacing finite-support probability distributions by probabilistic branching via the --unroll-distrs option in the command above); run
moconv.exe -?
for an overview and explanation of all available options.
Conversion of input models given in the Probabilistic Planning Domain Definition Language (PPDDL) is supported by ppddl2jani, a script written by Marcel Steinmetz, which uses parts of the Fast Downward PPDDL parser.
For example, the PPDDL files of the elevator problem p01.pddl and domain.pddl can be converted into a JANI file using ppddl2jani with the following command:
ppddl2jani.py domain.pddl p01.pddl --jani elevators.jani
Conversion of input models given in the PRISM launguage is supported by Storm-conv, which is part of Storm.
For example, the PRISM model file resource-gathering.pm and the PRISM property file resource-gathering.prctl can be converted into a JANI file using Storm-conv version 1.2.4 with the following command:
storm-conv --prism resource-gathering.pm --prop resource-gathering.prctl --tojani resource-gathering.jani
In addition, the following options can be used:
There are tools which support the analysis of model types which are often represented in JANI but do not directly accept JANI as an input format. The following tools implement conversions from JANI to other input formats:
Conversion of JANI MDP models using a restricted JANI syntax into the Probabilistic Planning Domain Definition Language (PPDDL) is supported by jani2ppddl, a script written by Michaela Klauck.
For example, the JANI file of Rabin's mutual exclusion protocol rabin.3.jani can be converted into a PPDDL domain and a problem file using jani2ppddl with the following command, where the configuration file lists the arithmetic expressions used in the model (see the script's webpage for more information).
jani2ppddl.py rabin.3.jani -c config_rabin.py
JANI includes model types and advanced modelling features that might not be supported by some tools. The following tools implement conversions to less expressive model types or more conservative fragments of JANI: