Log files for model crowds.6-20 and tool configuration prism_from-prism_to-tra-xz_ex
[635.593, 593.216, 635.901, 816.16, 787.182]
Log file: prism_from-prism_to-tra-xz_ex_crowds.6-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17
Wallclock time: 728.268 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:30:27 GMT+02:00 2026
Hostname: n23m0287.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957383/tmpkaod8vn7prism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957383/tmp49ztvz_vprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957383/tmpkaod8vn7prism_from-prism_to-tra-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... 490934 871800 1420916 1689906 2167718 2594212 2948488 3446026 3902774 4110463 4342639 4595263 4925097 5360130 5894999 6405934 6911166 7420913 7673421 7917850 8150169 8348491 8577251 8803768 9018617 9358332 10187371 10633591 states
Reachable states exploration and model construction done in 82.78 secs.
Sorting reachable states list...
Time for model construction: 89.997 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4957383/tmp49ztvz_vprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 635.593 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.pexp.xz: Size of output file is 25682516 bytes
Log file: prism_from-prism_to-tra-xz_ex_crowds.6-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17
Wallclock time: 683.918 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:32:24 GMT+02:00 2026
Hostname: n23m0050.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955054/tmphymjzfevprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955054/tmpbx0qodhsprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955054/tmphymjzfevprism_from-prism_to-tra-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... 485537 866051 1408844 1685457 2083574 2584394 2927040 3447952 3907508 4098983 4321649 4580446 4923942 5399960 5965115 6497332 7000625 7468739 7717475 7973246 8216209 8390791 8619680 8809600 9018497 9374873 10201333 10633591 states
Reachable states exploration and model construction done in 81.992 secs.
Sorting reachable states list...
Time for model construction: 88.707 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4955054/tmpbx0qodhsprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 593.216 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.pexp.xz: Size of output file is 25682516 bytes
Log file: prism_from-prism_to-tra-xz_ex_crowds.6-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17
Wallclock time: 728.547 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:40:59 GMT+02:00 2026
Hostname: n23m0144.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955388/tmpkxrsd97cprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955388/tmpk36l72ypprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955388/tmpkxrsd97cprism_from-prism_to-tra-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... 480823 849489 1394612 1668827 2018051 2496295 2824551 3257627 3822391 4002158 4197437 4444901 4687791 5092910 5494846 6058686 6572607 7056086 7468028 7706961 7947547 8195300 8359164 8604650 8825853 9040221 9437037 10203866 10633591 states
Reachable states exploration and model construction done in 84.997 secs.
Sorting reachable states list...
Time for model construction: 91.928 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4955388/tmpk36l72ypprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 635.901 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.pexp.xz: Size of output file is 25682516 bytes
Log file: prism_from-prism_to-tra-xz_ex_crowds.6-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17
Wallclock time: 904.058 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:32:49 GMT+02:00 2026
Hostname: r23m0207.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957484/tmpqcxetx0lprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957484/tmpvh5x5a0bprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957484/tmpqcxetx0lprism_from-prism_to-tra-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... 429944 823741 1392191 1672513 2067245 2579798 2939203 3473957 3905614 4118927 4367589 4635250 5045388 5496706 6029581 6590567 7136065 7522330 7774803 8044945 8306206 8568213 8740877 8990670 9317184 10088086 10633591 states
Reachable states exploration and model construction done in 79.77 secs.
Sorting reachable states list...
Time for model construction: 87.23 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4957484/tmpvh5x5a0bprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 816.16 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.pexp.xz: Size of output file is 25682516 bytes
Log file: prism_from-prism_to-tra-xz_ex_crowds.6-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17
Wallclock time: 873.625 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:54:27 GMT+02:00 2026
Hostname: r23m0212.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958179/tmp_6v9uibvprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958179/tmpudwwodarprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp.xz:format=explicit,states=false,zip=xz,precision=17'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958179/tmp_6v9uibvprism_from-prism_to-tra-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... 474435 843372 1415530 1713425 2155465 2598749 2973126 3557570 3935925 4146070 4388763 4657712 5087330 5519037 6153662 6657105 7184998 7571623 7846476 8114805 8376904 8567419 8823514 9073005 9566836 10633591 states
Reachable states exploration and model construction done in 77.88 secs.
Sorting reachable states list...
Time for model construction: 85.726 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4958179/tmpudwwodarprism_from-prism_to-tra-xz_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 787.182 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.pexp.xz: Size of output file is 25682516 bytes