Storm.exact

Benchmark
Model:polling v.1 (CTMC)
Parameter(s)N = 18, T = 16
Property:s1_before_s2 (prob-reach)
Invocation (exact)
storm/build/bin/storm --prism qcomp/benchmarks/ctmc/polling/polling.18.prism --prop qcomp/benchmarks/ctmc/polling/polling.props s1_before_s2 --constants T=16 --prismcompat --exact --timemem
Sparse engine with exact model checking Use `--prismcompat` to ensure compatibility with prism benchmark.
Execution
Walltime:297.1694715023041s
Return code:-9
Log
Storm 1.4.1 (dev)

Date: Fri Dec  6 09:47:21 2019
Command line arguments: --prism qcomp/benchmarks/ctmc/polling/polling.18.prism --prop qcomp/benchmarks/ctmc/polling/polling.props s1_before_s2 --constants T=16 --prismcompat --exact --timemem
Current working directory: 

 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:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): 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:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1250): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.