PRISM

Benchmark
Model:crowds v.1 (DTMC)
Parameter(s)TotalRuns = 6, CrowdSize = 20
Property:positive (prob-reach)
Invocation (specific)
./fix-syntax ./prism --javamaxmem 11g crowds.prism crowds.props --property positive -const TotalRuns=6,CrowdSize=20 -mtbdd
Select best engine
Execution
Walltime:12.383137702941895s
Return code:0
Relative Error:9.929700521031815e-06
Log
PRISM
=====

Version: 4.4.dev
Date: Mon Dec 10 19:55:03 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g crowds.prism crowds.props --property positive -const 'TotalRuns=6,CrowdSize=20' -mtbdd

Parsing model file "crowds.prism"...

Parsing properties file "crowds.props"...

1 property:
(1) "positive": P=? [ F observe0>1 ]

Type:        DTMC
Modules:     crowds 
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19 

---------------------------------------------------------------------

Model checking: "positive": P=? [ F observe0>1 ]
Model constants: TotalRuns=6,CrowdSize=20

Building model...
Model constants: TotalRuns=6,CrowdSize=20

Warning: Guard for command 6 of module "crowds" is never satisfied.

Warning: Guard for command 7 of module "crowds" is never satisfied.

Warning: Guard for command 8 of module "crowds" is never satisfied.

Warning: Guard for command 9 of module "crowds" is never satisfied.

Warning: Guard for command 10 of module "crowds" is never satisfied.

Warning: Guard for command 2 of module "crowds" overlaps with previous commands.

Warning: Guard for command 3 of module "crowds" overlaps with previous commands.

Warning: Guard for command 4 of module "crowds" overlaps with previous commands.

Warning: Guard for command 5 of module "crowds" overlaps with previous commands.

Warning: Guard for command 11 of module "crowds" overlaps with previous commands.

Warning: Guard for command 12 of module "crowds" overlaps with previous commands.

Warning: Guard for command 13 of module "crowds" overlaps with previous commands.

Warning: Guard for command 14 of module "crowds" overlaps with previous commands.

Warning: Guard for command 15 of module "crowds" overlaps with previous commands.

Warning: Guard for command 16 of module "crowds" overlaps with previous commands.

Warning: Guard for command 17 of module "crowds" overlaps with previous commands.

Warning: Guard for command 18 of module "crowds" overlaps with previous commands.

Warning: Guard for command 19 of module "crowds" overlaps with previous commands.

Warning: Guard for command 20 of module "crowds" overlaps with previous commands.

Warning: Guard for command 21 of module "crowds" overlaps with previous commands.

Warning: Guard for command 22 of module "crowds" overlaps with previous commands.

Warning: Guard for command 23 of module "crowds" overlaps with previous commands.

Warning: Guard for command 24 of module "crowds" overlaps with previous commands.

Warning: Guard for command 25 of module "crowds" overlaps with previous commands.

Warning: Guard for command 26 of module "crowds" overlaps with previous commands.

Warning: Guard for command 27 of module "crowds" overlaps with previous commands.

Warning: Guard for command 28 of module "crowds" overlaps with previous commands.

Warning: Guard for command 29 of module "crowds" overlaps with previous commands.

Warning: Guard for command 30 of module "crowds" overlaps with previous commands.

Warning: Guard for command 31 of module "crowds" overlaps with previous commands.

Warning: Guard for command 32 of module "crowds" overlaps with previous commands.

Warning: Guard for command 33 of module "crowds" overlaps with previous commands.

Computing reachable states...

Reachability (BFS): 56 iterations in 0.29 seconds (average 0.005232, setup 0.00)

Time for model construction: 0.489 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Transition matrix: 40814 nodes (7 terminal), 38261191 minterms, vars: 78r/78c

Prob0: 14 iterations in 0.15 seconds (average 0.010857, setup 0.00)

Prob1: 37 iterations in 0.19 seconds (average 0.005162, setup 0.00)

yes = 363561, no = 8587502, maybe = 1682528

Computing remaining probabilities...
Engine: MTBDD

Iteration matrix MTBDD... [nodes=27895] [544.8 Kb]
Diagonals MTBDD... [nodes=9679] [189.0 Kb]

Starting iterations...
Iteration 103: 5.02 sec so far
Iteration 194: 10.06 sec so far

Jacobi: 206 iterations in 10.73 seconds (average 0.051995, setup 0.02)

Value in the initial state: 0.12047517459031551

Time for model checking: 11.087 seconds.

Result: 0.12047517459031551 (value in the initial state)


Overall running time: 12.14 seconds.

---------------------------------------------------------------------

Note: There were 33 warnings during computation.