Storm.ddbisim

Benchmark
Model:philosophers v.1 (CTMC)
Parameter(s)N = 16, TIME_BOUND = 1
Property:MinExpTimeDeadlock (exp-time)
Invocation (ddbisim)
storm/build/bin/storm --jani qcomp/benchmarks/ctmc/philosophers/philosophers.16.jani --janiproperty MinExpTimeDeadlock --constants TIME_BOUND=1 --engine dd --bisimulation --bisimulation:quot sparse --ddlib sylvan --sylvan:maxmem 4096 --sylvan:threads 4 --timemem
Symbolic bisimulation with sparse quotient and sylvan using 4GB memory
Execution
Walltime:144.91897678375244s
Return code:0
Relative Error:1.1675088592935362e-07
Log
Storm 1.4.1 (dev)

Date: Mon Dec  9 13:25:42 2019
Command line arguments: --jani qcomp/benchmarks/ctmc/philosophers/philosophers.16.jani --janiproperty MinExpTimeDeadlock --constants TIME_BOUND=1 --engine dd --bisimulation '--bisimulation:quot' sparse --ddlib sylvan '--sylvan:maxmem' 4096 '--sylvan:threads' 4 --timemem
Current working directory: 

Time for model input parsing: 0.008s.

Time for model construction: 0.620s.

-------------------------------------------------------------- 
Model type: 	CTMC (symbolic)
States: 	1331714 (270 nodes)
Transitions: 	13774113 (2229 nodes)
Reward Models:  none
Variables: 	rows: 65 meta variables (65 DD variables), columns: 65 meta variables (65 DD variables)
Labels: 	3
   * deadlock -> 1 state(s) (66 nodes)
   * init -> 1 state(s) (66 nodes)
   * deadl
-------------------------------------------------------------- 

