mcsta

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

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

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, '--chainopt' = use state chain compression during state space exploration, which tends to work well for PTA and unbounded properties.

Walltime:	155.82286739349365s
Return code:	0
Relative Error:	9.53674316e-07

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 1176142 states for delay=30, T=5000.

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

+ State space exploration
  State size:  18 bytes
  States:      1176142
  Transitions: 2273670
  Branches:    2277702
  Rate:        9967 states/s
  Time:        118.2 s

+ Property eventually
  Probability: 0.999999046325684
  Bounds:      [0.999999046325684, 1]
  Time:        36.5 s

  + Value iteration
    Final error: 9.53675225901819E-07
    Iterations:  662
    Time:        36.5 s