PRISM
=====
Version: 4.4.dev
Date: Tue Dec 11 01:55:59 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g firewire-pta.prism firewire-pta.props --property deadline -const 'delay=30,T=5000'
Parsing model file "firewire-pta.prism"...
Parsing properties file "firewire-pta.props"...
2 properties:
(1) "deadline": Pmin=? [ F<=T "done" ]
(2) "eventually": Pmin=? [ F "done" ]
Type: PTA
Modules: wire12 node1 wire21 node2
Variables: w12 y1 y2 x1 s1 w21 z1 z2 x2 s2
---------------------------------------------------------------------
Model checking: "deadline": Pmin=? [ F<=T "done" ]
Model constants: delay=30
Property constants: T=5000
Building PTA...
PTA: 6 clocks, 65 locations, 127 transitions
Target (s1=8&s2=7|s1=7&s2=8) satisfied by 4 locations.
Modifying PTA to encode time bound from property...
New PTA: 7 clocks, 66 locations, 135 transitions
Building initial STPG...
Building forwards reachability graph... 3469 states
Graph constructed in 0.162 secs.
Graph: 3469 symbolic states (1 initial, 130 target)
Model checking STPG...
STPG model checked in 0.284 secs.
2634/3469 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.
Refinement 1...
42 states successfully refined in 0.176 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3511 states.
Model checking STPG...
STPG model checked in 0.204 secs.
2718/3511 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
96 refineable states.
Refinement 2...
96 states successfully refined in 0.295 secs.
288+0=288 states of STPG rebuilt in 0.0 secs.
New STPG has 3607 states.
Model checking STPG...
STPG model checked in 0.169 secs.
2910/3607 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
36 refineable states.
Refinement 3...
36 states successfully refined in 0.084 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 3643 states.
Model checking STPG...
STPG model checked in 0.119 secs.
2982/3643 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.
Refinement 4...
60 states successfully refined in 0.111 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3703 states.
Model checking STPG...
STPG model checked in 0.124 secs.
3102/3703 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.
Refinement 5...
60 states successfully refined in 0.124 secs.
162+0=162 states of STPG rebuilt in 0.0 secs.
New STPG has 3763 states.
Model checking STPG...
STPG model checked in 0.083 secs.
3222/3763 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.
Refinement 6...
42 states successfully refined in 0.084 secs.
108+0=108 states of STPG rebuilt in 0.0 secs.
New STPG has 3805 states.
Model checking STPG...
STPG model checked in 0.065 secs.
3306/3805 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
24 refineable states.
Refinement 7...
24 states successfully refined in 0.041 secs.
75+0=75 states of STPG rebuilt in 0.0 secs.
New STPG has 3829 states.
Model checking STPG...
STPG model checked in 0.061 secs.
3354/3829 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
27 refineable states.
Refinement 8...
27 states successfully refined in 0.065 secs.
66+0=66 states of STPG rebuilt in 0.0 secs.
New STPG has 3856 states.
Model checking STPG...
STPG model checked in 0.061 secs.
3408/3856 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
12 refineable states.
Refinement 9...
12 states successfully refined in 0.037 secs.
42+0=42 states of STPG rebuilt in 0.0 secs.
New STPG has 3880 states.
Model checking STPG...
STPG model checked in 0.059 secs.
3444/3880 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
6 refineable states.
Refinement 10...
6 states successfully refined in 0.075 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 3892 states.
Model checking STPG...
STPG model checked in 0.064 secs.
3462/3892 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 11...
40 states successfully refined in 0.253 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 3972 states.
Model checking STPG...
STPG model checked in 0.074 secs.
3582/3972 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 12...
40 states successfully refined in 0.288 secs.
144+0=144 states of STPG rebuilt in 0.0 secs.
New STPG has 4036 states.
Model checking STPG...
STPG model checked in 0.071 secs.
3686/4036 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 13...
40 states successfully refined in 0.157 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 4100 states.
Model checking STPG...
STPG model checked in 0.079 secs.
3790/4100 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
28 refineable states.
Refinement 14...
28 states successfully refined in 0.116 secs.
88+0=88 states of STPG rebuilt in 0.0 secs.
New STPG has 4144 states.
Model checking STPG...
STPG model checked in 0.079 secs.
3862/4144 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.25
16 refineable states.
Refinement 15...
16 states successfully refined in 0.072 secs.
60+0=60 states of STPG rebuilt in 0.0 secs.
New STPG has 4168 states.
Model checking STPG...
STPG model checked in 0.075 secs.
3902/4168 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.25
20 refineable states.
Refinement 16...
20 states successfully refined in 0.093 secs.
68+0=68 states of STPG rebuilt in 0.0 secs.
New STPG has 4200 states.
Model checking STPG...
STPG model checked in 0.088 secs.
3950/4200 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.15625
16 refineable states.
Refinement 17...
16 states successfully refined in 0.056 secs.
52+0=52 states of STPG rebuilt in 0.0 secs.
New STPG has 4228 states.
Model checking STPG...
STPG model checked in 0.093 secs.
3974/4228 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
8 refineable states.
Refinement 18...
6 states successfully refined in 0.084 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 4240 states.
Model checking STPG...
STPG model checked in 0.077 secs.
3986/4240 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
44 refineable states.
Refinement 19...
40 states successfully refined in 0.199 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 4320 states.
Model checking STPG...
STPG model checked in 0.086 secs.
4175/4320 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.
Refinement 20...
10 states successfully refined in 0.064 secs.
36+0=36 states of STPG rebuilt in 0.0 secs.
New STPG has 4336 states.
Model checking STPG...
STPG model checked in 0.085 secs.
4201/4336 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.
Refinement 21...
10 states successfully refined in 0.038 secs.
33+0=33 states of STPG rebuilt in 0.0 secs.
New STPG has 4352 states.
Model checking STPG...
STPG model checked in 0.126 secs.
4227/4352 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
23 refineable states.
Refinement 22...
7 states successfully refined in 0.026 secs.
22+0=22 states of STPG rebuilt in 0.0 secs.
New STPG has 4363 states.
Model checking STPG...
STPG model checked in 0.132 secs.
4245/4363 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.0625
20 refineable states.
Refinement 23...
4 states successfully refined in 0.013 secs.
16+0=16 states of STPG rebuilt in 0.0 secs.
New STPG has 4369 states.
Model checking STPG...
STPG model checked in 0.119 secs.
4332/4369 states converged.
Diff across 1 initial state: 0.0
Lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625
Initial STPG: 3469 states (1 initial), 4982 transitions, 4620 choices, 3423 choice sets, p1max/avg = 3/0.99, p2max/avg = 2/1.35
Final STPG: 4369 states (1 initial), 8212 transitions, 7674 choices, 4756 choice sets, p1max/avg = 7/1.09, p2max/avg = 6/1.61
Terminated after 23 refinements in 5.86 secs.
Abstraction-refinement time breakdown:
* 0.79 secs (13.5%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (23 x avg 0.00 secs)
* 2.48 secs (42.2%) = model checking STPG (24 x avg 0.10 secs) (lb=45.8%) (prob0=18.4%) (pre=94.0%) (iters=964)
* 2.55 secs (43.5%) = refinement (23 x avg 0.11 secs)
Final diff across 1 initial state: 0.0
Final lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625
Model checking completed in 6.01 secs.
Result (minimum probability): 0.8515625
Overall running time: 6.383 seconds.