Storm.ddbisim

Benchmark
Model:philosophers v.1 (CTMC)
Parameter(s)N = 16, TIME_BOUND = 1
Property:MaxPrReachDeadlockTB (prob-reach-time-bounded)
Invocation (ddbisim)
/home/tq429871/storm/build/bin/storm --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/philosophers/philosophers.16.jani --janiproperty MaxPrReachDeadlockTB --constants TIME_BOUND=1 --engine dd-to-sparse --bisimulation --sylvan:maxmem 4096 --sylvan:threads 4 --timemem --precision 0.001
Symbolic bisimulation with sparse quotient and sylvan using 4GB memory
Execution
Walltime:143.1089916229248s
Return code:0
Relative Error:0.0
Log
Storm 1.6.2

Date: Sat Sep  5 21:01:37 2020
Command line arguments: --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/philosophers/philosophers.16.jani --janiproperty MaxPrReachDeadlockTB --constants TIME_BOUND=1 --engine dd-to-sparse --bisimulation '--sylvan:maxmem' 4096 '--sylvan:threads' 4 --timemem --precision 0.001
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.008s.

Time for model construction: 0.610s.

-------------------------------------------------------------- 
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 -> 0 state(s) (1 nodes)
   * init -> 1 state(s) (66 nodes)
   * deadl
-------------------------------------------------------------- 

Time for model preprocessing: 141.581s.

-------------------------------------------------------------- 
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 -> 0 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "MaxPrReachDeadlockTB": Pmax=? [true U<=1 "deadl"] ...
Result (for initial states): 6.928238934e-05
Time for model checking: 0.833s.

Performance statistics:
  * peak memory usage: 4026MB
  * CPU time: 555.546s
  * wallclock time: 143.052s