mcsta

Model:	firewire-pta v.1 (PTA)
Parameter(s)	delay = 30, T = 5000
Property:	deadline (prob-reach-time-bounded)

mono mcsta/mcsta.exe firewire-pta.jani --props deadline -E delay=30,T=5000 --relative-width -O out.txt Minimal --unsafe -S Memory --bounded-alg StateElimination

Settings specific for this benchmark: '--unsafe' = compile model without bounds and assignment checks, '-S Memory' = store all data in memory since the model is small, '--bounded-alg StateElimination' = use state elimination for the reward-bounded property, which tends to work well for PTA and reward-bounded properties.

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

firewire-pta.jani:model: info: firewire-pta is a PTA model.
firewire-pta.jani: info: Need 18 bytes per state.
firewire-pta.jani: info: Explored 4432272 states for delay=30, T=5000.

Peak memory usage: 8461 MB
Analysis results for firewire-pta.jani
Experiment delay=30, T=5000

+ State space exploration
  State size:  18 bytes
  States:      4432272
  Transitions: 5529800
  Branches:    5533832
  Rate:        38213 states/s
  Time:        116.5 s

+ Property deadline
  Probability: 0.8515625
  Bounds:      [0.8515625, 0.8515625]
  CDF:         { (0, 0), ..., (1699, 0), (1700, 0.5), ..., (2579, 0.5), (2580, 0.625), ..., (3399, 0.625), (3400, 0.75), ..., (3459, 0.75), (3460, 0.78125), ..., (4279, 0.78125), (4280, 0.84375), ..., (4339, 0.84375), (4340, 0.8515625), ..., (5000, 0.8515625) }
  Time:        692.9 s

  + State elimination
    States:      4223853
    Transitions: 15865901
    Branches:    43314977
    Time:        111.2 s

  + Value iteration
    Time: 581.7 s