Storm

Benchmark
Model:wlan-large v.1 (PTA)
Parameter(s)K = 2
Property:P_max (prob-reach)
Invocation (default)
mono modest/moconv.exe wlan-large.jani --digital-clocks  --unroll-distrs --output converted_wlan-large.jani --overwrite --experiment K=2
~/storm/build/bin/storm --jani converted_wlan-large.jani --janiproperty P_max
Default settings. Use moconv to convert the PTA to an MDP using digital-clocks semantics.
Execution
Walltime:46.141990423202515s
Return code:0, 0
Relative Error:0.0
Log
Storm 1.3.1 (dev)

Date: Wed Jan  2 13:31:57 2019
Command line arguments: --jani converted_wlan-large.jani --janiproperty P_max
Current working directory: /home/qcomp

Time for model input parsing: 0.041s.

Time for model construction: 44.002s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	3283371
Transitions: 	6221633
Choices: 	6200795
Reward Models:  none
State Labels: 	4 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * (bc1 = 2) -> 2496014 item(s)
   * (bc2 = 2) -> 2496014 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "P_max": Pmax=? [F ((bc1 = 2) | (bc2 = 2))] ...
Result (for initial states): 0.0625
Time for model checking: 1.335s.