Log files for model crowds.6-20 and tool configuration prism_from-prism_to-umb-xz_ex
[11708704.0, 11708704.0, 11708668.0, 11708704.0, 11708704.0]
Log file: prism_from-prism_to-umb-xz_ex_crowds.6-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 273.684 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:18:47 GMT+02:00 2026
Hostname: n23m0310.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956918/tmpp__o6fjxprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956918/tmpwkcfpe9hprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956918/tmpp__o6fjxprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism"...
Type: DTMC
Modules: crowds
Actions: []
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 476599 859686 1423250 1721684 2266952 2635930 3065182 3634496 3988000 4204404 4469273 4770996 5241402 5772358 6358512 6917458 7440502 7720560 7979944 8259001 8523238 8790036 9045016 9550866 10603090 10633591 states
Reachable states exploration and model construction done in 75.432 secs.
Sorting reachable states list...
Time for model construction: 82.677 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956918/tmpwkcfpe9hprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz"...
Time for exporting: 190.345 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 11708704 bytes
Log file: prism_from-prism_to-umb-xz_ex_crowds.6-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 236.051 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:07:40 GMT+02:00 2026
Hostname: n23m0043.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956474/tmp9jcizsxtprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956474/tmp8e22luz3prism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956474/tmp9jcizsxtprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism"...
Type: DTMC
Modules: crowds
Actions: []
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 490842 876944 1420636 1688140 2169409 2578080 2930808 3413507 3881961 4093208 4336683 4593747 4949060 5400014 5962444 6492307 7022800 7480260 7726792 7984183 8239260 8412166 8644147 8865279 9085073 9619638 10633591 states
Reachable states exploration and model construction done in 80.932 secs.
Sorting reachable states list...
Time for model construction: 87.78 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956474/tmp8e22luz3prism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz"...
Time for exporting: 147.559 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 11708704 bytes
Log file: prism_from-prism_to-umb-xz_ex_crowds.6-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 271.467 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:46:46 GMT+02:00 2026
Hostname: r23m0209.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957889/tmpve606jlzprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957889/tmpjww0s58uprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957889/tmpve606jlzprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism"...
Type: DTMC
Modules: crowds
Actions: []
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 477552 867573 1417485 1729527 2284549 2641207 3099795 3656061 3994693 4217431 4508444 4867146 5359535 5918861 6529085 7108053 7562054 7838574 8113610 8404127 8682898 8958511 9315327 10183169 10633591 states
Reachable states exploration and model construction done in 73.007 secs.
Sorting reachable states list...
Time for model construction: 80.696 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957889/tmpjww0s58uprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz"...
Time for exporting: 190.036 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 11708668 bytes
Log file: prism_from-prism_to-umb-xz_ex_crowds.6-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 289.831 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:23:55 GMT+02:00 2026
Hostname: n23m0336.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957124/tmpr4ob6nqmprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957124/tmplca3an32prism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957124/tmpr4ob6nqmprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism"...
Type: DTMC
Modules: crowds
Actions: []
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 471789 836569 1346490 1629441 1939124 2452700 2707801 3098326 3632620 3939507 4117675 4322055 4555966 4836750 5257494 5705974 6229070 6749933 7284675 7549426 7766500 7984683 8201759 8413500 8606095 8812935 8961115 9150744 9750511 10633591 states
Reachable states exploration and model construction done in 89.822 secs.
Sorting reachable states list...
Time for model construction: 97.125 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957124/tmplca3an32prism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz"...
Time for exporting: 192.057 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 11708704 bytes
Log file: prism_from-prism_to-umb-xz_ex_crowds.6-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 268.150 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:03:35 GMT+02:00 2026
Hostname: n23m0276.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956294/tmp4q0kaszvprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956294/tmpjdcout9bprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956294/tmp4q0kaszvprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_indir_/model.prism"...
Type: DTMC
Modules: crowds
Actions: []
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 463220 826541 1404318 1716017 2284473 2638346 3059523 3679484 3987291 4218386 4528033 4899161 5404795 5953347 6565237 7146919 7574039 7838057 8121459 8413633 8703766 8972813 9362354 10224687 10633591 states
Reachable states exploration and model construction done in 72.777 secs.
Sorting reachable states list...
Time for model construction: 80.503 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956294/tmpjdcout9bprism_from-prism_to-umb-xz_ex_crowds.6-20_tmp_outdir_/model.umbxz"...
Time for exporting: 187.005 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 11708704 bytes