Benchmark

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

Parameter(s) | T = 200 |

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

Invocation (specific)

./fix-syntax ./prism --javamaxmem 11g zeroconf-pta.prism zeroconf-pta.props --property deadline -const T=200Use default settings

Execution

Walltime: | 1.169358491897583s |

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:56:58 CET 2018 Hostname: qcomp2019 Memory limits: cudd=1g, java(heap)=1g Command line: prism --javamaxmem 11g zeroconf-pta.prism zeroconf-pta.props --property deadline -const T=200 Parsing model file "zeroconf-pta.prism"... Parsing properties file "zeroconf-pta.props"... 2 properties: (1) "deadline": Pmax=? [ F<=T s=2&ip=2 ] (2) "incorrect": Pmax=? [ F s=2&ip=2 ] Type: PTA Modules: sender environment Variables: s probes ip x e y --------------------------------------------------------------------- Model checking: "deadline": Pmax=? [ F<=T s=2&ip=2 ] Property constants: T=200 Building PTA... PTA: 2 clocks, 23 locations, 26 transitions Target (s=2&ip=2) satisfied by 3 locations. Modifying PTA to encode time bound from property... New PTA: 3 clocks, 24 locations, 33 transitions Building initial STPG... Building forwards reachability graph... 811 states Graph constructed in 0.066 secs. Graph: 811 symbolic states (1 initial, 22 target) Model checking STPG... STPG model checked in 0.063 secs. 747/811 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 1.0 4 refineable states. Refinement 1... 4 states successfully refined in 0.004 secs. 14+0=14 states of STPG rebuilt in 0.0 secs. New STPG has 815 states. Model checking STPG... STPG model checked in 0.021 secs. 755/815 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.19 6 refineable states. Refinement 2... 4 states successfully refined in 0.004 secs. 12+0=12 states of STPG rebuilt in 0.0 secs. New STPG has 819 states. Model checking STPG... STPG model checked in 0.013 secs. 763/819 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.19 4 refineable states. Refinement 3... 4 states successfully refined in 0.003 secs. 12+0=12 states of STPG rebuilt in 0.0 secs. New STPG has 823 states. Model checking STPG... STPG model checked in 0.012 secs. 771/823 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.03610000000000001 4 refineable states. Refinement 4... 4 states successfully refined in 0.003 secs. 14+0=14 states of STPG rebuilt in 0.0 secs. New STPG has 827 states. Model checking STPG... STPG model checked in 0.014 secs. 779/827 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.006859000000000001 6 refineable states. Refinement 5... 4 states successfully refined in 0.004 secs. 12+0=12 states of STPG rebuilt in 0.0 secs. New STPG has 831 states. Model checking STPG... STPG model checked in 0.013 secs. 787/831 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.006859000000000001 4 refineable states. Refinement 6... 4 states successfully refined in 0.002 secs. 10+0=10 states of STPG rebuilt in 0.0 secs. New STPG has 835 states. Model checking STPG... STPG model checked in 0.014 secs. 795/835 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 0.0013032100000000004 2 refineable states. Refinement 7... 2 states successfully refined in 0.002 secs. 6+0=6 states of STPG rebuilt in 0.0 secs. New STPG has 837 states. Model checking STPG... STPG model checked in 0.013 secs. 799/837 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 6.516050000000002E-4 2 refineable states. Refinement 8... 2 states successfully refined in 0.001 secs. 7+0=7 states of STPG rebuilt in 0.0 secs. New STPG has 839 states. Model checking STPG... STPG model checked in 0.014 secs. 803/839 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 6.516050000000002E-4 3 refineable states. Refinement 9... 3 states successfully refined in 0.002 secs. 9+0=9 states of STPG rebuilt in 0.0 secs. New STPG has 842 states. Model checking STPG... STPG model checked in 0.014 secs. 809/842 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 5.864445000000004E-4 3 refineable states. Refinement 10... 3 states successfully refined in 0.003 secs. 10+0=10 states of STPG rebuilt in 0.0 secs. New STPG has 845 states. Model checking STPG... STPG model checked in 0.015 secs. 815/845 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 5.278000499999999E-4 4 refineable states. Refinement 11... 4 states successfully refined in 0.003 secs. 12+0=12 states of STPG rebuilt in 0.0 secs. New STPG has 849 states. Model checking STPG... STPG model checked in 0.015 secs. 823/849 states converged. Diff across 1 initial state: 4.2204046560609214E-5 Lower/upper bounds for 1 initial state: 0.0011793378874436382 - 0.0012215419340042475 Max diff over all states: 3.1404102975000035E-4 4 refineable states. Refinement 12... 3 states successfully refined in 0.003 secs. 10+0=10 states of STPG rebuilt in 0.0 secs. New STPG has 852 states. Model checking STPG... STPG model checked in 0.015 secs. 839/852 states converged. Diff across 1 initial state: 2.5755289952371927E-5 Lower/upper bounds for 1 initial state: 0.0011957866440518755 - 0.0012215419340042475 Max diff over all states: 3.1404102975000035E-4 2 refineable states. Refinement 13... 2 states successfully refined in 0.002 secs. 7+0=7 states of STPG rebuilt in 0.0 secs. New STPG has 854 states. Model checking STPG... STPG model checked in 0.015 secs. 843/854 states converged. Diff across 1 initial state: 2.5755289952371927E-5 Lower/upper bounds for 1 initial state: 0.0011957866440518755 - 0.0012215419340042475 Max diff over all states: 2.3751002250000015E-4 2 refineable states. Refinement 14... 2 states successfully refined in 0.002 secs. 6+0=6 states of STPG rebuilt in 0.0 secs. New STPG has 856 states. Model checking STPG... STPG model checked in 0.014 secs. 846/856 states converged. Diff across 1 initial state: 1.7530911648253175E-5 Lower/upper bounds for 1 initial state: 0.0012040110223559943 - 0.0012215419340042475 Max diff over all states: 2.1375902025000003E-4 2 refineable states. Refinement 15... 1 states successfully refined in 0.001 secs. 3+0=3 states of STPG rebuilt in 0.0 secs. New STPG has 857 states. Model checking STPG... STPG model checked in 0.015 secs. 848/857 states converged. Diff across 1 initial state: 1.7530911648253175E-5 Lower/upper bounds for 1 initial state: 0.0012040110223559943 - 0.0012215419340042475 Max diff over all states: 1.0687951012500001E-4 2 refineable states. Refinement 16... 1 states successfully refined in 0.0 secs. 3+0=3 states of STPG rebuilt in 0.0 secs. New STPG has 858 states. Model checking STPG... STPG model checked in 0.015 secs. 858/858 states converged. Diff across 1 initial state: 0.0 Lower/upper bounds for 1 initial state: 0.0012215419340042475 - 0.0012215419340042475 Initial STPG: 811 states (1 initial), 1192 transitions, 848 choices, 793 choice sets, p1max/avg = 2/0.98, p2max/avg = 2/1.07 Final STPG: 858 states (1 initial), 1307 transitions, 916 choices, 848 choice sets, p1max/avg = 3/0.99, p2max/avg = 3/1.08 Terminated after 16 refinements in 0.51 secs. Abstraction-refinement time breakdown: * 0.15 secs (29.1%) = Building initial STPG * 0.00 secs (0.0%) = Rebuilding STPG (16 x avg 0.00 secs) * 0.30 secs (58.3%) = model checking STPG (17 x avg 0.02 secs) (lb=53.1%) (prob0=27.5%) (pre=89.8%) (iters=404) * 0.04 secs (7.7%) = refinement (16 x avg 0.00 secs) Final diff across 1 initial state: 0.0 Final lower/upper bounds for 1 initial state: 0.0012215419340042475 - 0.0012215419340042475 Model checking completed in 0.57 secs. Result (maximum probability): 0.0012215419340042475 Overall running time: 0.921 seconds.