TimQu
9 years ago
48 changed files with 4143 additions and 0 deletions
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus2_3_2.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus2_4_2.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus2_5_2.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus3_3_2.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus3_4_2.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/1_consensus3_5_2.prism-gs.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/2_zeroconf4.prism-gs.output
-
97examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/2_zeroconf6.prism-gs.output
-
97examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/2_zeroconf8.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/3_zeroconf-tb2_14.prism-gs.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/3_zeroconf-tb4_10.prism-gs.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/3_zeroconf-tb4_14.prism-gs.output
-
81examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/4_team2obj_3.prism-gs.output
-
81examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/4_team2obj_4.prism-gs.output
-
79examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/4_team2obj_5.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/5_team3obj_3.prism-gs.output
-
98examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/5_team3obj_4.prism-gs.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/5_team3obj_5.prism-gs.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/6_scheduler05.prism-gs.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/6_scheduler25.prism-gs.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/6_scheduler50.prism-gs.output
-
56examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/7_dpm100.prism-gs.output
-
56examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/7_dpm200.prism-gs.output
-
56examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-gs/7_dpm300.prism-gs.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus2_3_2.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus2_4_2.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus2_5_2.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus3_3_2.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus3_4_2.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/1_consensus3_5_2.prism.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/2_zeroconf4.prism.output
-
97examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/2_zeroconf6.prism.output
-
97examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/2_zeroconf8.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/3_zeroconf-tb2_14.prism.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/3_zeroconf-tb4_10.prism.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/3_zeroconf-tb4_14.prism.output
-
81examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/4_team2obj_3.prism.output
-
81examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/4_team2obj_4.prism.output
-
79examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/4_team2obj_5.prism.output
-
96examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/5_team3obj_3.prism.output
-
98examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/5_team3obj_4.prism.output
-
95examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/5_team3obj_5.prism.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/6_scheduler05.prism.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/6_scheduler25.prism.output
-
69examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/6_scheduler50.prism.output
-
67examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/7_dpm100.prism.output
-
66examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/7_dpm200.prism.output
-
66examples/multi-objective/mdp/benchmarks_numerical/2016-06-13/prism-valiter/7_dpm300.prism.output
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:38:54 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_3_2.nm consensus/consensus2_3_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus2_3_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_3_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.8916673903 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.8916673903 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000391, setup 0.00) |
|||
|
|||
Time for model construction: 0.051 seconds. |
|||
|
|||
Type: MDP |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2044 nodes (2 terminal), 1190 minterms, vars: 17r/17c/15nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.019 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000304, setup 0.00) |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2210 nodes (2 terminal), 1190 minterms, vars: 18r/18c/15nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000304, setup 0.00) |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2522 nodes (2 terminal), 1190 minterms, vars: 19r/19c/15nd |
|||
|
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2522 nodes (2 terminal), 1190 minterms, vars: 19r/19c/15nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.0 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.01 seconds (average 0.000727, setup 0.00) |
|||
|
|||
yes = 38, no = 116, maybe = 537 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 17 iterations in 0.00 seconds (average 0.000059, setup 0.00) |
|||
Iterative method: 9 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
Iterative method: 17 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
The value iteration(s) took 0.021 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.021 s. |
|||
|
|||
Value in the initial state: 0.10833260970000025 |
|||
|
|||
Time for model checking: 0.12 seconds. |
|||
|
|||
Result: 0.10833260970000025 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:38:57 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_4_2.nm consensus/consensus2_4_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus2_4_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_4_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9882640457 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error coin2_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 c2 v2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9882640457 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.02 seconds (average 0.000548, setup 0.00) |
|||
|
|||
Time for model construction: 0.07 seconds. |
|||
|
|||
Type: MDP |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 3647 nodes (2 terminal), 2616 minterms, vars: 22r/22c/21nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.01 seconds (average 0.000387, setup 0.00) |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 3851 nodes (2 terminal), 2616 minterms, vars: 23r/23c/21nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.01 seconds (average 0.000355, setup 0.00) |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 4185 nodes (2 terminal), 2616 minterms, vars: 24r/24c/21nd |
|||
|
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 4185 nodes (2 terminal), 2616 minterms, vars: 24r/24c/21nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.0 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.01 seconds (average 0.001182, setup 0.00) |
|||
|
|||
yes = 84, no = 232, maybe = 1201 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 23 iterations in 0.00 seconds (average 0.000174, setup 0.00) |
|||
Iterative method: 9 iterations in 0.00 seconds (average 0.000111, setup 0.00) |
|||
Iterative method: 10 iterations in 0.00 seconds (average 0.000100, setup 0.00) |
|||
The value iteration(s) took 0.024 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.024 s. |
|||
|
|||
Value in the initial state: 0.011735954299999853 |
|||
|
|||
Time for model checking: 0.189 seconds. |
|||
|
|||
Result: 0.011735954299999853 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:00 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_5_2.nm consensus/consensus2_5_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus2_5_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_5_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9987286134 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error coin2_error coin3_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 c2 v2 c3 v3 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9987286134 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.03 seconds (average 0.000795, setup 0.00) |
|||
|
|||
Time for model construction: 0.096 seconds. |
|||
|
|||
Type: MDP |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5160 nodes (2 terminal), 5468 minterms, vars: 25r/25c/27nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.02 seconds (average 0.000487, setup 0.00) |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5368 nodes (2 terminal), 5468 minterms, vars: 26r/26c/27nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.02 seconds (average 0.000436, setup 0.00) |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5692 nodes (2 terminal), 5468 minterms, vars: 27r/27c/27nd |
|||
|
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5692 nodes (2 terminal), 5468 minterms, vars: 27r/27c/27nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.02 seconds (average 0.001455, setup 0.00) |
|||
|
|||
yes = 176, no = 464, maybe = 2529 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 29 iterations in 0.01 seconds (average 0.000276, setup 0.00) |
|||
Iterative method: 9 iterations in 0.00 seconds (average 0.000111, setup 0.00) |
|||
Iterative method: 29 iterations in 0.01 seconds (average 0.000172, setup 0.00) |
|||
The value iteration(s) took 0.039 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.04 s. |
|||
|
|||
Value in the initial state: 0.001271386600000368 |
|||
|
|||
Time for model checking: 0.321 seconds. |
|||
|
|||
Result: 0.001271386600000368 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:03 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_3_2.nm consensus/consensus3_3_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus3_3_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_3_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.7709112445 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.7709112445 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.10 seconds (average 0.003333, setup 0.00) |
|||
|
|||
Time for model construction: 0.193 seconds. |
|||
|
|||
Type: MDP |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 12325 nodes (2 terminal), 46702 minterms, vars: 24r/24c/22nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.10 seconds (average 0.003400, setup 0.00) |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 14942 nodes (2 terminal), 46702 minterms, vars: 25r/25c/22nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.10 seconds (average 0.003367, setup 0.00) |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 16175 nodes (2 terminal), 46702 minterms, vars: 26r/26c/22nd |
|||
|
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 16175 nodes (2 terminal), 46702 minterms, vars: 26r/26c/22nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.002 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 16 iterations in 0.11 seconds (average 0.006812, setup 0.00) |
|||
|
|||
yes = 156, no = 2868, maybe = 14431 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 0.03 seconds (average 0.001450, setup 0.00) |
|||
Iterative method: 12 iterations in 0.02 seconds (average 0.001333, setup 0.00) |
|||
Iterative method: 15 iterations in 0.02 seconds (average 0.001333, setup 0.00) |
|||
The value iteration(s) took 0.135 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.136 s. |
|||
|
|||
Value in the initial state: 0.22908875549999985 |
|||
|
|||
Time for model checking: 0.919 seconds. |
|||
|
|||
Result: 0.22908875549999985 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:06 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_4_2.nm consensus/consensus3_4_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus3_4_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_4_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9475183421 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error coin2_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 c2 v2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9475183421 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.29 seconds (average 0.007150, setup 0.00) |
|||
|
|||
Time for model construction: 0.43 seconds. |
|||
|
|||
Type: MDP |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 25874 nodes (2 terminal), 164012 minterms, vars: 30r/30c/31nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.31 seconds (average 0.007650, setup 0.00) |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 29567 nodes (2 terminal), 164012 minterms, vars: 31r/31c/31nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.30 seconds (average 0.007400, setup 0.00) |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 31366 nodes (2 terminal), 164012 minterms, vars: 32r/32c/31nd |
|||
|
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 31366 nodes (2 terminal), 164012 minterms, vars: 32r/32c/31nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.006 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.003 seconds. |
|||
|
|||
Prob0A: 20 iterations in 0.25 seconds (average 0.012450, setup 0.00) |
|||
|
|||
yes = 492, no = 10320, maybe = 50205 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 26 iterations in 0.12 seconds (average 0.004615, setup 0.00) |
|||
Iterative method: 12 iterations in 0.06 seconds (average 0.004500, setup 0.00) |
|||
Iterative method: 26 iterations in 0.13 seconds (average 0.005000, setup 0.00) |
|||
The value iteration(s) took 0.534 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.535 s. |
|||
|
|||
Value in the initial state: 0.052481657900000145 |
|||
|
|||
Time for model checking: 2.767 seconds. |
|||
|
|||
Result: 0.052481657900000145 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:11 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_5_2.nm consensus/consensus3_5_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "consensus/consensus3_5_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_5_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9879770423 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error coin2_error coin3_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 c2 v2 c3 v3 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9879770423 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.43 seconds (average 0.008700, setup 0.00) |
|||
|
|||
Time for model construction: 0.671 seconds. |
|||
|
|||
Type: MDP |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 39636 nodes (2 terminal), 487456 minterms, vars: 33r/33c/40nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.55 seconds (average 0.011040, setup 0.00) |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 43778 nodes (2 terminal), 487456 minterms, vars: 34r/34c/40nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.49 seconds (average 0.009900, setup 0.00) |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 46178 nodes (2 terminal), 487456 minterms, vars: 35r/35c/40nd |
|||
|
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 46178 nodes (2 terminal), 487456 minterms, vars: 35r/35c/40nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.02 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.01 seconds. |
|||
|
|||
Prob0A: 24 iterations in 0.45 seconds (average 0.018583, setup 0.00) |
|||
|
|||
yes = 1416, no = 29808, maybe = 149905 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 32 iterations in 0.46 seconds (average 0.014094, setup 0.00) |
|||
Iterative method: 12 iterations in 0.17 seconds (average 0.013917, setup 0.00) |
|||
Iterative method: 32 iterations in 0.46 seconds (average 0.014250, setup 0.00) |
|||
The value iteration(s) took 1.666 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 1.667 s. |
|||
|
|||
Value in the initial state: 0.012022957700000277 |
|||
|
|||
Time for model checking: 6.56 seconds. |
|||
|
|||
Result: 0.012022957700000277 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:20 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf4.nm zeroconf/zeroconf4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf/zeroconf4.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.07 seconds (average 0.000603, setup 0.00) |
|||
|
|||
Time for model construction: 0.138 seconds. |
|||
|
|||
Type: MDP |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 2515 nodes (4 terminal), 17152 minterms, vars: 36r/36c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.06 seconds (average 0.000483, setup 0.00) |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 2604 nodes (4 terminal), 17152 minterms, vars: 37r/37c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.07 seconds (average 0.000603, setup 0.00) |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 3754 nodes (4 terminal), 17152 minterms, vars: 38r/38c/7nd |
|||
|
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 3754 nodes (4 terminal), 17152 minterms, vars: 38r/38c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.034 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.048 seconds. |
|||
|
|||
Prob0A: 82 iterations in 0.03 seconds (average 0.000366, setup 0.00) |
|||
|
|||
yes = 4813, no = 172, maybe = 464 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 78 iterations in 0.02 seconds (average 0.000269, setup 0.00) |
|||
Iterative method: 78 iterations in 0.02 seconds (average 0.000269, setup 0.00) |
|||
The value iteration(s) took 0.076 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.076 s. |
|||
|
|||
Value in the initial state: 3.075787401574803E-4 |
|||
|
|||
Time for model checking: 3.693 seconds. |
|||
|
|||
Result: 3.075787401574803E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,97 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:26 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf6.nm zeroconf/zeroconf6_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf/zeroconf6.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf6_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.9997523901 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error6 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 c5 c6 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.9997523901 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.10 seconds (average 0.000805, setup 0.00) |
|||
|
|||
Time for model construction: 0.173 seconds. |
|||
|
|||
Type: MDP |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 3238 nodes (4 terminal), 32003 minterms, vars: 40r/40c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.08 seconds (average 0.000648, setup 0.00) |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 3325 nodes (4 terminal), 32003 minterms, vars: 41r/41c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.12 seconds (average 0.000969, setup 0.00) |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 4445 nodes (4 terminal), 32003 minterms, vars: 42r/42c/7nd |
|||
|
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 4445 nodes (4 terminal), 32003 minterms, vars: 42r/42c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.069 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.081 seconds. |
|||
|
|||
Prob0A: 88 iterations in 0.04 seconds (average 0.000409, setup 0.00) |
|||
|
|||
yes = 9673, no = 238, maybe = 632 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 82 iterations in 0.04 seconds (average 0.000524, setup 0.00) |
|||
Iterative method: 82 iterations in 0.04 seconds (average 0.000488, setup 0.00) |
|||
Iterative method: 82 iterations in 0.04 seconds (average 0.000512, setup 0.00) |
|||
Iterative method: 82 iterations in 0.04 seconds (average 0.000524, setup 0.00) |
|||
The value iteration(s) took 0.231 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.231 s. |
|||
|
|||
Value in the initial state: 2.476283452671333E-4 |
|||
|
|||
Time for model checking: 8.101 seconds. |
|||
|
|||
Result: 2.476283452671333E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,97 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:37 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf8.nm zeroconf/zeroconf8_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf/zeroconf8.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf8_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.9999910613 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error8 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 c5 c6 c7 c8 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.9999910613 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.17 seconds (average 0.001200, setup 0.00) |
|||
|
|||
Time for model construction: 0.246 seconds. |
|||
|
|||
Type: MDP |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 4321 nodes (4 terminal), 52163 minterms, vars: 46r/46c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.14 seconds (average 0.001029, setup 0.00) |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 4412 nodes (4 terminal), 52163 minterms, vars: 47r/47c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.19 seconds (average 0.001364, setup 0.00) |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 5586 nodes (4 terminal), 52163 minterms, vars: 48r/48c/7nd |
|||
|
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 5586 nodes (4 terminal), 52163 minterms, vars: 48r/48c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.136 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.161 seconds. |
|||
|
|||
Prob0A: 94 iterations in 0.05 seconds (average 0.000574, setup 0.00) |
|||
|
|||
yes = 16117, no = 304, maybe = 800 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 86 iterations in 0.07 seconds (average 0.000837, setup 0.00) |
|||
Iterative method: 86 iterations in 0.07 seconds (average 0.000802, setup 0.00) |
|||
Iterative method: 86 iterations in 0.07 seconds (average 0.000837, setup 0.00) |
|||
Iterative method: 86 iterations in 0.08 seconds (average 0.000895, setup 0.00) |
|||
The value iteration(s) took 0.386 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.386 s. |
|||
|
|||
Value in the initial state: 9.030555331603746E-6 |
|||
|
|||
Time for model checking: 15.146 seconds. |
|||
|
|||
Result: 9.030555331603746E-6 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:39:54 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb2_14.nm zeroconf-tb/zeroconf-tb2_14_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb2_14.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb2_14_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.81 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error2 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.81 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.31 seconds (average 0.002452, setup 0.00) |
|||
|
|||
Time for model construction: 0.388 seconds. |
|||
|
|||
Type: MDP |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 9057 nodes (4 terminal), 92605 minterms, vars: 36r/36c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.39 seconds (average 0.003063, setup 0.00) |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 10373 nodes (4 terminal), 92605 minterms, vars: 37r/37c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.001 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.43 seconds (average 0.003429, setup 0.00) |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 14230 nodes (4 terminal), 92605 minterms, vars: 38r/38c/8nd |
|||
|
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 14230 nodes (4 terminal), 92605 minterms, vars: 38r/38c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.189 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.228 seconds. |
|||
|
|||
Prob0A: 20 iterations in 0.05 seconds (average 0.002350, setup 0.00) |
|||
|
|||
yes = 23767, no = 3321, maybe = 2484 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 24 iterations in 0.04 seconds (average 0.001583, setup 0.00) |
|||
Iterative method: 24 iterations in 0.04 seconds (average 0.001458, setup 0.00) |
|||
Iterative method: 24 iterations in 0.04 seconds (average 0.001583, setup 0.00) |
|||
The value iteration(s) took 0.179 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.179 s. |
|||
|
|||
Value in the initial state: 8.059348391417451E-8 |
|||
|
|||
Time for model checking: 30.471 seconds. |
|||
|
|||
Result: 8.059348391417451E-8 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:40:27 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb4_10.nm zeroconf-tb/zeroconf-tb4_10_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb4_10.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb4_10_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.23 seconds (average 0.001832, setup 0.00) |
|||
|
|||
Time for model construction: 0.312 seconds. |
|||
|
|||
Type: MDP |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 9893 nodes (4 terminal), 63353 minterms, vars: 42r/42c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.26 seconds (average 0.002104, setup 0.00) |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 11570 nodes (4 terminal), 63353 minterms, vars: 43r/43c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.26 seconds (average 0.002080, setup 0.00) |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 14283 nodes (4 terminal), 63353 minterms, vars: 44r/44c/8nd |
|||
|
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 14283 nodes (4 terminal), 63353 minterms, vars: 44r/44c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.173 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.159 seconds. |
|||
|
|||
Prob0A: 6 iterations in 0.02 seconds (average 0.003167, setup 0.00) |
|||
|
|||
yes = 17645, no = 902, maybe = 1123 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 16 iterations in 0.02 seconds (average 0.001063, setup 0.00) |
|||
Iterative method: 16 iterations in 0.02 seconds (average 0.001000, setup 0.00) |
|||
The value iteration(s) took 0.115 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.115 s. |
|||
|
|||
Value in the initial state: 0.33353838582677153 |
|||
|
|||
Time for model checking: 27.859 seconds. |
|||
|
|||
Result: 0.33353838582677153 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:40:58 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb4_14.nm zeroconf-tb/zeroconf-tb4_14_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb4_14.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb4_14_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.44 seconds (average 0.003311, setup 0.00) |
|||
|
|||
Time for model construction: 0.534 seconds. |
|||
|
|||
Type: MDP |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 14874 nodes (4 terminal), 138025 minterms, vars: 42r/42c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.53 seconds (average 0.004000, setup 0.00) |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 16458 nodes (4 terminal), 138025 minterms, vars: 43r/43c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.52 seconds (average 0.003909, setup 0.00) |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 19902 nodes (4 terminal), 138025 minterms, vars: 44r/44c/8nd |
|||
|
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 19902 nodes (4 terminal), 138025 minterms, vars: 44r/44c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.321 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.353 seconds. |
|||
|
|||
Prob0A: 12 iterations in 0.04 seconds (average 0.003417, setup 0.00) |
|||
|
|||
yes = 38966, no = 1353, maybe = 2649 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 0.05 seconds (average 0.002450, setup 0.00) |
|||
Iterative method: 20 iterations in 0.05 seconds (average 0.002250, setup 0.00) |
|||
The value iteration(s) took 0.203 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.204 s. |
|||
|
|||
Value in the initial state: 3.075787401574803E-4 |
|||
|
|||
Time for model checking: 72.996 seconds. |
|||
|
|||
Result: 3.075787401574803E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,81 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:42:13 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_3.nm team/team2obj_3_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team2obj_3.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_3_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.003154, setup 0.00) |
|||
|
|||
Time for model construction: 0.147 seconds. |
|||
|
|||
Type: MDP |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 16500 nodes (4 terminal), 15228 minterms, vars: 24r/24c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.03 seconds (average 0.002538, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.015 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.04 seconds (average 0.003182, setup 0.00) |
|||
|
|||
yes = 546, no = 0, maybe = 11929 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000714, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000571, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000571, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000500, setup 0.00) |
|||
The value iteration(s) took 0.112 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.112 s. |
|||
|
|||
Value in the initial state: 0.8714285710612256 |
|||
|
|||
Time for model checking: 9.82 seconds. |
|||
|
|||
Result: 0.8714285710612256 (value in the initial state) |
|||
|
|||
@ -0,0 +1,81 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:42:42 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_4.nm team/team2obj_4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team2obj_4.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.34 seconds (average 0.021375, setup 0.00) |
|||
|
|||
Time for model construction: 0.961 seconds. |
|||
|
|||
Type: MDP |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 101788 nodes (4 terminal), 116464 minterms, vars: 36r/36c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.35 seconds (average 0.022062, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.17 seconds. |
|||
|
|||
Prob0A: 13 iterations in 0.33 seconds (average 0.025538, setup 0.00) |
|||
|
|||
yes = 4872, no = 0, maybe = 91793 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 17 iterations in 0.08 seconds (average 0.004294, setup 0.00) |
|||
Iterative method: 17 iterations in 0.07 seconds (average 0.004353, setup 0.00) |
|||
Iterative method: 17 iterations in 0.08 seconds (average 0.004529, setup 0.00) |
|||
Iterative method: 17 iterations in 0.08 seconds (average 0.004529, setup 0.00) |
|||
The value iteration(s) took 1.038 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 1.038 s. |
|||
|
|||
Value in the initial state: 0.9438775507764041 |
|||
|
|||
Time for model checking: 241.247 seconds. |
|||
|
|||
Result: 0.9438775507764041 (value in the initial state) |
|||
|
|||
@ -0,0 +1,79 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:52:43 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_5.nm team/team2obj_5_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team2obj_5.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_5_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 sensor5 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 state5 m5_t1 m5_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.47 seconds (average 0.077105, setup 0.00) |
|||
|
|||
Time for model construction: 4.707 seconds. |
|||
|
|||
Type: MDP |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 361071 nodes (4 terminal), 1084752 minterms, vars: 40r/40c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.018 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.35 seconds (average 0.071158, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 1.624 seconds. |
|||
|
|||
Prob0A: 15 iterations in 1.46 seconds (average 0.097267, setup 0.00) |
|||
|
|||
yes = 52200, no = 0, maybe = 855793 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 0.85 seconds (average 0.042050, setup 0.01) |
|||
Iterative method: 20 iterations in 0.83 seconds (average 0.041350, setup 0.01) |
|||
The value iteration(s) took 4.231 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 4.231 s. |
|||
|
|||
Value in the initial state: 1.0 |
|||
|
|||
Time for model checking: 7198.624 seconds. |
|||
|
|||
Result: 1.0 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:42:27 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_3.nm team/team3obj_3_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team3obj_3.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_3_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.003077, setup 0.00) |
|||
|
|||
Time for model construction: 0.147 seconds. |
|||
|
|||
Type: MDP |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 16500 nodes (4 terminal), 15228 minterms, vars: 24r/24c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.014 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.002692, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.03 seconds (average 0.002077, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 21624 nodes (4 terminal), 15228 minterms, vars: 26r/26c/10nd |
|||
|
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 21624 nodes (4 terminal), 15228 minterms, vars: 26r/26c/10nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.021 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 0.009 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.07 seconds (average 0.006273, setup 0.00) |
|||
|
|||
yes = 1020, no = 0, maybe = 11455 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000786, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000643, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000643, setup 0.00) |
|||
The value iteration(s) took 0.108 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.108 s. |
|||
|
|||
Value in the initial state: 0.7448979591841851 |
|||
|
|||
Time for model checking: 13.151 seconds. |
|||
|
|||
Result: 0.7448979591841851 (value in the initial state) |
|||
|
|||
@ -0,0 +1,98 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:46:46 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_4.nm team/team3obj_4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team3obj_4.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.37 seconds (average 0.023312, setup 0.00) |
|||
|
|||
Time for model construction: 0.991 seconds. |
|||
|
|||
Type: MDP |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 101788 nodes (4 terminal), 116464 minterms, vars: 36r/36c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.33 seconds (average 0.020688, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.37 seconds (average 0.022875, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 130439 nodes (4 terminal), 116464 minterms, vars: 38r/38c/13nd |
|||
|
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 130439 nodes (4 terminal), 116464 minterms, vars: 38r/38c/13nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.143 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 0.09 seconds. |
|||
|
|||
Prob0A: 13 iterations in 0.54 seconds (average 0.041769, setup 0.00) |
|||
|
|||
yes = 8784, no = 0, maybe = 87881 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005176, setup 0.01) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005118, setup 0.00) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005059, setup 0.00) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005235, setup 0.00) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005059, setup 0.00) |
|||
The value iteration(s) took 1.113 seconds altogether. |
|||
Number of weight vectors used: 5 |
|||
Multi-objective value iterations took 1.113 s. |
|||
|
|||
Value in the initial state: 0.9285714285727903 |
|||
|
|||
Time for model checking: 353.141 seconds. |
|||
|
|||
Result: 0.9285714285727903 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 14:52:49 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_5.nm team/team3obj_5_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "team/team3obj_5.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_5_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 sensor5 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 state5 m5_t1 m5_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.37 seconds (average 0.072316, setup 0.00) |
|||
|
|||
Time for model construction: 4.376 seconds. |
|||
|
|||
Type: MDP |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 361071 nodes (4 terminal), 1084752 minterms, vars: 40r/40c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.018 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.32 seconds (average 0.069474, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.26 seconds (average 0.066263, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 449699 nodes (4 terminal), 1084752 minterms, vars: 42r/42c/16nd |
|||
|
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 449699 nodes (4 terminal), 1084752 minterms, vars: 42r/42c/16nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 1.741 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 1.108 seconds. |
|||
|
|||
Prob0A: 15 iterations in 2.55 seconds (average 0.169933, setup 0.00) |
|||
|
|||
yes = 90960, no = 0, maybe = 817033 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 1.03 seconds (average 0.051050, setup 0.01) |
|||
Iterative method: 20 iterations in 1.04 seconds (average 0.051600, setup 0.01) |
|||
The value iteration(s) took 5.24 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 5.241 s. |
|||
|
|||
Value in the initial state: 1.0 |
|||
|
|||
Time for model checking: 9736.935 seconds. |
|||
|
|||
Result: 1.0 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 17:35:13 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler05.nm scheduler/scheduler05_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "scheduler/scheduler05.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler05_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 99 iterations in 0.30 seconds (average 0.003071, setup 0.00) |
|||
|
|||
Time for model construction: 0.374 seconds. |
|||
|
|||
Type: MDP |
|||
States: 31965 (1 initial) |
|||
Transitions: 60434 |
|||
Choices: 57965 |
|||
|
|||
Transition matrix: 7870 nodes (5 terminal), 60434 minterms, vars: 30r/30c/10nd |
|||
|
|||
States: 31965 (1 initial) |
|||
Transitions: 60434 |
|||
Choices: 57965 |
|||
|
|||
Transition matrix: 7870 nodes (5 terminal), 60434 minterms, vars: 30r/30c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.002000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 31965 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 132 iterations in 0.24 seconds (average 0.001811, setup 0.00) |
|||
Iterative method: 131 iterations in 0.31 seconds (average 0.002351, setup 0.00) |
|||
Iterative method: 223 iterations in 0.53 seconds (average 0.002359, setup 0.00) |
|||
Iterative method: 193 iterations in 0.45 seconds (average 0.002342, setup 0.00) |
|||
Iterative method: 141 iterations in 0.34 seconds (average 0.002433, setup 0.00) |
|||
Iterative method: 126 iterations in 0.29 seconds (average 0.002302, setup 0.00) |
|||
Iterative method: 128 iterations in 0.31 seconds (average 0.002391, setup 0.00) |
|||
Iterative method: 125 iterations in 0.30 seconds (average 0.002384, setup 0.00) |
|||
The value iteration(s) took 2.91 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 2.91 s. |
|||
|
|||
Value in the initial state: 16.169598765430386 |
|||
|
|||
Time for model checking: 3.363 seconds. |
|||
|
|||
Result: 16.169598765430386 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 17:35:19 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler25.nm scheduler/scheduler25_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "scheduler/scheduler25.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler25_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 419 iterations in 6.52 seconds (average 0.015566, setup 0.00) |
|||
|
|||
Time for model construction: 6.727 seconds. |
|||
|
|||
Type: MDP |
|||
States: 633735 (1 initial) |
|||
Transitions: 1179444 |
|||
Choices: 1168375 |
|||
|
|||
Transition matrix: 25430 nodes (5 terminal), 1179444 minterms, vars: 35r/35c/10nd |
|||
|
|||
States: 633735 (1 initial) |
|||
Transitions: 1179444 |
|||
Choices: 1168375 |
|||
|
|||
Transition matrix: 25430 nodes (5 terminal), 1179444 minterms, vars: 35r/35c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.01 seconds (average 0.006000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 633735 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 552 iterations in 19.70 seconds (average 0.035690, setup 0.00) |
|||
Iterative method: 551 iterations in 26.77 seconds (average 0.048575, setup 0.01) |
|||
Iterative method: 1033 iterations in 48.95 seconds (average 0.047379, setup 0.00) |
|||
Iterative method: 879 iterations in 41.70 seconds (average 0.047438, setup 0.00) |
|||
Iterative method: 594 iterations in 28.37 seconds (average 0.047763, setup 0.00) |
|||
Iterative method: 524 iterations in 24.91 seconds (average 0.047527, setup 0.00) |
|||
Iterative method: 541 iterations in 25.82 seconds (average 0.047726, setup 0.00) |
|||
Iterative method: 542 iterations in 25.75 seconds (average 0.047500, setup 0.00) |
|||
The value iteration(s) took 243.66 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 243.66 s. |
|||
|
|||
Value in the initial state: 15.81452325633229 |
|||
|
|||
Time for model checking: 248.97 seconds. |
|||
|
|||
Result: 15.81452325633229 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 17:39:36 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler50.nm scheduler/scheduler50_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "scheduler/scheduler50.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler50_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 819 iterations in 25.06 seconds (average 0.030596, setup 0.00) |
|||
|
|||
Time for model construction: 25.354 seconds. |
|||
|
|||
Type: MDP |
|||
States: 2457510 (1 initial) |
|||
Transitions: 4564394 |
|||
Choices: 4542575 |
|||
|
|||
Transition matrix: 45541 nodes (5 terminal), 4564394 minterms, vars: 37r/37c/10nd |
|||
|
|||
States: 2457510 (1 initial) |
|||
Transitions: 4564394 |
|||
Choices: 4542575 |
|||
|
|||
Transition matrix: 45541 nodes (5 terminal), 4564394 minterms, vars: 37r/37c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.01 seconds (average 0.011000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 2457510 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 1077 iterations in 147.26 seconds (average 0.136725, setup 0.01) |
|||
Iterative method: 1076 iterations in 200.63 seconds (average 0.186444, setup 0.01) |
|||
Iterative method: 2045 iterations in 377.10 seconds (average 0.184393, setup 0.02) |
|||
Iterative method: 1715 iterations in 321.81 seconds (average 0.187638, setup 0.01) |
|||
Iterative method: 1163 iterations in 214.18 seconds (average 0.184150, setup 0.01) |
|||
Iterative method: 1028 iterations in 189.16 seconds (average 0.183994, setup 0.01) |
|||
Iterative method: 1058 iterations in 195.37 seconds (average 0.184645, setup 0.01) |
|||
Iterative method: 1059 iterations in 197.55 seconds (average 0.186530, setup 0.01) |
|||
The value iteration(s) took 1850.07 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 1850.071 s. |
|||
|
|||
Value in the initial state: 15.773985890650346 |
|||
|
|||
Time for model checking: 1868.047 seconds. |
|||
|
|||
Result: 15.773985890650346 (value in the initial state) |
|||
|
|||
@ -0,0 +1,56 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 18:11:12 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm100.nm dpm/dpm100_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "dpm/dpm100.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm100_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000077, setup 0.00) |
|||
|
|||
Time for model construction: 0.031 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
|
|||
Error: Cannot do Gauss Seidel method for step bounded objectives!. |
|||
|
|||
Warning: CUDD reports 13 non-zero references. |
|||
|
|||
@ -0,0 +1,56 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 18:11:15 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm200.nm dpm/dpm200_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "dpm/dpm200.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm200_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=200 ], R{"queue"}<=170 [ C<=200 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=200 ], R{"queue"}<=170 [ C<=200 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000077, setup 0.00) |
|||
|
|||
Time for model construction: 0.031 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
|
|||
Error: Cannot do Gauss Seidel method for step bounded objectives!. |
|||
|
|||
Warning: CUDD reports 13 non-zero references. |
|||
|
|||
@ -0,0 +1,56 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 18:11:18 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm300.nm dpm/dpm300_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs |
|||
|
|||
Parsing model file "dpm/dpm300.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm300_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=300 ], R{"queue"}<=270 [ C<=300 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=300 ], R{"queue"}<=270 [ C<=300 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000077, setup 0.00) |
|||
|
|||
Time for model construction: 0.031 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
|
|||
Error: Cannot do Gauss Seidel method for step bounded objectives!. |
|||
|
|||
Warning: CUDD reports 13 non-zero references. |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:11 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_3_2.nm consensus/consensus2_3_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus2_3_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_3_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.8916673903 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.8916673903 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000348, setup 0.00) |
|||
|
|||
Time for model construction: 0.063 seconds. |
|||
|
|||
Type: MDP |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2044 nodes (2 terminal), 1190 minterms, vars: 17r/17c/15nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.029 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000261, setup 0.00) |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2210 nodes (2 terminal), 1190 minterms, vars: 18r/18c/15nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 23 iterations in 0.01 seconds (average 0.000261, setup 0.00) |
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2522 nodes (2 terminal), 1190 minterms, vars: 19r/19c/15nd |
|||
|
|||
States: 691 (1 initial) |
|||
Transitions: 1190 |
|||
Choices: 1190 |
|||
|
|||
Transition matrix: 2522 nodes (2 terminal), 1190 minterms, vars: 19r/19c/15nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.0 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.0 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.01 seconds (average 0.000636, setup 0.00) |
|||
|
|||
yes = 38, no = 116, maybe = 537 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 0.00 seconds (average 0.000050, setup 0.00) |
|||
Iterative method: 10 iterations in 0.00 seconds (average 0.000100, setup 0.00) |
|||
Iterative method: 20 iterations in 0.00 seconds (average 0.000050, setup 0.00) |
|||
The value iteration(s) took 0.03 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.031 s. |
|||
|
|||
Value in the initial state: 0.10833260970000025 |
|||
|
|||
Time for model checking: 0.155 seconds. |
|||
|
|||
Result: 0.10833260970000025 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:14 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_4_2.nm consensus/consensus2_4_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus2_4_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_4_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9882640457 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error coin2_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 c2 v2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9882640457 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.02 seconds (average 0.000548, setup 0.00) |
|||
|
|||
Time for model construction: 0.076 seconds. |
|||
|
|||
Type: MDP |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 3647 nodes (2 terminal), 2616 minterms, vars: 22r/22c/21nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.014 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.01 seconds (average 0.000387, setup 0.00) |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 3851 nodes (2 terminal), 2616 minterms, vars: 23r/23c/21nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 31 iterations in 0.01 seconds (average 0.000419, setup 0.00) |
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 4185 nodes (2 terminal), 2616 minterms, vars: 24r/24c/21nd |
|||
|
|||
States: 1517 (1 initial) |
|||
Transitions: 2616 |
|||
Choices: 2616 |
|||
|
|||
Transition matrix: 4185 nodes (2 terminal), 2616 minterms, vars: 24r/24c/21nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.0 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.02 seconds (average 0.001455, setup 0.00) |
|||
|
|||
yes = 84, no = 232, maybe = 1201 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 28 iterations in 0.00 seconds (average 0.000143, setup 0.00) |
|||
Iterative method: 10 iterations in 0.00 seconds (average 0.000100, setup 0.00) |
|||
Iterative method: 12 iterations in 0.00 seconds (average 0.000083, setup 0.00) |
|||
The value iteration(s) took 0.032 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.032 s. |
|||
|
|||
Value in the initial state: 0.011735954299999853 |
|||
|
|||
Time for model checking: 0.21 seconds. |
|||
|
|||
Result: 0.011735954299999853 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:16 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus2_5_2.nm consensus/consensus2_5_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus2_5_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus2_5_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9987286134 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 coin1_error coin2_error coin3_error |
|||
Variables: s1 r1 p1 s2 r2 p2 c1 v1 c2 v2 c3 v3 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9987286134 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.03 seconds (average 0.000872, setup 0.00) |
|||
|
|||
Time for model construction: 0.102 seconds. |
|||
|
|||
Type: MDP |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5160 nodes (2 terminal), 5468 minterms, vars: 25r/25c/27nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.02 seconds (average 0.000564, setup 0.00) |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5368 nodes (2 terminal), 5468 minterms, vars: 26r/26c/27nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 39 iterations in 0.02 seconds (average 0.000462, setup 0.00) |
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5692 nodes (2 terminal), 5468 minterms, vars: 27r/27c/27nd |
|||
|
|||
States: 3169 (1 initial) |
|||
Transitions: 5468 |
|||
Choices: 5468 |
|||
|
|||
Transition matrix: 5692 nodes (2 terminal), 5468 minterms, vars: 27r/27c/27nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.02 seconds (average 0.001455, setup 0.00) |
|||
|
|||
yes = 176, no = 464, maybe = 2529 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 36 iterations in 0.01 seconds (average 0.000222, setup 0.00) |
|||
Iterative method: 10 iterations in 0.00 seconds (average 0.000200, setup 0.00) |
|||
Iterative method: 36 iterations in 0.01 seconds (average 0.000194, setup 0.00) |
|||
The value iteration(s) took 0.045 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.045 s. |
|||
|
|||
Value in the initial state: 0.001271386600000368 |
|||
|
|||
Time for model checking: 0.35 seconds. |
|||
|
|||
Result: 0.001271386600000368 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:19 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_3_2.nm consensus/consensus3_3_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus3_3_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_3_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.7709112445 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.7709112445 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.10 seconds (average 0.003233, setup 0.00) |
|||
|
|||
Time for model construction: 0.2 seconds. |
|||
|
|||
Type: MDP |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 12325 nodes (2 terminal), 46702 minterms, vars: 24r/24c/22nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.10 seconds (average 0.003167, setup 0.00) |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 14942 nodes (2 terminal), 46702 minterms, vars: 25r/25c/22nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 30 iterations in 0.09 seconds (average 0.003033, setup 0.00) |
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 16175 nodes (2 terminal), 46702 minterms, vars: 26r/26c/22nd |
|||
|
|||
States: 17455 (1 initial) |
|||
Transitions: 46702 |
|||
Choices: 46702 |
|||
|
|||
Transition matrix: 16175 nodes (2 terminal), 46702 minterms, vars: 26r/26c/22nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.001 seconds. |
|||
|
|||
Prob0A: 16 iterations in 0.10 seconds (average 0.006437, setup 0.00) |
|||
|
|||
yes = 156, no = 2868, maybe = 14431 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 23 iterations in 0.04 seconds (average 0.001478, setup 0.00) |
|||
Iterative method: 14 iterations in 0.02 seconds (average 0.001357, setup 0.00) |
|||
Iterative method: 18 iterations in 0.03 seconds (average 0.001667, setup 0.00) |
|||
The value iteration(s) took 0.167 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.168 s. |
|||
|
|||
Value in the initial state: 0.22908875549999985 |
|||
|
|||
Time for model checking: 0.928 seconds. |
|||
|
|||
Result: 0.22908875549999985 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:22 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_4_2.nm consensus/consensus3_4_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus3_4_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_4_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9475183421 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error coin2_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 c2 v2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9475183421 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.32 seconds (average 0.007975, setup 0.00) |
|||
|
|||
Time for model construction: 0.47 seconds. |
|||
|
|||
Type: MDP |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 25874 nodes (2 terminal), 164012 minterms, vars: 30r/30c/31nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.017 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.27 seconds (average 0.006800, setup 0.00) |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 29567 nodes (2 terminal), 164012 minterms, vars: 31r/31c/31nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 40 iterations in 0.28 seconds (average 0.007075, setup 0.00) |
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 31366 nodes (2 terminal), 164012 minterms, vars: 32r/32c/31nd |
|||
|
|||
States: 61017 (1 initial) |
|||
Transitions: 164012 |
|||
Choices: 164012 |
|||
|
|||
Transition matrix: 31366 nodes (2 terminal), 164012 minterms, vars: 32r/32c/31nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.005 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.003 seconds. |
|||
|
|||
Prob0A: 20 iterations in 0.23 seconds (average 0.011500, setup 0.00) |
|||
|
|||
yes = 492, no = 10320, maybe = 50205 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 31 iterations in 0.16 seconds (average 0.005161, setup 0.00) |
|||
Iterative method: 14 iterations in 0.08 seconds (average 0.005429, setup 0.00) |
|||
Iterative method: 31 iterations in 0.17 seconds (average 0.005419, setup 0.00) |
|||
The value iteration(s) took 0.642 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.642 s. |
|||
|
|||
Value in the initial state: 0.052481657900000145 |
|||
|
|||
Time for model checking: 2.779 seconds. |
|||
|
|||
Result: 0.052481657900000145 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:27 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism consensus/consensus3_5_2.nm consensus/consensus3_5_2_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "consensus/consensus3_5_2.nm"... |
|||
|
|||
Parsing properties file "consensus/consensus3_5_2_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F "one_proc_err" ], P>=0.9879770423 [ G "one_coin_ok" ]) |
|||
|
|||
Type: MDP |
|||
Modules: process1 process2 process3 coin1_error coin2_error coin3_error |
|||
Variables: s1 r1 p1 s2 r2 p2 s3 r3 p3 c1 v1 c2 v2 c3 v3 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F "one_proc_err" ], P>=0.9879770423 [ G "one_coin_ok" ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.41 seconds (average 0.008180, setup 0.00) |
|||
|
|||
Time for model construction: 0.64 seconds. |
|||
|
|||
Type: MDP |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 39636 nodes (2 terminal), 487456 minterms, vars: 33r/33c/40nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.016 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.52 seconds (average 0.010440, setup 0.00) |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 43778 nodes (2 terminal), 487456 minterms, vars: 34r/34c/40nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 50 iterations in 0.47 seconds (average 0.009460, setup 0.00) |
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 46178 nodes (2 terminal), 487456 minterms, vars: 35r/35c/40nd |
|||
|
|||
States: 181129 (1 initial) |
|||
Transitions: 487456 |
|||
Choices: 487456 |
|||
|
|||
Transition matrix: 46178 nodes (2 terminal), 487456 minterms, vars: 35r/35c/40nd |
|||
|
|||
Finding accepting end components for F "one_proc_err"... |
|||
Time for end component identification: 0.018 seconds. |
|||
|
|||
Finding accepting end components for G "one_coin_ok"... |
|||
Time for end component identification: 0.01 seconds. |
|||
|
|||
Prob0A: 24 iterations in 0.43 seconds (average 0.018125, setup 0.00) |
|||
|
|||
yes = 1416, no = 29808, maybe = 149905 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 39 iterations in 0.61 seconds (average 0.015462, setup 0.01) |
|||
Iterative method: 14 iterations in 0.24 seconds (average 0.017071, setup 0.00) |
|||
Iterative method: 39 iterations in 0.61 seconds (average 0.015641, setup 0.00) |
|||
The value iteration(s) took 2.049 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 2.049 s. |
|||
|
|||
Value in the initial state: 0.012022957700000277 |
|||
|
|||
Time for model checking: 6.751 seconds. |
|||
|
|||
Result: 0.012022957700000277 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:37 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf4.nm zeroconf/zeroconf4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf/zeroconf4.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.07 seconds (average 0.000603, setup 0.00) |
|||
|
|||
Time for model construction: 0.148 seconds. |
|||
|
|||
Type: MDP |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 2515 nodes (4 terminal), 17152 minterms, vars: 36r/36c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.015 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.06 seconds (average 0.000500, setup 0.00) |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 2604 nodes (4 terminal), 17152 minterms, vars: 37r/37c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.001 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 116 iterations in 0.07 seconds (average 0.000647, setup 0.00) |
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 3754 nodes (4 terminal), 17152 minterms, vars: 38r/38c/7nd |
|||
|
|||
States: 5449 (1 initial) |
|||
Transitions: 17152 |
|||
Choices: 16487 |
|||
|
|||
Transition matrix: 3754 nodes (4 terminal), 17152 minterms, vars: 38r/38c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.031 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.051 seconds. |
|||
|
|||
Prob0A: 82 iterations in 0.03 seconds (average 0.000354, setup 0.00) |
|||
|
|||
yes = 4813, no = 172, maybe = 464 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 85 iterations in 0.03 seconds (average 0.000306, setup 0.00) |
|||
Iterative method: 85 iterations in 0.03 seconds (average 0.000318, setup 0.00) |
|||
The value iteration(s) took 0.096 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.096 s. |
|||
|
|||
Value in the initial state: 3.075787401574803E-4 |
|||
|
|||
Time for model checking: 3.519 seconds. |
|||
|
|||
Result: 3.075787401574803E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,97 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:42 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf6.nm zeroconf/zeroconf6_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf/zeroconf6.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf6_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.9997523901 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error6 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 c5 c6 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.9997523901 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.10 seconds (average 0.000820, setup 0.00) |
|||
|
|||
Time for model construction: 0.183 seconds. |
|||
|
|||
Type: MDP |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 3238 nodes (4 terminal), 32003 minterms, vars: 40r/40c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.09 seconds (average 0.000703, setup 0.00) |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 3325 nodes (4 terminal), 32003 minterms, vars: 41r/41c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 128 iterations in 0.12 seconds (average 0.000922, setup 0.00) |
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 4445 nodes (4 terminal), 32003 minterms, vars: 42r/42c/7nd |
|||
|
|||
States: 10543 (1 initial) |
|||
Transitions: 32003 |
|||
Choices: 31008 |
|||
|
|||
Transition matrix: 4445 nodes (4 terminal), 32003 minterms, vars: 42r/42c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.069 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.075 seconds. |
|||
|
|||
Prob0A: 88 iterations in 0.04 seconds (average 0.000398, setup 0.00) |
|||
|
|||
yes = 9673, no = 238, maybe = 632 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 91 iterations in 0.05 seconds (average 0.000582, setup 0.00) |
|||
Iterative method: 91 iterations in 0.05 seconds (average 0.000549, setup 0.00) |
|||
Iterative method: 91 iterations in 0.05 seconds (average 0.000582, setup 0.00) |
|||
Iterative method: 91 iterations in 0.06 seconds (average 0.000637, setup 0.00) |
|||
The value iteration(s) took 0.269 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.269 s. |
|||
|
|||
Value in the initial state: 2.476283452671333E-4 |
|||
|
|||
Time for model checking: 7.973 seconds. |
|||
|
|||
Result: 2.476283452671333E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,97 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:34:53 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf/zeroconf8.nm zeroconf/zeroconf8_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf/zeroconf8.nm"... |
|||
|
|||
Parsing properties file "zeroconf/zeroconf8_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F l=4&ip=1 ], P>=0.9999910613 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error8 |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 c5 c6 c7 c8 error |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F l=4&ip=1 ], P>=0.9999910613 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.16 seconds (average 0.001164, setup 0.00) |
|||
|
|||
Time for model construction: 0.24 seconds. |
|||
|
|||
Type: MDP |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 4321 nodes (4 terminal), 52163 minterms, vars: 46r/46c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.14 seconds (average 0.000993, setup 0.00) |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 4412 nodes (4 terminal), 52163 minterms, vars: 47r/47c/7nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 140 iterations in 0.19 seconds (average 0.001386, setup 0.00) |
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 5586 nodes (4 terminal), 52163 minterms, vars: 48r/48c/7nd |
|||
|
|||
States: 17221 (1 initial) |
|||
Transitions: 52163 |
|||
Choices: 50838 |
|||
|
|||
Transition matrix: 5586 nodes (4 terminal), 52163 minterms, vars: 48r/48c/7nd |
|||
|
|||
Finding accepting end components for F l=4&ip=1... |
|||
Time for end component identification: 0.136 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.155 seconds. |
|||
|
|||
Prob0A: 94 iterations in 0.05 seconds (average 0.000511, setup 0.00) |
|||
|
|||
yes = 16117, no = 304, maybe = 800 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 97 iterations in 0.10 seconds (average 0.001021, setup 0.00) |
|||
Iterative method: 97 iterations in 0.09 seconds (average 0.000887, setup 0.00) |
|||
Iterative method: 97 iterations in 0.09 seconds (average 0.000959, setup 0.00) |
|||
Iterative method: 97 iterations in 0.09 seconds (average 0.000969, setup 0.00) |
|||
The value iteration(s) took 0.469 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.469 s. |
|||
|
|||
Value in the initial state: 9.030555331603746E-6 |
|||
|
|||
Time for model checking: 14.675 seconds. |
|||
|
|||
Result: 9.030555331603746E-6 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:35:10 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb2_14.nm zeroconf-tb/zeroconf-tb2_14_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb2_14.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb2_14_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.81 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error2 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.81 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.27 seconds (average 0.002103, setup 0.00) |
|||
|
|||
Time for model construction: 0.336 seconds. |
|||
|
|||
Type: MDP |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 9057 nodes (4 terminal), 92605 minterms, vars: 36r/36c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.33 seconds (average 0.002611, setup 0.00) |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 10373 nodes (4 terminal), 92605 minterms, vars: 37r/37c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 126 iterations in 0.39 seconds (average 0.003127, setup 0.00) |
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 14230 nodes (4 terminal), 92605 minterms, vars: 38r/38c/8nd |
|||
|
|||
States: 29572 (1 initial) |
|||
Transitions: 92605 |
|||
Choices: 86585 |
|||
|
|||
Transition matrix: 14230 nodes (4 terminal), 92605 minterms, vars: 38r/38c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.191 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.225 seconds. |
|||
|
|||
Prob0A: 20 iterations in 0.05 seconds (average 0.002300, setup 0.00) |
|||
|
|||
yes = 23767, no = 3321, maybe = 2484 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 34 iterations in 0.06 seconds (average 0.001794, setup 0.00) |
|||
Iterative method: 34 iterations in 0.06 seconds (average 0.001588, setup 0.00) |
|||
Iterative method: 34 iterations in 0.06 seconds (average 0.001794, setup 0.00) |
|||
The value iteration(s) took 0.239 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.239 s. |
|||
|
|||
Value in the initial state: 8.059348391417451E-8 |
|||
|
|||
Time for model checking: 30.265 seconds. |
|||
|
|||
Result: 8.059348391417451E-8 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:35:42 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb4_10.nm zeroconf-tb/zeroconf-tb4_10_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb4_10.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb4_10_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.21 seconds (average 0.001656, setup 0.00) |
|||
|
|||
Time for model construction: 0.286 seconds. |
|||
|
|||
Type: MDP |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 9893 nodes (4 terminal), 63353 minterms, vars: 42r/42c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.24 seconds (average 0.001952, setup 0.00) |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 11570 nodes (4 terminal), 63353 minterms, vars: 43r/43c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 125 iterations in 0.23 seconds (average 0.001848, setup 0.00) |
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 14283 nodes (4 terminal), 63353 minterms, vars: 44r/44c/8nd |
|||
|
|||
States: 19670 (1 initial) |
|||
Transitions: 63353 |
|||
Choices: 59358 |
|||
|
|||
Transition matrix: 14283 nodes (4 terminal), 63353 minterms, vars: 44r/44c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.157 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.147 seconds. |
|||
|
|||
Prob0A: 6 iterations in 0.02 seconds (average 0.003167, setup 0.00) |
|||
|
|||
yes = 17645, no = 902, maybe = 1123 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 22 iterations in 0.03 seconds (average 0.001182, setup 0.00) |
|||
Iterative method: 22 iterations in 0.03 seconds (average 0.001182, setup 0.00) |
|||
The value iteration(s) took 0.133 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.133 s. |
|||
|
|||
Value in the initial state: 0.33353838582677153 |
|||
|
|||
Time for model checking: 27.184 seconds. |
|||
|
|||
Result: 0.33353838582677153 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:36:12 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism zeroconf-tb/zeroconf-tb4_14.nm zeroconf-tb/zeroconf-tb4_14_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "zeroconf-tb/zeroconf-tb4_14.nm"... |
|||
|
|||
Parsing properties file "zeroconf-tb/zeroconf-tb4_14_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Type: MDP |
|||
Modules: host0 env_error4 time_error |
|||
Variables: x y coll probes mess defend ip l env k c1 c2 c3 c4 error time_error done t |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F time_error=1 ], P>=0.993141 [ G (error=0) ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.39 seconds (average 0.002977, setup 0.00) |
|||
|
|||
Time for model construction: 0.478 seconds. |
|||
|
|||
Type: MDP |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 14874 nodes (4 terminal), 138025 minterms, vars: 42r/42c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.50 seconds (average 0.003765, setup 0.00) |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 16458 nodes (4 terminal), 138025 minterms, vars: 43r/43c/8nd |
|||
|
|||
Building deterministic Rabin automaton (for G "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 132 iterations in 0.48 seconds (average 0.003644, setup 0.00) |
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 19902 nodes (4 terminal), 138025 minterms, vars: 44r/44c/8nd |
|||
|
|||
States: 42968 (1 initial) |
|||
Transitions: 138025 |
|||
Choices: 130735 |
|||
|
|||
Transition matrix: 19902 nodes (4 terminal), 138025 minterms, vars: 44r/44c/8nd |
|||
|
|||
Finding accepting end components for F time_error=1... |
|||
Time for end component identification: 0.318 seconds. |
|||
|
|||
Finding accepting end components for G (error=0)... |
|||
Time for end component identification: 0.341 seconds. |
|||
|
|||
Prob0A: 12 iterations in 0.04 seconds (average 0.003250, setup 0.00) |
|||
|
|||
yes = 38966, no = 1353, maybe = 2649 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 28 iterations in 0.08 seconds (average 0.002893, setup 0.00) |
|||
Iterative method: 28 iterations in 0.08 seconds (average 0.002714, setup 0.00) |
|||
The value iteration(s) took 0.267 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 0.267 s. |
|||
|
|||
Value in the initial state: 3.075787401574803E-4 |
|||
|
|||
Time for model checking: 74.546 seconds. |
|||
|
|||
Result: 3.075787401574803E-4 (value in the initial state) |
|||
|
|||
@ -0,0 +1,81 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:37:29 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_3.nm team/team2obj_3_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team2obj_3.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_3_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.003231, setup 0.00) |
|||
|
|||
Time for model construction: 0.159 seconds. |
|||
|
|||
Type: MDP |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 16500 nodes (4 terminal), 15228 minterms, vars: 24r/24c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.021 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.03 seconds (average 0.002538, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.015 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.04 seconds (average 0.003273, setup 0.00) |
|||
|
|||
yes = 546, no = 0, maybe = 11929 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000643, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000643, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000643, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000714, setup 0.00) |
|||
The value iteration(s) took 0.129 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 0.13 s. |
|||
|
|||
Value in the initial state: 0.8714285710612256 |
|||
|
|||
Time for model checking: 10.362 seconds. |
|||
|
|||
Result: 0.8714285710612256 (value in the initial state) |
|||
|
|||
@ -0,0 +1,81 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:37:57 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_4.nm team/team2obj_4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team2obj_4.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.35 seconds (average 0.022000, setup 0.00) |
|||
|
|||
Time for model construction: 0.985 seconds. |
|||
|
|||
Type: MDP |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 101788 nodes (4 terminal), 116464 minterms, vars: 36r/36c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.32 seconds (average 0.020063, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.171 seconds. |
|||
|
|||
Prob0A: 13 iterations in 0.33 seconds (average 0.025308, setup 0.00) |
|||
|
|||
yes = 4872, no = 0, maybe = 91793 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005118, setup 0.01) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005059, setup 0.00) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.005000, setup 0.00) |
|||
Iterative method: 17 iterations in 0.09 seconds (average 0.004882, setup 0.00) |
|||
The value iteration(s) took 1.056 seconds altogether. |
|||
Number of weight vectors used: 4 |
|||
Multi-objective value iterations took 1.058 s. |
|||
|
|||
Value in the initial state: 0.9438775507764041 |
|||
|
|||
Time for model checking: 237.397 seconds. |
|||
|
|||
Result: 0.9438775507764041 (value in the initial state) |
|||
|
|||
@ -0,0 +1,79 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:47:17 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team2obj_5.nm team/team2obj_5_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team2obj_5.nm"... |
|||
|
|||
Parsing properties file "team/team2obj_5_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 sensor5 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 state5 m5_t1 m5_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.39 seconds (average 0.073368, setup 0.00) |
|||
|
|||
Time for model construction: 4.464 seconds. |
|||
|
|||
Type: MDP |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 361071 nodes (4 terminal), 1084752 minterms, vars: 40r/40c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.012 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.32 seconds (average 0.069474, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 1.631 seconds. |
|||
|
|||
Prob0A: 15 iterations in 1.45 seconds (average 0.096667, setup 0.00) |
|||
|
|||
yes = 52200, no = 0, maybe = 855793 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 1.03 seconds (average 0.050450, setup 0.02) |
|||
Iterative method: 20 iterations in 1.01 seconds (average 0.049500, setup 0.02) |
|||
The value iteration(s) took 4.642 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 4.642 s. |
|||
|
|||
Value in the initial state: 1.0 |
|||
|
|||
Time for model checking: 7024.324 seconds. |
|||
|
|||
Result: 1.0 (value in the initial state) |
|||
|
|||
@ -0,0 +1,96 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:37:42 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_3.nm team/team3obj_3_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team3obj_3.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_3_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.003077, setup 0.00) |
|||
|
|||
Time for model construction: 0.16 seconds. |
|||
|
|||
Type: MDP |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 16500 nodes (4 terminal), 15228 minterms, vars: 24r/24c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.014 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.04 seconds (average 0.002846, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 17753 nodes (4 terminal), 15228 minterms, vars: 25r/25c/10nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.001 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.03 seconds (average 0.002308, setup 0.00) |
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 21624 nodes (4 terminal), 15228 minterms, vars: 26r/26c/10nd |
|||
|
|||
States: 12475 (1 initial) |
|||
Transitions: 15228 |
|||
Choices: 14935 |
|||
|
|||
Transition matrix: 21624 nodes (4 terminal), 15228 minterms, vars: 26r/26c/10nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.021 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 0.01 seconds. |
|||
|
|||
Prob0A: 11 iterations in 0.07 seconds (average 0.006545, setup 0.00) |
|||
|
|||
yes = 1020, no = 0, maybe = 11455 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000857, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.000714, setup 0.00) |
|||
Iterative method: 14 iterations in 0.01 seconds (average 0.001071, setup 0.00) |
|||
The value iteration(s) took 0.123 seconds altogether. |
|||
Number of weight vectors used: 3 |
|||
Multi-objective value iterations took 0.123 s. |
|||
|
|||
Value in the initial state: 0.7448979591841851 |
|||
|
|||
Time for model checking: 12.811 seconds. |
|||
|
|||
Result: 0.7448979591841851 (value in the initial state) |
|||
|
|||
@ -0,0 +1,98 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Sun Jun 12 16:41:57 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_4.nm team/team3obj_4_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team3obj_4.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_4_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.33 seconds (average 0.020500, setup 0.00) |
|||
|
|||
Time for model construction: 0.958 seconds. |
|||
|
|||
Type: MDP |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 101788 nodes (4 terminal), 116464 minterms, vars: 36r/36c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.013 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.32 seconds (average 0.019750, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 109827 nodes (4 terminal), 116464 minterms, vars: 37r/37c/13nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 16 iterations in 0.36 seconds (average 0.022437, setup 0.00) |
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 130439 nodes (4 terminal), 116464 minterms, vars: 38r/38c/13nd |
|||
|
|||
States: 96665 (1 initial) |
|||
Transitions: 116464 |
|||
Choices: 115289 |
|||
|
|||
Transition matrix: 130439 nodes (4 terminal), 116464 minterms, vars: 38r/38c/13nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 0.135 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 0.083 seconds. |
|||
|
|||
Prob0A: 13 iterations in 0.52 seconds (average 0.039846, setup 0.00) |
|||
|
|||
yes = 8784, no = 0, maybe = 87881 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 17 iterations in 0.11 seconds (average 0.005882, setup 0.01) |
|||
Iterative method: 17 iterations in 0.10 seconds (average 0.005882, setup 0.00) |
|||
Iterative method: 17 iterations in 0.10 seconds (average 0.006000, setup 0.00) |
|||
Iterative method: 17 iterations in 0.10 seconds (average 0.006000, setup 0.00) |
|||
Iterative method: 17 iterations in 0.11 seconds (average 0.006235, setup 0.00) |
|||
The value iteration(s) took 1.195 seconds altogether. |
|||
Number of weight vectors used: 5 |
|||
Multi-objective value iterations took 1.195 s. |
|||
|
|||
Value in the initial state: 0.9285714285727903 |
|||
|
|||
Time for model checking: 316.672 seconds. |
|||
|
|||
Result: 0.9285714285727903 (value in the initial state) |
|||
|
|||
@ -0,0 +1,95 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 09:16:24 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism team/team3obj_5.nm team/team3obj_5_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "team/team3obj_5.nm"... |
|||
|
|||
Parsing properties file "team/team3obj_5_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Type: MDP |
|||
Modules: controller sensor1 sensor2 sensor3 sensor4 sensor5 |
|||
Variables: status t1_r1 t1_r2 t1_r3 t2_r1 t2_r2 t2_r3 turn1 turn2 turn3 turn4 turn5 state1 m1_t1 m1_t2 state2 m2_t1 m2_t2 state3 m3_t1 m3_t2 state4 m4_t1 m4_t2 state5 m5_t1 m5_t2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ], P>=0.5 [ F task2_completed ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.42 seconds (average 0.074737, setup 0.00) |
|||
|
|||
Time for model construction: 4.426 seconds. |
|||
|
|||
Type: MDP |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 361071 nodes (4 terminal), 1084752 minterms, vars: 40r/40c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.02 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.32 seconds (average 0.069579, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 388712 nodes (4 terminal), 1084752 minterms, vars: 41r/41c/16nd |
|||
|
|||
Building deterministic Rabin automaton (for F "L0")... |
|||
Taking deterministic Rabin automaton from library... |
|||
DRA has 2 states, , 1 Rabin pairs.Time for Rabin translation: 0.0 seconds. |
|||
|
|||
Constructing MDP-DRA product... |
|||
|
|||
Reachability (BFS): 19 iterations in 1.24 seconds (average 0.065105, setup 0.00) |
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 449699 nodes (4 terminal), 1084752 minterms, vars: 42r/42c/16nd |
|||
|
|||
States: 907993 (1 initial) |
|||
Transitions: 1084752 |
|||
Choices: 1078873 |
|||
|
|||
Transition matrix: 449699 nodes (4 terminal), 1084752 minterms, vars: 42r/42c/16nd |
|||
|
|||
Finding accepting end components for F task1_completed... |
|||
Time for end component identification: 1.892 seconds. |
|||
|
|||
Finding accepting end components for F task2_completed... |
|||
Time for end component identification: 1.139 seconds. |
|||
|
|||
Prob0A: 15 iterations in 2.55 seconds (average 0.169867, setup 0.00) |
|||
|
|||
yes = 90960, no = 0, maybe = 817033 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 20 iterations in 1.27 seconds (average 0.062050, setup 0.03) |
|||
Iterative method: 20 iterations in 1.25 seconds (average 0.061150, setup 0.03) |
|||
The value iteration(s) took 5.736 seconds altogether. |
|||
Number of weight vectors used: 2 |
|||
Multi-objective value iterations took 5.736 s. |
|||
|
|||
Value in the initial state: 1.0 |
|||
|
|||
Time for model checking: 9760.251 seconds. |
|||
|
|||
Result: 1.0 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 11:59:12 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler05.nm scheduler/scheduler05_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "scheduler/scheduler05.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler05_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 99 iterations in 0.34 seconds (average 0.003384, setup 0.00) |
|||
|
|||
Time for model construction: 0.409 seconds. |
|||
|
|||
Type: MDP |
|||
States: 31965 (1 initial) |
|||
Transitions: 60434 |
|||
Choices: 57965 |
|||
|
|||
Transition matrix: 7870 nodes (5 terminal), 60434 minterms, vars: 30r/30c/10nd |
|||
|
|||
States: 31965 (1 initial) |
|||
Transitions: 60434 |
|||
Choices: 57965 |
|||
|
|||
Transition matrix: 7870 nodes (5 terminal), 60434 minterms, vars: 30r/30c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.002000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 31965 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 132 iterations in 0.24 seconds (average 0.001788, setup 0.00) |
|||
Iterative method: 131 iterations in 0.32 seconds (average 0.002420, setup 0.00) |
|||
Iterative method: 223 iterations in 0.55 seconds (average 0.002475, setup 0.00) |
|||
Iterative method: 193 iterations in 0.47 seconds (average 0.002461, setup 0.00) |
|||
Iterative method: 141 iterations in 0.34 seconds (average 0.002411, setup 0.00) |
|||
Iterative method: 126 iterations in 0.32 seconds (average 0.002516, setup 0.00) |
|||
Iterative method: 128 iterations in 0.32 seconds (average 0.002500, setup 0.00) |
|||
Iterative method: 125 iterations in 0.31 seconds (average 0.002440, setup 0.00) |
|||
The value iteration(s) took 2.967 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 2.967 s. |
|||
|
|||
Value in the initial state: 16.169598765430386 |
|||
|
|||
Time for model checking: 3.429 seconds. |
|||
|
|||
Result: 16.169598765430386 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 11:59:18 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler25.nm scheduler/scheduler25_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "scheduler/scheduler25.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler25_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 419 iterations in 6.66 seconds (average 0.015897, setup 0.00) |
|||
|
|||
Time for model construction: 6.846 seconds. |
|||
|
|||
Type: MDP |
|||
States: 633735 (1 initial) |
|||
Transitions: 1179444 |
|||
Choices: 1168375 |
|||
|
|||
Transition matrix: 25430 nodes (5 terminal), 1179444 minterms, vars: 35r/35c/10nd |
|||
|
|||
States: 633735 (1 initial) |
|||
Transitions: 1179444 |
|||
Choices: 1168375 |
|||
|
|||
Transition matrix: 25430 nodes (5 terminal), 1179444 minterms, vars: 35r/35c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.01 seconds (average 0.007000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 633735 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 552 iterations in 20.71 seconds (average 0.037500, setup 0.01) |
|||
Iterative method: 551 iterations in 29.07 seconds (average 0.052735, setup 0.01) |
|||
Iterative method: 1033 iterations in 54.54 seconds (average 0.052791, setup 0.01) |
|||
Iterative method: 879 iterations in 46.18 seconds (average 0.052523, setup 0.01) |
|||
Iterative method: 594 iterations in 30.94 seconds (average 0.052079, setup 0.01) |
|||
Iterative method: 524 iterations in 27.22 seconds (average 0.051926, setup 0.01) |
|||
Iterative method: 541 iterations in 28.16 seconds (average 0.052035, setup 0.01) |
|||
Iterative method: 542 iterations in 29.42 seconds (average 0.054264, setup 0.01) |
|||
The value iteration(s) took 270.237 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 270.237 s. |
|||
|
|||
Value in the initial state: 15.81452325633229 |
|||
|
|||
Time for model checking: 275.779 seconds. |
|||
|
|||
Result: 15.81452325633229 (value in the initial state) |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:04:02 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism scheduler/scheduler50.nm scheduler/scheduler50_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "scheduler/scheduler50.nm"... |
|||
|
|||
Parsing properties file "scheduler/scheduler50_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Type: MDP |
|||
Modules: scheduler P1 P2 |
|||
Variables: task1 task2 task3 task4 task5 task6 p1 c1 x1 p2 c2 x2 |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"time"}min=? [ C ], R{"energy"}<=1.45 [ C ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 819 iterations in 26.33 seconds (average 0.032154, setup 0.00) |
|||
|
|||
Time for model construction: 26.732 seconds. |
|||
|
|||
Type: MDP |
|||
States: 2457510 (1 initial) |
|||
Transitions: 4564394 |
|||
Choices: 4542575 |
|||
|
|||
Transition matrix: 45541 nodes (5 terminal), 4564394 minterms, vars: 37r/37c/10nd |
|||
|
|||
States: 2457510 (1 initial) |
|||
Transitions: 4564394 |
|||
Choices: 4542575 |
|||
|
|||
Transition matrix: 45541 nodes (5 terminal), 4564394 minterms, vars: 37r/37c/10nd |
|||
|
|||
Prob0A: 1 iterations in 0.01 seconds (average 0.011000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 2457510 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 1077 iterations in 156.35 seconds (average 0.145150, setup 0.02) |
|||
Iterative method: 1076 iterations in 217.65 seconds (average 0.202246, setup 0.04) |
|||
Iterative method: 2045 iterations in 421.85 seconds (average 0.206265, setup 0.04) |
|||
Iterative method: 1715 iterations in 348.82 seconds (average 0.203373, setup 0.03) |
|||
Iterative method: 1163 iterations in 234.00 seconds (average 0.201176, setup 0.03) |
|||
Iterative method: 1028 iterations in 211.41 seconds (average 0.205620, setup 0.03) |
|||
Iterative method: 1058 iterations in 214.38 seconds (average 0.202599, setup 0.03) |
|||
Iterative method: 1059 iterations in 212.69 seconds (average 0.200815, setup 0.03) |
|||
The value iteration(s) took 2036.128 seconds altogether. |
|||
Number of weight vectors used: 8 |
|||
Multi-objective value iterations took 2036.128 s. |
|||
|
|||
Value in the initial state: 15.773985890650346 |
|||
|
|||
Time for model checking: 2055.074 seconds. |
|||
|
|||
Result: 15.773985890650346 (value in the initial state) |
|||
|
|||
@ -0,0 +1,67 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:38:46 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm100.nm dpm/dpm100_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "dpm/dpm100.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm100_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000077, setup 0.00) |
|||
|
|||
Time for model construction: 0.034 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000059, setup 0.00) |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000088, setup 0.00) |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000108, setup 0.00) |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000088, setup 0.00) |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000078, setup 0.00) |
|||
Iterative method: 102 iterations in 0.01 seconds (average 0.000078, setup 0.00) |
|||
The value iteration(s) took 0.066 seconds altogether. |
|||
Number of weight vectors used: 6 |
|||
Multi-objective value iterations took 0.066 s. |
|||
|
|||
Value in the initial state: 121.61288420945114 |
|||
|
|||
Time for model checking: 0.082 seconds. |
|||
|
|||
Result: 121.61288420945114 (value in the initial state) |
|||
|
|||
@ -0,0 +1,66 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:38:49 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm200.nm dpm/dpm200_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "dpm/dpm200.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm200_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=200 ], R{"queue"}<=170 [ C<=200 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=200 ], R{"queue"}<=170 [ C<=200 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000077, setup 0.00) |
|||
|
|||
Time for model construction: 0.03 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 202 iterations in 0.01 seconds (average 0.000064, setup 0.00) |
|||
Iterative method: 202 iterations in 0.02 seconds (average 0.000084, setup 0.00) |
|||
Iterative method: 202 iterations in 0.02 seconds (average 0.000099, setup 0.00) |
|||
Iterative method: 202 iterations in 0.02 seconds (average 0.000084, setup 0.00) |
|||
Iterative method: 202 iterations in 0.02 seconds (average 0.000084, setup 0.00) |
|||
The value iteration(s) took 0.098 seconds altogether. |
|||
Number of weight vectors used: 5 |
|||
Multi-objective value iterations took 0.098 s. |
|||
|
|||
Value in the initial state: 57.463619566549646 |
|||
|
|||
Time for model checking: 0.112 seconds. |
|||
|
|||
Result: 57.463619566549646 (value in the initial state) |
|||
|
|||
@ -0,0 +1,66 @@ |
|||
PRISM |
|||
===== |
|||
|
|||
Version: 4.3 |
|||
Date: Mon Jun 13 12:38:52 CEST 2016 |
|||
Hostname: Tims-iMac.fritz.box |
|||
Memory limits: cudd=1g, java(heap)=2.7g |
|||
Command line: prism dpm/dpm300.nm dpm/dpm300_numerical.pctl -epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g |
|||
|
|||
Parsing model file "dpm/dpm300.nm"... |
|||
|
|||
Parsing properties file "dpm/dpm300_numerical.pctl"... |
|||
|
|||
1 property: |
|||
(1) multi(R{"power"}min=? [ C<=300 ], R{"queue"}<=270 [ C<=300 ]) |
|||
|
|||
Type: MDP |
|||
Modules: timer PM SR SP SQ |
|||
Variables: c pm sr sp q |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Model checking: multi(R{"power"}min=? [ C<=300 ], R{"queue"}<=270 [ C<=300 ]) |
|||
|
|||
Building model... |
|||
|
|||
Computing reachable states... |
|||
|
|||
Reachability (BFS): 13 iterations in 0.00 seconds (average 0.000154, setup 0.00) |
|||
|
|||
Time for model construction: 0.031 seconds. |
|||
|
|||
Type: MDP |
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
States: 636 (1 initial) |
|||
Transitions: 2550 |
|||
Choices: 1860 |
|||
|
|||
Transition matrix: 772 nodes (30 terminal), 2550 minterms, vars: 11r/11c/5nd |
|||
|
|||
Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) |
|||
|
|||
yes = 0, no = 0, maybe = 636 |
|||
|
|||
Computing remaining probabilities... |
|||
Engine: Sparse |
|||
Iterative method: 302 iterations in 0.02 seconds (average 0.000063, setup 0.00) |
|||
Iterative method: 302 iterations in 0.03 seconds (average 0.000083, setup 0.00) |
|||
Iterative method: 302 iterations in 0.03 seconds (average 0.000096, setup 0.00) |
|||
Iterative method: 302 iterations in 0.03 seconds (average 0.000083, setup 0.00) |
|||
Iterative method: 302 iterations in 0.03 seconds (average 0.000083, setup 0.00) |
|||
The value iteration(s) took 0.136 seconds altogether. |
|||
Number of weight vectors used: 5 |
|||
Multi-objective value iterations took 0.136 s. |
|||
|
|||
Value in the initial state: 46.48477803835034 |
|||
|
|||
Time for model checking: 0.15 seconds. |
|||
|
|||
Result: 46.48477803835034 (value in the initial state) |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue