PRISM
=====
Version: 4.4.dev
Date: Tue Dec 11 01:56:06 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g firewire-pta.prism firewire-pta.props --property eventually -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: "eventually": Pmin=? [ F "done" ]
Model constants: delay=30
Building PTA...
PTA: 6 clocks, 65 locations, 127 transitions
Target (s1=8&s2=7|s1=7&s2=8) satisfied by 4 locations.
Building initial STPG...
Building forwards reachability graph... 215 states
Graph constructed in 0.037 secs.
Graph: 215 symbolic states (1 initial, 14 target)
Model checking STPG...
STPG model checked in 0.026 secs.
215/215 states converged.
Diff across 1 initial state: 0.0
Lower/upper bounds for 1 initial state: 1.0 - 1.0
Initial STPG: 215 states (1 initial), 290 transitions, 268 choices, 201 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.33
Final STPG: 215 states (1 initial), 290 transitions, 268 choices, 201 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.33
Terminated after 0 refinements in 0.16 secs.
Abstraction-refinement time breakdown:
* 0.12 secs (76.6%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (0 x avg 0.00 secs)
* 0.03 secs (16.5%) = model checking STPG (1 x avg 0.03 secs) (lb=69.2%) (prob0=53.8%) (pre=88.5%) (iters=2)
* 0.00 secs (0.0%) = refinement (0 x avg 0.00 secs)
Final diff across 1 initial state: 0.0
Final lower/upper bounds for 1 initial state: 1.0 - 1.0
Model checking completed in 0.287 secs.
Result (minimum probability): 1.0
Overall running time: 0.645 seconds.