PRISM
=====
Version: 4.4.dev
Date: Tue Dec 11 01:13:01 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g rabin.10.prism rabin.10.props --property live
Parsing model file "rabin.10.prism"...
Parsing properties file "rabin.10.props"...
1 property:
(1) "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2) ]
Type: MDP
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10
Variables: c b r p1 b1 r1 draw1 p2 b2 r2 draw2 p3 b3 r3 draw3 p4 b4 r4 draw4 p5 b5 r5 draw5 p6 b6 r6 draw6 p7 b7 r7 draw7 p8 b8 r8 draw8 p9 b9 r9 draw9 p10 b10 r10 draw10
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2) ]
Building model...
Computing reachable states...
Reachability (BFS): 42 iterations in 59.10 seconds (average 1.407167, setup 0.00)
Time for model construction: 63.863 seconds.
Type: MDP
States: 358055586147376 (1 initial)
Transitions: 2908346849726720
Choices: 696028935338720
Transition matrix: 894897 nodes (9 terminal), 2908346849726720 minterms, vars: 96r/96c/10nd
Warning: Switching to MTBDD engine, as number of states is too large for Hybrid engine.
Prob0A: 5 iterations in 1.14 seconds (average 0.228800, setup 0.00)
Prob1E: 6 iterations in 0.62 seconds (average 0.103333, setup 0.00)
yes = 358055586147376, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 1.828 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 66.378 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.