PRISM

Benchmark
Model:firewire-pta v.1 (PTA)
Parameter(s)delay = 30, T = 5000
Property:eventually (prob-reach)
Invocation (default)
./fix-syntax ./prism --javamaxmem 11g firewire-pta.prism firewire-pta.props --property eventually -const delay=30,T=5000
Default settings.
Execution
Walltime:0.8681981563568115s
Return code:0
Relative Error:0.0
Log
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.