Storm.hybrid

Benchmark
Model:firewire v.2 (MDP)
Parameter(s)explicit_timer = False, delay = 36, deadline = 800
Property:deadline (prob-reach-reward-bounded)
Invocation (hybrid)
/home/tq429871/storm/build/bin/storm --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/firewire/firewire.false.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/firewire/firewire.false.props deadline --constants delay=36,deadline=800 --engine hybrid --sylvan:maxmem 4096 --sylvan:threads 4 --timemem
Hybrid engine with Sylvan using 4GB memory
Execution
Walltime:0.8572280406951904s
Return code:0
Note(s):Unable to obtain tool result.
Log
Storm 1.6.2

Date: Sat Sep  5 20:47:57 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/firewire/firewire.false.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/firewire/firewire.false.props deadline --constants 'delay=36,deadline=800' --engine hybrid '--sylvan:maxmem' 4096 '--sylvan:threads' 4 --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.008s.

 WARN (cli.cpp:262): The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties.
Time for model construction: 0.770s.

-------------------------------------------------------------- 
Model type: 	MDP (symbolic)
States: 	212268 (18185 nodes)
Transitions: 	481788 (88920 nodes)
Choices: 	478752
Reward Models:  time
Variables: 	rows: 10 meta variables (56 DD variables), columns: 10 meta variables (56 DD variables), nondeterminism: 14 meta variables (14 DD variables)
Labels: 	3
   * deadlock -> 0 state(s) (1 nodes)
   * init -> 1 state(s) (57 nodes)
   * done
-------------------------------------------------------------- 

Model checking property "deadline": Pmin=? [true Urew{"time"}<=800 (((s1 = 8) & (s2 = 7)) | ((s1 = 7) & (s2 = 8)))] ...
ERROR (model-handling.h:847): Property is unsupported by selected engine/settings.


Performance statistics:
  * peak memory usage: 2880MB
  * CPU time: 2.567s
  * wallclock time: 0.803s