Running Storm on Parametric Models

Many model descriptions contain constants which may be specified only by an interval of possible values. We refer to these constants as parameters. Such parametric models are supported by the binary storm-pars. In what follows, we assume that all occurring parameters are graph-preserving, that is, they do not influence the topology of the underlying Markov model.

A comprehensive overview on the theoretical backgrounds is given in (Junges et al., 2019).

Computing the exact solution function

We can run storm to obtain closed-form solutions, i.e. a rational function that represents, e.g., the probability with which the given property is satisfied for certain parameter valuations.

Example 1 (Obtaining a closed-form solution of the parametric Knuth-Yao die)

The following model is an adaption of the Knuth-Yao die used in previous examples. The probability of flipping heads is now given by a parameter p.

Show parametric version of Knuth-Yao die
Hide parametric version of Knuth-Yao die

Download parametric version of Knuth-Yao die

// Knuth's model of a fair die using only fair coins
dtmc

const double p;

module die

	// local state
	s : [0..7] init 0;
	// value of the dice
	d : [0..6] init 0;
	
	[] s=0 -> p : (s'=1) + (1-p) : (s'=2);
	[] s=1 -> p : (s'=3) + (1-p) : (s'=4);
	[] s=2 -> p : (s'=5) + (1-p) : (s'=6);
	[] s=3 -> p : (s'=1) + (1-p) : (s'=7) & (d'=1);
	[] s=4 -> p : (s'=7) & (d'=2) + (1-p) : (s'=7) & (d'=3);
	[] s=5 -> p : (s'=7) & (d'=4) + (1-p) : (s'=7) & (d'=5);
	[] s=6 -> p : (s'=2) + (1-p) : (s'=7) & (d'=6);
	[] s=7 -> 1: (s'=7);
	
endmodule

rewards "coin_flips"
	[] s<7 : 1;
endrewards

label "one" = s=7&d=1;
label "two" = s=7&d=2;
label "three" = s=7&d=3;
label "four" = s=7&d=4;
label "five" = s=7&d=5;
label "six" = s=7&d=6;
label "done" = s=7;

We can consider the probability of a die roll reflecting an outcome of one.

$ storm-pars --prism parametric-die.pm --prop "P=? [F s=7&d=1]"

The result is an expression over the parameter p.

Show output
Hide output
Storm-pars 1.2.2-alpha

Command line arguments: --prism parametric_die.pm --prop P=? [F s=7&d=1] 
Current working directory: ~/storm/release-build

Time for model construction: 0.024s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	13
Transitions: 	20
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * ((s = 7) & (d = 1)) -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property P=? [F ((s = 7) & (d = 1))] ...
Result (initial states): 
((p)^2)/(p+1)
Time for model checking: 0.002s.

Parameter lifting for region refinement

For bounded properties we can use parameter lifting to partition a given region into safe, unsafe and ambiguous subregions.

Example 2 (Region refinement for a Bounded retransmission protocol)

This example is an adaption of the Bounded Retransmission Protocol from the PRISM website. Here, we have two channels whose reliabilities are represented by parameters pL and pK.

Show parametric version of the Bounded Retransmission Protocol
Hide parametric version of the Bounded Retransmission Protocol

Download parametric version of the Bounded Retransmission Protocol

// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001

dtmc

// number of chunks
const int N = 2;
// maximum number of retransmissions
const int MAX = 4;

// reliability of channels
const double pL;
const double pK;

// timeouts
const double TOMsg = 0.1;
const double TOAck = 0.1;

module sender

    s : [0..6];
    // 0 idle
    // 1 next_frame 
    // 2 wait_ack
    // 3 retransmit
    // 4 success
    // 5 error
    // 6 wait sync
    srep : [0..3];
    // 0 bottom
    // 1 not ok (nok)
    // 2 do not know (dk)
    // 3 ok (ok)
    nrtr : [0..MAX];
    i : [0..N];
    bs : bool;
    s_ab : bool;
    fs : bool;
    ls : bool;
    
    // idle
    [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
    // next_frame
    [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
    // wait_ack
    [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
    [TO_Msg] (s=2) -> (s'=3);
    [TO_Ack] (s=2) -> (s'=3);
    // retransmit
    [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
    [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
    [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
    // success
    [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
    [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
    // error
    [SyncWait] (s=5) -> (s'=6); 
    // wait sync
    [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); 
    
endmodule

module receiver

    r : [0..5];
    // 0 new_file
    // 1 fst_safe
    // 2 frame_received
    // 3 frame_reported
    // 4 idle
    // 5 resync
    rrep : [0..4];
    // 0 bottom
    // 1 fst
    // 2 inc
    // 3 ok
    // 4 nok
    fr : bool;
    lr : bool;
    br : bool;
    r_ab : bool;
    recv : bool;
    
    
    // new_file
    [SyncWait] (r=0) -> (r'=0);
    [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
    // fst_safe_frame
    [] (r=1) -> (r'=2) & (r_ab'=br);
    // frame_received
    [] (r=2) & (r_ab=br) & (fr=true) & (lr=false)  -> (r'=3) & (rrep'=1);
    [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
    [] (r=2) & (r_ab=br) & (fr=false) & (lr=true)  -> (r'=3) & (rrep'=3);
    [aA] (r=2) & !(r_ab=br) -> (r'=4);  
    // frame_reported
    [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
    // idle
    [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
    [SyncWait] (r=4) & (ls=true) -> (r'=5);
    [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
    // resync
    [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
    
endmodule

// prevents more than one file being sent
module tester 

    T : bool;
    
    [NewFile] (T=false) -> (T'=true);
    
endmodule

module  channelK

    k : [0..2];
    
    // idle
    [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
    // sending
    [aG] (k=1) -> (k'=0);
    // lost
    [TO_Msg] (k=2) -> (k'=0);
    
endmodule

module  channelL

    l : [0..2];
    
    // idle
    [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
    // sending
    [aB] (l=1) -> (l'=0);
    // lost
    [TO_Ack] (l=2) -> (l'=0);
    
endmodule

label "error" = s=5;

rewards
	[TO_Msg] true : TOMsg;
	[TO_Ack] true : TOAck;
endrewards


We want to split our region into those subregions that result in a chance for a successful transmission that is greater than 0.5 and those that do not.

$ storm-pars --prism brp.pm --prop "P>0.5 [F s=5]" --region "0.1 <= pL <= 0.9, 0.1 <=pK <=0.9" --refine 0.01 10

We use the --regions option to set the parameter region. The arguments we give to --refine are the coverage threshold and the depth limit. The coverage threshold decides how precisely we want to partition our region. The value 0.01 means that Storm will continue to refine until only 1% of the given region remains ambiguous while the rest has been determined to be either safe or unsafe. The depth limit is an optional second argument. If the level at which regions are split reaches this bound, the region is not refined any further, regardless of the coverage achieved so far.

This produces the following output:

Show output
Hide output
Storm-pars 1.6.4 (dev)

Date: Wed Feb 10 14:41:07 2021
Command line arguments: --prism brp.pm --prop 'P>0.5 [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <=pK <=0.9' --refine 0.01 10
Current working directory: ~/storm/build

Time for model input parsing: 0.003s.

Time for model construction: 0.015s.

--------------------------------------------------------------
Model type: 	DTMC (sparse)
States: 	135
Transitions: 	175
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 5 item(s)
   * init -> 1 item(s)
   * (s = 5) -> 4 item(s)
Choice Labels: 	none
--------------------------------------------------------------

Analyzing parameter region 1/10<=pK<=9/10,1/10<=pL<=9/10; using Parameter Lifting with iterative refinement until 99% is covered. Depth limit is 10.

Model checking property "1": P>1/2 [F (s = 5)] ...
Result (initial states):   Fraction of satisfied area: 51.6495%
Fraction of unsatisfied area: 47.3511%
            Unknown fraction: 0.999451%
     Total number of regions: 1822
                     Unknown: 468
                   ExistsSat: 392
              ExistsViolated: 356
                      AllSat: 321
                 AllViolated: 285

Region refinement Check result (visualization):
 	 x-axis: pK  	 y-axis: pL  	 S=safe, [ ]=unsafe, -=ambiguous
##################################################################################################################################
#SSSSSSSSSSSSSSSSSSSSSS--                                                                                                        #
#SSSSSSSSSSSSSSSSSSSSSSS-                                                                                                        #
#SSSSSSSSSSSSSSSSSSSSSSS--                                                                                                       #
#SSSSSSSSSSSSSSSSSSSSSSSS-                                                                                                       #
#SSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                      #
#SSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                     #
#SSSSSSSSSSSSSSSSSSSSSSSSSS-                                                                                                     #
#SSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                    #
#SSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                   #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSS-                                                                                                   #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                  #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                 #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                                #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                               #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-                                                                                               #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                              #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                             #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                            #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                           #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                          #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                         #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                        #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                       #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                                     #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                    #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                   #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                                  #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                                #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                               #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                             #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--                                                                            #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                          #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                        #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                      #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                    #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                  #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                                #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                              #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS----                                                           #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS----                                                        #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS---                                                      #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS----                                                   #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-----                                               #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS----                                            #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-----                                        #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-----                                    #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-----                                #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS------                           #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS------                      #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS------                 #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-------           #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS--------    #
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS-----#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
#SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
##################################################################################################################################

Time for model checking: 0.080s.

We can see that for two parameters, Storm even visulalizes the acquired data to give an initial understanding of the region partition.

Further options on this can be found with the following two queries:

$ storm-pars --help region
$ storm-pars --help parametric

Monotonicity analysis

Storm can also check if the parameters of a model are monotonic in regard to a certain property. For this, we use the --monotonicity-analysis option.

Example 3 (Checking the monotonicity of a parameter)

Again, we use the BRP model and check if any of the parameters are monotonic:

$ storm-pars --prism brp.pm --prop 'P=? [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <=pK <=0.9' --monotonicity-analysis --bisimulation

We use --bisimulation to apply further model simplification and significantly reduce the workload of the modelchecker. This results in the following output:

Show output
Hide output
Storm-pars 1.6.4 (dev)

Date: Wed Feb 10 14:39:02 2021
Command line arguments: --prism brp.pm --prop 'P=? [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <=pK <=0.9' --monotonicity-analysis --bisimulation
Current working directory: ~/storm/build

Time for model input parsing: 0.004s.

Time for model construction: 0.017s.

--------------------------------------------------------------
Model type: 	DTMC (sparse)
States: 	135
Transitions: 	175
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 5 item(s)
   * init -> 1 item(s)
   * (s = 5) -> 4 item(s)
Choice Labels: 	none
--------------------------------------------------------------

Time for model simplification: 0.000s.

--------------------------------------------------------------
Model type: 	DTMC (sparse)
States: 	43
Transitions: 	83
Reward Models:  none
State Labels: 	4 labels
   * (s = 5) -> 1 item(s)
   * deadlock -> 1 item(s)
   * target -> 1 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
--------------------------------------------------------------

Time for model preprocessing: 0.000s.

--------------------------------------------------------------
Model type: 	DTMC (sparse)
States: 	23
Transitions: 	43
Reward Models:  none
State Labels: 	2 labels
   * init -> 1 item(s)
   * (s = 5) -> 1 item(s)
Choice Labels: 	none
--------------------------------------------------------------
Number of done states: 23
No Assumptions
Monotonicity Result:
    #Incr: 0 #Decr: 2
pK MonDecr; pL MonDecr;


Total time for monotonicity checking: 0.000s.

If we want to take a look at the reachability order that is built during monotonicity checking, we can add the option --mon:dotOutput followed by an optional filename. Storm will then write a dot output of the order into the file which can then be processed using, e.g., Graphviz. In this case, it results in the following graph:

Reachability Order

For checking the monotonicity on samples, we use --mon:samples and provide it with the number of samples we want to be taken.

For more options on monotonictiy checking and their usages, we can use the --help option:

$ storm-pars --help mon

Computing extrema

Another feature Storm offers is the computations of extrema for a property within a given region.

Example 4 (Extremum computation for a bounded retransmission protocol)

We reuse our BRP model from earlier to compute the maximum probability for a successful transmission that is possible in the given region.

$ storm-pars --prism brp.pm --prop "P=? [F s=5]" --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9" --extremum max 0.01

We use --extremum and give it first a direction, in this case max to compute the maximum, and then a precision with which we want the maximum to be computed.

The result is the extremum as well as the specific valuation with which it was achieved.

Show output
Hide output
Storm-pars 1.6.4 (dev)

Date: Wed Feb 10 14:57:21 2021
Command line arguments: --prism brp.pm --prop 'P=? [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <=pK <=0.9' --extremum max 0.01
Current working directory: ~/storm/build

Time for model input parsing: 0.002s.

Time for model construction: 0.011s.

--------------------------------------------------------------
Model type: 	DTMC (sparse)
States: 	135
Transitions: 	175
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 5 item(s)
   * init -> 1 item(s)
   * (s = 5) -> 4 item(s)
Choice Labels: 	none
--------------------------------------------------------------
Computing extremal value for property 1: P=? [F (s = 5)] within region 1/10<=pK<=9/10,1/10<=pL<=9/10;...
Total number of plaCalls: 10
Result at initial state: 4451506352734141/4503599627370496 ( approx. 0.9884329694) at [pK=3/20, pL=3/20].
Time for model checking: 0.001s.

More relevant options can be found via

$ storm-pars --help region
$ storm-pars --help parametric

References