PRISM
=====

Version: 4.8.1
Date: Mon Oct 21 08:49:32 CEST 2024
Hostname: thomasLaptop
Memory limits: cudd=1g, java(heap)=1g

Type:        DTMC
Modules:     die
Variables:   s d

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

Model checking: P=? [ F s=7&d=x ]
Property constants: x=3

Building model...

Computing reachable states...

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

Time for model construction: 0.028 seconds.

Type:        DTMC
States:      13 (1 initial)
Transitions: 20

Transition matrix: 71 nodes (3 terminal), 20 minterms, vars: 6r/6c

Prob0: 4 iterations in 0.00 seconds (average 0.000000, setup 0.00)

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

yes = 1, no = 8, maybe = 4

Computing remaining probabilities...
Engine: Hybrid

Building hybrid MTBDD matrix... [levels=6, nodes=41] [1.9 KB]
Adding explicit sparse matrices... [levels=6, num=1, compact] [0.1 KB]
Creating vector for diagonals... [dist=1, compact] [0.0 KB]
Creating vector for RHS... [dist=2, compact] [0.0 KB]
Allocating iteration vectors... [2 x 0.1 KB]
TOTAL: [2.3 KB]

Starting iterations...

Jacobi: 22 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Value in the initial state: 0.16666650772094727

Time for model checking: 0.005 seconds.

Result: 0.16666650772094727 (+/- 1.1920928955078125E-6 estimated; rel err 7.1525641942636435E-6)