Time for model preprocessing: 143.857s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	83311
Transitions: 	860723
Reward Models:  none
State Labels: 	4 labels
   * deadl -> 1 item(s)
   * init -> 1 item(s)
   * (((((((((thinking16 < 1) | (fork16 < 1)) | ((wait16 + 1) > 1)) & (((wait1 < 1) | (fork16 < 1)) | ((eating1 + 1) > 1))) & (((((thinking9 + 1) > 1) | ((fork8 + 1) > 1)) | (((fork9 + 1) > 1) | (eating9 < 1))) & (((thinking8 < 1) | (fork8 < 1)) | ((wait8 + 1) > 1)))) & ((((((thinking13 + 1) > 1) | ((fork12 + 1) > 1)) | (((fork13 + 1) > 1) | (eating13 < 1))) & (((thinking4 < 1) | (fork4 < 1)) | ((wait4 + 1) > 1))) & ((((thinking12 < 1) | (fork12 < 1)) | ((wait12 + 1) > 1)) & ((((thinking5 + 1) > 1) | ((fork4 + 1) > 1)) | (((fork5 + 1) > 1) | (eating5 < 1)))))) & (((((((thinking15 + 1) > 1) | ((fork14 + 1) > 1)) | (((fork15 + 1) > 1) | (eating15 < 1))) & (((thinking2 < 1) | (fork2 < 1)) | ((wait2 + 1) > 1))) & ((((thinking10 < 1) | (fork10 < 1)) | ((wait10 + 1) > 1)) & ((((thinking7 + 1) > 1) | ((fork6 + 1) > 1)) | (((fork7 + 1) > 1) | (eating7 < 1))))) & (((((thinking14 < 1) | (fork14 < 1)) | ((wait14 + 1) > 1)) & ((((thinking3 + 1) > 1) | ((fork2 + 1) > 1)) | (((fork3 + 1) > 1) | (eating3 < 1)))) & (((((thinking11 + 1) > 1) | ((fork10 + 1) > 1)) | (((fork11 + 1) > 1) | (eating11 < 1))) & (((thinking6 < 1) | (fork6 < 1)) | ((wait6 + 1) > 1)))))) & ((((((((thinking16 + 1) > 1) | ((fork15 + 1) > 1)) | (((fork16 + 1) > 1) | (eating16 < 1))) & (((thinking1 < 1) | (fork1 < 1)) | ((wait1 + 1) > 1))) & ((((thinking9 < 1) | (fork9 < 1)) | ((wait9 + 1) > 1)) & ((((thinking8 + 1) > 1) | ((fork7 + 1) > 1)) | (((fork8 + 1) > 1) | (eating8 < 1))))) & (((((thinking13 < 1) | (fork13 < 1)) | ((wait13 + 1) > 1)) & ((((thinking4 + 1) > 1) | ((fork3 + 1) > 1)) | (((fork4 + 1) > 1) | (eating4 < 1)))) & (((((thinking12 + 1) > 1) | ((fork11 + 1) > 1)) | (((fork12 + 1) > 1) | (eating12 < 1))) & (((thinking5 < 1) | (fork5 < 1)) | ((wait5 + 1) > 1))))) & ((((((thinking15 < 1) | (fork15 < 1)) | ((wait15 + 1) > 1)) & ((((thinking2 + 1) > 1) | ((fork1 + 1) > 1)) | (((fork2 + 1) > 1) | (eating2 < 1)))) & (((((thinking10 + 1) > 1) | ((fork9 + 1) > 1)) | (((fork10 + 1) > 1) | (eating10 < 1))) & (((thinking7 < 1) | (fork7 < 1)) | ((wait7 + 1) > 1)))) & ((((((thinking14 + 1) > 1) | ((fork13 + 1) > 1)) | (((fork14 + 1) > 1) | (eating14 < 1))) & (((thinking3 < 1) | (fork3 < 1)) | ((wait3 + 1) > 1))) & ((((thinking11 < 1) | (fork11 < 1)) | ((wait11 + 1) > 1)) & ((((thinking6 + 1) > 1) | ((fork5 + 1) > 1)) | (((fork6 + 1) > 1) | (eating6 < 1)))))))) & (((((((wait16 < 1) | (fork15 < 1)) | ((eating16 + 1) > 1)) & ((((thinking1 + 1) > 1) | ((fork16 + 1) > 1)) | (((fork1 + 1) > 1) | (eating1 < 1)))) & ((((wait9 < 1) | (fork8 < 1)) | ((eating9 + 1) > 1)) & (((wait8 < 1) | (fork7 < 1)) | ((eating8 + 1) > 1)))) & (((((wait13 < 1) | (fork12 < 1)) | ((eating13 + 1) > 1)) & (((wait4 < 1) | (fork3 < 1)) | ((eating4 + 1) > 1))) & ((((wait12 < 1) | (fork11 < 1)) | ((eating12 + 1) > 1)) & (((wait5 < 1) | (fork4 < 1)) | ((eating5 + 1) > 1))))) & ((((((wait15 < 1) | (fork14 < 1)) | ((eating15 + 1) > 1)) & (((wait2 < 1) | (fork1 < 1)) | ((eating2 + 1) > 1))) & ((((wait10 < 1) | (fork9 < 1)) | ((eating10 + 1) > 1)) & (((wait7 < 1) | (fork6 < 1)) | ((eating7 + 1) > 1)))) & (((((wait14 < 1) | (fork13 < 1)) | ((eating14 + 1) > 1)) & (((wait3 < 1) | (fork2 < 1)) | ((eating3 + 1) > 1))) & ((((wait11 < 1) | (fork10 < 1)) | ((eating11 + 1) > 1)) & (((wait6 < 1) | (fork5 < 1)) | ((eating6 + 1) > 1))))))) -> 1 item(s)
   * deadlock -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "MinExpTimeDeadlock": T[exp]min=? [F "deadl"] ...
Result (for initial states): 10.78297471
Time for model checking: 0.355s.

Performance statistics:
  * peak memory usage: 4024MB
  * CPU time: 563.850s
  * wallclock time: 144.861s