Storm.exact

Benchmark
Model:bitcoin-attack v.1 (MA)
Parameter(s)MALICIOUS = 20, CD = 6
Property:P_MWinMax (prob-reach-time-bounded)
Invocation (exact)
/home/tq429871/storm/build/bin/storm --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/bitcoin-attack/bitcoin-attack.jani --janiproperty P_MWinMax --constants MALICIOUS=20,CD=6 --exact --timemem
Sparse engine with exact model checking
Execution
Walltime:0.0855560302734375s
Return code:0
Note(s):Unable to obtain tool result.
Log
Storm 1.6.2

Date: Sat Sep  5 21:02:57 2020
Command line arguments: --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/bitcoin-attack/bitcoin-attack.jani --janiproperty P_MWinMax --constants 'MALICIOUS=20,CD=6' --exact --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.001s.

 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.018s.

-------------------------------------------------------------- 
Model type: 	Markov Automaton (sparse)
States: 	177
Transitions: 	284
Choices: 	227
Markovian St.: 	63
Max. Rate.: 	1
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * ((m_len >= 6) & (m_diff > 0)) -> 6 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Time for model preprocessing: 0.000s.

-------------------------------------------------------------- 
Model type: 	Markov Automaton (sparse)
States: 	177
Transitions: 	284
Choices: 	227
Markovian St.: 	63
Max. Rate.: 	1
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * ((m_len >= 6) & (m_diff > 0)) -> 6 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "P_MWinMax": Pmax=? [true U<=2880 ((m_len >= 6) & (m_diff > 0))] ...
ERROR (model-handling.h:847): Property is unsupported by selected engine/settings.


Performance statistics:
  * peak memory usage: 31MB
  * CPU time: 0.046s
  * wallclock time: 0.021s