Storm.exact

Benchmark
Model:cluster v.1 (CTMC)
Parameter(s)N = 64, T = 2000, t = 20
Property:below_min (exp-reward-time-bounded)
Invocation (exact)
/home/tq429871/storm/build/bin/storm --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/cluster/cluster.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/cluster/cluster.props below_min --constants N=64,T=2000,t=20 --prismcompat --exact --timemem
Sparse engine with exact model checking Use `--prismcompat` to ensure compatibility with prism benchmark.
Execution
Walltime:4.5662782192230225s
Return code:0
Note(s):Unable to obtain tool result.
Log
Storm 1.6.2

Date: Sat Sep  5 21:05:39 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/cluster/cluster.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ctmc/cluster/cluster.props below_min --constants 'N=64,T=2000,t=20' --prismcompat --exact --timemem
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.003s.

 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.
 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 construction: 4.386s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	151060
Transitions: 	733216
Reward Models:  time_not_min
State Labels: 	2 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "below_min": R[exp]{"time_not_min"}=? [C<=2000] ...
ERROR (model-handling.h:847): Property is unsupported by selected engine/settings.


Performance statistics:
  * peak memory usage: 146MB
  * CPU time: 4.419s
  * wallclock time: 4.480s