PRISM

Benchmark
Model:herman v.1 (DTMC)
Parameter(s)N = 15
Property:steps (exp-reward)
Invocation (specific)
./fix-syntax ./prism --javamaxmem 11g herman.15.prism herman.props --property steps -sparse -gs
Select best engine and numerical method
Execution
Walltime:5.5580761432647705s
Return code:0
Relative Error:9.4649282638e-06
Log
PRISM
=====

Version: 4.4.dev
Date: Mon Dec 10 20:31:45 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g herman.15.prism herman.props --property steps -sparse -gs

Parsing model file "herman.15.prism"...

Parsing properties file "herman.props"...

1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")

Type:        DTMC
Modules:     process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 
Variables:   x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 

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

Model checking: "steps": filter(max, R=? [ F "stable" ], "init")

Building model...

Computing reachable states...

Reachability (BFS): 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.027 seconds.

Type:        DTMC
States:      32768 (32768 initial)
Transitions: 14348908

Transition matrix: 810 nodes (9 terminal), 14348908 minterms, vars: 15r/15c

Prob0: 6 iterations in 0.02 seconds (average 0.003667, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

goal = 30, inf = 0, maybe = 32738

Computing remaining rewards...
Engine: Sparse

Building sparse matrix... [n=32768, nnz=14348846, compact] [54.9 MB]
Creating vector for diagonals... [dist=2, compact] [64.0 KB]
Creating vector for RHS... [dist=2, compact] [64.0 KB]
Allocating iteration vector... [256.0 KB]
TOTAL: [55.2 MB]

Starting iterations...

Gauss-Seidel: 132 iterations in 4.66 seconds (average 0.026682, setup 1.14)

Maximum value over states satisfying filter: 33.33301783572454

There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)

Time for model checking: 4.725 seconds.

Result: 33.33301783572454 (maximum value over states satisfying filter)


Overall running time: 5.346 seconds.