/home/tq429871/storm/build/bin/storm --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/mapk_cascade/mapk_cascade.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/mapk_cascade/mapk_cascade.props reactions --constants N=4,T=30 --prismcompat --engine dd --sylvan:maxmem 4096 --sylvan:threads 4 --timemem --precision 0.001
Symbolic engine with Sylvan using 4GB memory Use `--prismcompat` to ensure compatibility with prism benchmark.
Storm 1.6.2
Date: Sat Sep 5 21:06:00 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/mapk_cascade/mapk_cascade.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/mapk_cascade/mapk_cascade.props reactions --constants 'N=4,T=30' --prismcompat --engine dd '--sylvan:maxmem' 4096 '--sylvan:threads' 4 --timemem --precision 0.001
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks
WARN (Program.cpp:178): The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Time for model input parsing: 0.006s.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1277): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
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.554s.
--------------------------------------------------------------
Model type: CTMC (symbolic)
States: 99535 (4377 nodes)
Transitions: 910872 (111563 nodes)
Reward Models: reactions
Variables: rows: 22 meta variables (58 DD variables), columns: 22 meta variables (58 DD variables)
Labels: 2
* deadlock -> 0 state(s) (1 nodes)
* init -> 1 state(s) (59 nodes)
--------------------------------------------------------------
Model checking property "reactions": R[exp]{"reactions"}=? [C<=30] ...
ERROR (verification.h:425): The model type CTMC is not supported by the dd engine.
WARN (model-handling.h:885): Cannot handle property: NotSupportedException: The model type CTMC is not supported by the dd engine.
ERROR (model-handling.h:847): Property is unsupported by selected engine/settings.
Performance statistics:
* peak memory usage: 2878MB
* CPU time: 1.679s
* wallclock time: 0.581s