Model Files
Model files are specifications for state-spaces based on real-life interactions between elements within a system. Model files may implicitly create state spaces, such as PRISM files and JANI files, or explicitly instantiate every state with values, such as in transition files. These model formats may be bounded or unbounded and may be deterministic or nondeterministic. They may be in one of the following model types:
- CTMC: Continuous-time Markov Chains
- DTMC: Discrete-time Markov Chains
- MDP: Markov Decision Processes
- MA: Markov Automaton
- And more...
STAMINA/STORM supports both CTMC and DTMC models, and STAMINA/PRISM only supports CTMCs. Both versions of STAMINA support bounded and unbounded models, as well as only deterministic models. Nondeterministic models will throw an error.
PRISM Models
PRISM models are a type of model format designed for the PRISM model checker . They allow for many types of models to be specified, and are composed of modules and variables. PRISM has documentation for the entire language specification, located here .
Because full documentation for the PRISM language exists on their website, STAMINA will only provide a brief overview of the syntax. All PRISM models must first contain a line which says what type of model they are. For STAMINA, that line is most likely to be ctmc. From there, globally-accessible variables and modules may be declared from the supported types. Modules are a way of encapsulating certain elements of a model. Generally a module contains a variable, and all of the reactions that can affect that variable. Reactions are in the format:
[action] guard -> prob1 : (var1'=var1+value1) + prob2 : (var1'=var1+value2)
The expression immediately following the probability is the update expression, specifying the new value for var1 using the var1' syntax.
As an example of a simple PRISM model, let us create a simple two-species network, with one unbounded variable, and one bounded variable:
// We define our variables and their reactions in a module
module SpeciesA_Def
SpeciesA : [0..100] init 0;
// We cannot decrement in species A if the value is 0
// This basically says "if SpeciesA is equal to 0, you may choose from two transitions:
// 1. Increment by 1 with transition rate 5, or,
// 2. Increment by 5 with transition rate 1.
[] (SpeciesA = 0) -> 5 : (SpeciesA'=SpeciesA+1) + 1 : (SpeciesA'=SpeciesA+5);
// However, if there is a nonzero amount of SpeciesA, we have one more transition: we can decrement by 1 with transition rate 2.
[] (SpeciesA > 0) -> 5 : (SpeciesA'=SpeciesA+1) + 1 : (SpeciesA'=SpeciesA+5) + 2 : (SpeciesA'=SpeciesA-1);
module SpeciesB_Def
SpeciesB : int init 0;
// This species has only one increment and one decrement
[] (SpeciesB = 0) -> 1 : (SpeciesB'=SpeciesB+1);
// Again, if there is a nonzero amount of this species, there can be a decrement.
[] (SpeciesB > 0) -> 1 : (SpeciesB'=SpeciesB+1) + 0.5 : (SpeciesB'=SpeciesB-1)
This model will create an infinite-state CTMC with deterministic choices for probabilistic transitions. This would be a prime example of a model that would be perfect for STAMINA.
JANI Model Files
JANI is a JSON-based model-specification language designed to be easily parsable and versatile. STAMINA/PRISM currently does not support JANI, but STAMINA/STORM is slated to use STORM's JANI-parser to add support in the next major release.
JANI provides a complete language specification which is easy to read and understand. We recommend you view that here .