Benchmark

Model: | firewire-pta v.1 (PTA) |

Parameter(s) | delay = 30, T = 5000 |

Property: | deadline (prob-reach-time-bounded) |

Invocation (specific)

./fix-syntax ./prism --javamaxmem 11g firewire-pta.prism firewire-pta.props --property deadline -const delay=30,T=5000Use default settings

Execution

Walltime: | 6.62687349319458s |

Return code: | 0 |

Note(s): | Correctness of result is not checked because no reference result is available. |

Log

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.