Storm.exact

Model:	eajs v.1 (MDP)
Parameter(s)	N = 5, energy_capacity = 250, B = 11
Property:	ExpUtil (exp-reward)

storm/build/bin/storm --prism qcomp/benchmarks/mdp/eajs/eajs.5.prism --prop qcomp/benchmarks/mdp/eajs/eajs.props ExpUtil --constants energy_capacity=250,B=11 --exact --timemem

Sparse engine with exact model checking

Walltime:	97.68038487434387s
Return code:	0
Relative Error:	0.0

Storm 1.4.1 (dev)

Date: Fri Dec  6 09:41:10 2019
Command line arguments: --prism qcomp/benchmarks/mdp/eajs/eajs.5.prism --prop qcomp/benchmarks/mdp/eajs/eajs.props ExpUtil --constants 'energy_capacity=250,B=11' --exact --timemem
Current working directory: 

Time for model input parsing: 0.007s.

Time for model construction: 79.878s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	3049471
Transitions: 	6960278
Choices: 	4250853
Reward Models:  utilityLocal
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * (battery_load = 0) -> 13476 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R[exp]{"utilityLocal"}max=? [F (battery_load = 0)] ...
Result (for initial states): 266763997439241350774737/26588814358957503287787 (approx. 10.03294069)
Time for model checking: 16.028s.

Performance statistics:
  * peak memory usage: 3820MB
  * CPU time: 95.227s
  * wallclock time: 97.160s