Log files for model csma.4-2 and tool configuration prism_from-prism_to-umb-xz_ex
[1554644.0, 1546416.0, 1546416.0, 1546416.0, 1550556.0]
Log file: prism_from-prism_to-umb-xz_ex_csma.4-2_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: 15.886 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:18:12 GMT+02:00 2026
Hostname: n23m0033.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956886/tmpde2mg4whprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956886/tmpp1hjd8ejprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956886/tmpde2mg4whprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism"...
Type: MDP
Modules: bus station1 station2 station3 station4
Actions: [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables: b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels: "all_delivered" "collision_max_backoff"
Building model (engine:explicit)...
Computing reachable states... 518655 761962 states
Reachable states exploration and model construction done in 4.429 secs.
Sorting reachable states list...
Time for model construction: 5.189 seconds.
Type: MDP
States: 761962 (1 initial)
Transitions: 1327068
Choices: 825504
Max/avg: 4/1.08
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956886/tmpp1hjd8ejprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz"...
Time for exporting: 10.01 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 1554644 bytes
Log file: prism_from-prism_to-umb-xz_ex_csma.4-2_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: 13.582 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:02:26 GMT+02:00 2026
Hostname: r23m0215.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956240/tmp97yfu8phprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956240/tmp9hrxbmizprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956240/tmp97yfu8phprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism"...
Type: MDP
Modules: bus station1 station2 station3 station4
Actions: [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables: b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels: "all_delivered" "collision_max_backoff"
Building model (engine:explicit)...
Computing reachable states... 608743 761962 states
Reachable states exploration and model construction done in 3.771 secs.
Sorting reachable states list...
Time for model construction: 4.516 seconds.
Type: MDP
States: 761962 (1 initial)
Transitions: 1327068
Choices: 825504
Max/avg: 4/1.08
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956240/tmp9hrxbmizprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz"...
Time for exporting: 8.51 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 1546416 bytes
Log file: prism_from-prism_to-umb-xz_ex_csma.4-2_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: 14.216 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:15:22 GMT+02:00 2026
Hostname: n23m0301.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956746/tmpw52vqvrmprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956746/tmpw9hjdr8zprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956746/tmpw52vqvrmprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism"...
Type: MDP
Modules: bus station1 station2 station3 station4
Actions: [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables: b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels: "all_delivered" "collision_max_backoff"
Building model (engine:explicit)...
Computing reachable states... 572577 761962 states
Reachable states exploration and model construction done in 4.03 secs.
Sorting reachable states list...
Time for model construction: 4.771 seconds.
Type: MDP
States: 761962 (1 initial)
Transitions: 1327068
Choices: 825504
Max/avg: 4/1.08
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956746/tmpw9hjdr8zprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz"...
Time for exporting: 8.866 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 1546416 bytes
Log file: prism_from-prism_to-umb-xz_ex_csma.4-2_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: 15.297 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:13:02 GMT+02:00 2026
Hostname: n23m0048.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956647/tmpe2uwvyjvprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956647/tmpqsd416vlprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956647/tmpe2uwvyjvprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism"...
Type: MDP
Modules: bus station1 station2 station3 station4
Actions: [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables: b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels: "all_delivered" "collision_max_backoff"
Building model (engine:explicit)...
Computing reachable states... 548617 761962 states
Reachable states exploration and model construction done in 4.215 secs.
Sorting reachable states list...
Time for model construction: 4.928 seconds.
Type: MDP
States: 761962 (1 initial)
Transitions: 1327068
Choices: 825504
Max/avg: 4/1.08
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956647/tmpqsd416vlprism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz"...
Time for exporting: 9.761 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 1546416 bytes
Log file: prism_from-prism_to-umb-xz_ex_csma.4-2_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: 15.978 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:51:01 GMT+02:00 2026
Hostname: n23m0047.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958040/tmp2jpzm169prism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958040/tmp4g8dyz04prism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958040/tmp2jpzm169prism_from-prism_to-umb-xz_ex_csma.4-2_tmp_indir_/model.prism"...
Type: MDP
Modules: bus station1 station2 station3 station4
Actions: [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables: b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels: "all_delivered" "collision_max_backoff"
Building model (engine:explicit)...
Computing reachable states... 549093 761962 states
Reachable states exploration and model construction done in 4.491 secs.
Sorting reachable states list...
Time for model construction: 5.253 seconds.
Type: MDP
States: 761962 (1 initial)
Transitions: 1327068
Choices: 825504
Max/avg: 4/1.08
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958040/tmp4g8dyz04prism_from-prism_to-umb-xz_ex_csma.4-2_tmp_outdir_/model.umbxz"...
Time for exporting: 9.96 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 1550556 bytes