Log files for model eajs.6-300-13 and tool configuration storm_from-umb_check_sparse

Parsed values
[0.524, 0.506, 0.514, 0.53, 0.646]
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.754 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)

Date: Tue Oct 13 09:20:13 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965392/tmpbbux1rv7storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965392/tmpbbux1rv7storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments

Time for model construction: 0.524s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	7901694
Transitions: 	19722777
Choices: 	11897412
Reward Models:  utilityLocal
State Labels: 	3 labels
   * emptyBattery -> 28620 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 12.05111082
Time for model checking: 4.370s.

Performance statistics:
  * peak memory usage: 2134MB
  * CPU time: 4.423s
  * wallclock time: 4.920s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 4.936 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)

Date: Tue Oct 13 09:54:32 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4967094/tmpdoicpze3storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4967094/tmpdoicpze3storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments

Time for model construction: 0.506s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	7901694
Transitions: 	19722777
Choices: 	11897412
Reward Models:  utilityLocal
State Labels: 	3 labels
   * emptyBattery -> 28620 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 12.05111082
Time for model checking: 4.376s.

Performance statistics:
  * peak memory usage: 2134MB
  * CPU time: 4.402s
  * wallclock time: 4.906s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.668 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)

Date: Tue Oct 13 09:39:38 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966407/tmp1uh16ob4storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966407/tmp1uh16ob4storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments

Time for model construction: 0.514s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	7901694
Transitions: 	19722777
Choices: 	11897412
Reward Models:  utilityLocal
State Labels: 	3 labels
   * emptyBattery -> 28620 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 12.05111082
Time for model checking: 5.096s.

Performance statistics:
  * peak memory usage: 2134MB
  * CPU time: 5.137s
  * wallclock time: 5.637s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.819 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)

Date: Tue Oct 13 09:49:37 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966843/tmpe3a5s43mstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966843/tmpe3a5s43mstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments

Time for model construction: 0.530s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	7901694
Transitions: 	19722777
Choices: 	11897412
Reward Models:  utilityLocal
State Labels: 	3 labels
   * emptyBattery -> 28620 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 12.05111082
Time for model checking: 5.227s.

Performance statistics:
  * peak memory usage: 2135MB
  * CPU time: 5.283s
  * wallclock time: 5.784s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 6.061 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)

Date: Tue Oct 13 09:32:18 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966069/tmpgvhu1n1hstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966069/tmpgvhu1n1hstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments

Time for model construction: 0.646s.

-------------------------------------------------------------- 
Model type: 	MDP (sparse)
States: 	7901694
Transitions: 	19722777
Choices: 	11897412
Reward Models:  utilityLocal
State Labels: 	3 labels
   * emptyBattery -> 28620 item(s)
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 12.05111082
Time for model checking: 5.223s.

Performance statistics:
  * peak memory usage: 2135MB
  * CPU time: 5.271s
  * wallclock time: 5.903s