Options
The following options are user-specifiable and will affect how the STAMINA algorithm runs. You will learn how to set these via the CLI options in the next page.
Reachability Threshold (κ)
The reachability threshold is passed into STAMINA via the kappa command line argument.
Definition: The threshold probability that a particular state must be at to be considered “reachable”. Since we are in a Continuous Time Markov Chain, transitions are represented by a “rate” rather than a flat probability, meaning that a rate of 0.0 is undefined for a state transition. However, the number of states that the “reduced” state space model can reach is determined by this threshold. In the reachability analysis method of the StaminaModelBuilder classes (STAMINA/STORM) or the InfCTMCModelGenerator() class (STAMINA/PRISM), a truncated state space is created, based on this reachability threshold.
STAMINA only includes states where the probability mass is clustered, starting breadth-first from the initial state. This means that states less likely to be chosen and included in the truncated model if:
- They are farther away from the initial state.
- There is a low transition rate to that state.
The probability threshold is the probabilistic state search termination value; i.e., the lower the reachability threshold, the more states are to be explored, and the longer the simulation could take. If the probability threshold is set too low, then very little state space truncation could occur, causing the system to run out of resources. Do not set the value of the reachability threshold to 0, as this will result in an infinite (and therefore uncomputable) state space.
Kappa (κ) reduction factor (rκ)
Definition: the kappa reduction factor is the reduction factor on the reachability threshold, kappa (see above). It defines how much the reachability threshold is reduced by: κmin = κ / rκ. As mentioned above, too low of a reachability threshold could cause overuse of system resources, meaning that the kappa reduction factor ought not to be excessively high.
The κ reduction factor is used to compute the lower bound probability Pmin, the lower bound of the probability that Φ, the state formula, being satisfied within the state space.
Misprediction Factor (m)
Definition: This is used in determining the termination of the exploration. If Π is the probability we are in a terminal state, then exploration is terminated when Π < w / m. Additionally, if the bound between Pmax and Pmin is greater than the window, the misprediction factor will be updated accordingly. This updating is done in StaminaModelBuilder::buildMatrices() (STAMINA/STORM) or InfCTMCModelGenerator.doReachabilityAnalysis() (STAMINA/PRISM).
Max Approximate Count
Definition: The maximum number of approximation iterations (the second-outermost while loop in the algorithm).
Max Refinement Count
Definition: The maximum number of refinement iterations used in computing the upper and lower bounds of the probabilities of reaching a certain state, Pmax and Pmin.
Probability Error Window (w)
Definition: The defined maximum difference between Pmax and Pmin. This is user specified, and affects the computation of the misprediction factor, m.
No Property Refining
Definition: Whether or not to use property based refinement.
Rank Transitions
Definition: a boolean representing whether or not rank transitions will be used.
CUDD Memory Limit
Definition: A string representing the memory limit available to STAMINA and the associated PRISM model we are building.
Problems could arise if there are more states needed to be built than memory available, so make sure that the reachability threshold and its reduction factor are reflective of your memory limits. STAMINA will terminate if a memory limit is hit, regardless of whether or not the probability window is found tight enough.
Export Model
Definition: a boolean representing whether or not we are going to export the model.
Export Filename
Definition: If we are going to export the model, to what filename will we export it?
Export Perimeter States
Definition: A boolean representing whether or not we are going to export the perimeter states to file.
Export Perimeter Filename
Definition: if we are going to export the perimeter states to a file, what shall be the filename?
Import Model
Definition: a boolean representing whether or not we are going to import a model file from PRISM. Acceptable file extensions are .pm, .prism, and others associated with the PRISM modelling system. However, this tool does not check the file extension, or its contents before trying to import, so importing an incompatible file will raise a PrismException.
Associated methods:
Import Filename
Definition: The name of the file whose models STAMINA is going to import.
Specific Property
Definition: Whether or not this is associated with a specific property.
Property Name
Definition: The name of the specific property associated with these options.
Export Transitions to File
Definition: The filename where the export transitions will be sent.