Storm 1.3.1 (dev)
Date: Thu Dec 13 01:04:33 2018
Command line arguments: --jani echoring.jani --janiproperty MaxOffline1 --constants ITERATIONS=100
Current working directory: /home/qcomp
Time for model input parsing: 0.052s.
Time for model construction: 86.754s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 4741485
Transitions: 8510787
Choices: 7698426
Reward Models: none
State Labels: 6 labels
* deadlock -> 32227 item(s)
* is_offline_3 -> 71004 item(s)
* is_offline_2 -> 150987 item(s)
* init -> 1 item(s)
* (iter <= 100) -> 4694220 item(s)
* is_offline_1 -> 96460 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "MaxOffline1": Pmax=? [F (((is_offline_1 & !(is_offline_2)) & !(is_offline_3)) & (iter <= 100))] ...
Result (for initial states): 1.05008302e-06
Time for model checking: 5.958s.