Properties files are specified in Continuous Stochastic Logic, a format allowing for both state formulas and path formulas. PRISM provides documentation which is both easy to understand, and extensive. It is recommended to reference that page here.
The types of properties STAMINA supports
Because the STAMINA algorithm estimates state reachability using cumulative path probability, it lends itself well to most types of CSL properties. In most of the testing examples we use, the properties tested were bounded path probability formulas, i.e., "what is the probability that state formula Φ holds for all states for a path from time 0 s to t s?" If we reference our example model file from the previous page, an example of a property like this would be as follows:
P=? [true U[0,1000] (SpeciesA > 10 & SpeciesB < 30) ]Click this link to download this file.
This property asks "what is probability that from time 0 to 1000 s that all states satisfy SpeciesA > 10 and SpeciesB < 30?"