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

Default settings: '--relative-width' = use relative error for sound methods, '-O out.txt Minimal' = write the property results into file out.txt with minimal formatting (will be read by get_result).

Walltime:	218.61161398887634s
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 4432272 states for delay=30, T=5000.

Peak memory usage: 510 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:        38404 states/s
  Time:        116.9 s

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

  + Value iteration
    Final error: 9.53675225901819E-07
    Iterations:  641
    Time:        100.3 s