PRISM

Model:	fms v.1 (CTMC)
Parameter(s)	n = 8
Property:	productivity (steady-state-reward)

./fix-syntax ./prism --javamaxmem 11g fms.prism fms.props --property productivity -const n=8 -sparse -bgs

Select best engine and numerical method

Walltime:	90.62909603118896s
Return code:	0
Note(s):	Correctness of result is not checked because no reference result is available.

PRISM
=====

Version: 4.4.dev
Date: Mon Dec 10 21:27:59 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g fms.prism fms.props --property productivity -const n=8 -sparse -bgs

Parsing model file "fms.prism"...

Parsing properties file "fms.props"...

1 property:
(1) "productivity": R{"productivity"}=? [ S ]

Type:        CTMC
Modules:     machine1 machine2 machine3 machine12 
Variables:   P1 P1wM1 P1M1 P1d P1s P1wP2 M1 P2 P2wM2 P2M2 P2s P2wP1 M2 P3 P3M2 P3s P12 P12wM3 P12M3 P12s M3 

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

Model checking: "productivity": R{"productivity"}=? [ S ]
Model constants: n=8

Building model...
Model constants: n=8

Computing reachable states...

Reachability (BFS): 65 iterations in 5.91 seconds (average 0.090846, setup 0.00)

Time for model construction: 6.345 seconds.

Type:        CTMC
States:      4459455 (1 initial)
Transitions: 38533968

Rate matrix: 215250 nodes (84 terminal), 38533968 minterms, vars: 70r/70c

SCCs: 1, BSCCs: 1, non-BSCC states: 0
BSCC sizes: 1:4459455

Computing steady state probabilities for BSCC 1

Computing probabilities...
Engine: Sparse

Building sparse matrix... [n=4459455, nnz=38533968, compact] [151.2 MB]
Creating vector for diagonals... [dist=1070, compact] [8.5 MB]
Allocating iteration vector... [34.0 MB]
TOTAL: [193.8 MB]

Starting iterations...
Iteration 34: max relative diff=0.021984, 5.04 sec so far
Iteration 68: max relative diff=0.001512, 10.08 sec so far
Iteration 102: max relative diff=0.000075, 15.16 sec so far
Iteration 136: max relative diff=0.000004, 20.24 sec so far

Backwards Gauss-Seidel: 151 iterations in 75.66 seconds (average 0.148834, setup 53.18)

BSCC 1 Reward: 116.6246012120582

All states are in BSCCs (so no reachability probabilities computed)

Value in the initial state: 116.6246012120582

Time for model checking: 83.478 seconds.

Result: 116.6246012120582 (value in the initial state)


Overall running time: 90.396 seconds.