Log files for model eajs.6-300-13 and tool configuration prism_from-prism_to-umb_ex
[0.72, 1.068, 0.674, 0.692, 0.807]
Log file: prism_from-prism_to-umb_ex_eajs.6-300-13_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 74.844 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:33:24 GMT+02:00 2026
Hostname: n23m0252.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957501/tmp9rv7ndzoprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957501/tmpw9gi9_kpprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957501/tmp9rv7ndzoprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism"...
Type: MDP
Modules: Battery Process_1 Process_2 Resources Process_3 Process_4 Process_6 Process_5
Actions: [tick]
Variables: battery_load failure_1 loc_1 t_1 t_2 loc_2 boost_1 user_1 t_3 loc_3 t_4 loc_4 loc_6 t_6 t_5 loc_5
Labels: "emptyBattery"
Rewards: "utilityLocal"
Building model (engine:explicit)...
Computing reachable states... 328129 671459 1017102 1375552 1709591 2067969 2428041 2783796 3124377 3491620 3852168 4216859 4569452 4953975 5347123 5691777 6085926 6444488 6821192 7190833 7573872 7901694 states
Reachable states exploration and model construction done in 65.639 secs.
Sorting reachable states list...
Time for model construction: 73.347 seconds.
Type: MDP
States: 7901694 (1 initial)
Transitions: 19722777
Choices: 11897412
Max/avg: 12/1.51
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957501/tmpw9gi9_kpprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb"...
Time for exporting: 0.72 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 571122688 bytes
Log file: prism_from-prism_to-umb_ex_eajs.6-300-13_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 73.252 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:23:54 GMT+02:00 2026
Hostname: n23m0265.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957116/tmplj6gnqb6prism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957116/tmpsqxcq6vzprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957116/tmplj6gnqb6prism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism"...
Type: MDP
Modules: Battery Process_1 Process_2 Resources Process_3 Process_4 Process_6 Process_5
Actions: [tick]
Variables: battery_load failure_1 loc_1 t_1 t_2 loc_2 boost_1 user_1 t_3 loc_3 t_4 loc_4 loc_6 t_6 t_5 loc_5
Labels: "emptyBattery"
Rewards: "utilityLocal"
Building model (engine:explicit)...
Computing reachable states... 337285 705097 1069920 1442038 1801627 2193145 2562244 2946032 3326486 3698018 4068626 4456506 4830725 5222968 5603551 5994421 6358477 6743241 7111865 7508089 7892301 7901694 states
Reachable states exploration and model construction done in 63.222 secs.
Sorting reachable states list...
Time for model construction: 71.539 seconds.
Type: MDP
States: 7901694 (1 initial)
Transitions: 19722777
Choices: 11897412
Max/avg: 12/1.51
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957116/tmpsqxcq6vzprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb"...
Time for exporting: 1.068 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 571122688 bytes
Log file: prism_from-prism_to-umb_ex_eajs.6-300-13_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 71.414 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:37:33 GMT+02:00 2026
Hostname: r23m0216.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955248/tmpvtpsdq0tprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955248/tmpncmcfd2cprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955248/tmpvtpsdq0tprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism"...
Type: MDP
Modules: Battery Process_1 Process_2 Resources Process_3 Process_4 Process_6 Process_5
Actions: [tick]
Variables: battery_load failure_1 loc_1 t_1 t_2 loc_2 boost_1 user_1 t_3 loc_3 t_4 loc_4 loc_6 t_6 t_5 loc_5
Labels: "emptyBattery"
Rewards: "utilityLocal"
Building model (engine:explicit)...
Computing reachable states... 345536 714186 1096350 1482331 1844134 2228013 2601176 2992894 3376456 3751157 4129281 4519909 4895518 5282847 5644397 6048716 6419343 6812828 7186359 7584946 7901694 states
Reachable states exploration and model construction done in 62.459 secs.
Sorting reachable states list...
Time for model construction: 70.107 seconds.
Type: MDP
States: 7901694 (1 initial)
Transitions: 19722777
Choices: 11897412
Max/avg: 12/1.51
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955248/tmpncmcfd2cprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb"...
Time for exporting: 0.674 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 571122688 bytes
Log file: prism_from-prism_to-umb_ex_eajs.6-300-13_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 71.157 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:01:15 GMT+02:00 2026
Hostname: r23m0219.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956200/tmppqeya51pprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956200/tmpn52gwbzbprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956200/tmppqeya51pprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism"...
Type: MDP
Modules: Battery Process_1 Process_2 Resources Process_3 Process_4 Process_6 Process_5
Actions: [tick]
Variables: battery_load failure_1 loc_1 t_1 t_2 loc_2 boost_1 user_1 t_3 loc_3 t_4 loc_4 loc_6 t_6 t_5 loc_5
Labels: "emptyBattery"
Rewards: "utilityLocal"
Building model (engine:explicit)...
Computing reachable states... 348169 719795 1093233 1479289 1839200 2227534 2604494 3004616 3393053 3775009 4151296 4532118 4911821 5308388 5673407 6077664 6444145 6840919 7242338 7612083 7901694 states
Reachable states exploration and model construction done in 62.258 secs.
Sorting reachable states list...
Time for model construction: 69.793 seconds.
Type: MDP
States: 7901694 (1 initial)
Transitions: 19722777
Choices: 11897412
Max/avg: 12/1.51
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956200/tmpn52gwbzbprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb"...
Time for exporting: 0.692 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 571122688 bytes
Log file: prism_from-prism_to-umb_ex_eajs.6-300-13_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 73.573 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:39:16 GMT+02:00 2026
Hostname: n23m0237.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955323/tmp1h4pi1w5prism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955323/tmp87ga6qkkprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955323/tmp1h4pi1w5prism_from-prism_to-umb_ex_eajs.6-300-13_tmp_indir_/model.prism"...
Type: MDP
Modules: Battery Process_1 Process_2 Resources Process_3 Process_4 Process_6 Process_5
Actions: [tick]
Variables: battery_load failure_1 loc_1 t_1 t_2 loc_2 boost_1 user_1 t_3 loc_3 t_4 loc_4 loc_6 t_6 t_5 loc_5
Labels: "emptyBattery"
Rewards: "utilityLocal"
Building model (engine:explicit)...
Computing reachable states... 322109 688474 1037070 1398464 1760272 2121711 2460772 2851626 3190750 3541932 3907575 4267647 4637562 5025241 5397589 5789094 6166097 6551760 6922818 7320497 7688522 7901694 states
Reachable states exploration and model construction done in 64.751 secs.
Sorting reachable states list...
Time for model construction: 72.024 seconds.
Type: MDP
States: 7901694 (1 initial)
Transitions: 19722777
Choices: 11897412
Max/avg: 12/1.51
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955323/tmp87ga6qkkprism_from-prism_to-umb_ex_eajs.6-300-13_tmp_outdir_/model.umb"...
Time for exporting: 0.807 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 571122688 bytes