The PRISM language can be used to specify DTMCs, CTMCs and MDPs. Conceptually, it is a guarded command language using reactive modules. Storm supports (almost) the full PRISM language and extends it (in a straightforward way) to Markov Automata.
JANI is a recently introduced modeling language for the landscape of probabilistic models. To allow easy parsing, JANI is based on JSON. In general, JANI models can encode a variety of model types. Storm’s support for JANI models covers DTMCs, CTMCs and MDPs.
The Petri Net Markup Language is an ISO-standardized XML format to specify Petri nets.
GreatSPN editor projects
The GreatSPN editor is a GUI capable of specifying and verifying GSPNs. Project files (XML) specifying a single GSPN can be parsed directly by Storm.
Dynamic Fault Trees are given in the so-called Galileo Format. The format is a simple textual format naming the root of the tree and then lists all nodes of the tree, together with the children of each node. A rich collection of examples is available.
The conditional probabilistic guarded command language, cpGCL for short, is an extension of Dijkstra’s guarded command language and pGCL1 to also accommodate probabilistic choice and conditional observations. Examples can be found in some of the folders in the JANI repository. For example, the famous coupon collector example encoded as a cpGCL program can be found here.
In the spirit of MRMC, Storm also supports input models specified in an explicit format. While the format closely resembles that of MRMC, it does not match exactly. Likewise, at the moment the model export of PRISM generates files that can be easily modified to be handled by Storm, but they still need to be adapted by hand.
The main ingredient of an explicit model is a tra-file containing the transitions. For DTMCs, a tra file might look like this
dtmc 0 1 0.3 0 4 0.7 1 0 0.5 1 1 0.5 ...
This specifies four transitions: from state 0 to 1 with probability 0.3, state 0 to 4 with probability 0.7 and so on. For CTMCs, only the model hint needs to be set to
ctmc. For MDPs, the tra file needs to have the following shape:
mdp 0 0 1 0.3 0 0 4 0.7 0 1 0 0.5 0 1 1 0.5 1 0 1 1.0 ...
This specifies the behaviors of two states. State 0 has two nondeterministic choices (called 0 and 1). With the first one, choice 0, state 0 can probabilistically go to state 1 with probability 0.3 and to state 4 with probability 0.7. The second choice (1), is associated with a uniform distribution over the states 0 and 1.
The labeling file format matches that of MRMC. That is, it looks similar to this:
#DECLARATION one two goal #END 0 one two 1 goal
This creates three distinct labels, called
goal. State 0 is labeled with both
two, while state 1 only carries the