Log files for model wlan.5-0 and tool configuration prism_from-prism_check_ex
[7.074, 6.821, 6.004, 6.304, 6.865]
Log file: prism_from-prism_check_ex_wlan.5-0_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 49.737 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:35:22 GMT+02:00 2026
Hostname: n23m0032.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4962636/tmpb5qgl8jxprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962636/tmpb5qgl8jxprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962636/tmpb5qgl8jxprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism"...
Type: MDP
Modules: medium station1 station2
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4962636/tmpb5qgl8jxprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Computing reachable states... 538371 1249234 1295218 states
Reachable states exploration and model construction done in 6.192 secs.
Sorting reachable states list...
Time for model construction: 7.074 seconds.
Type: MDP
States: 1295218 (1 initial)
Transitions: 2929960
Choices: 1646074
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 1622 iterations and 18.719 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 23.126 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 41.89 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 41.951 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_wlan.5-0_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 50.996 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:00:04 GMT+02:00 2026
Hostname: n23m0059.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961139/tmpb605a42fprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961139/tmpb605a42fprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961139/tmpb605a42fprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism"...
Type: MDP
Modules: medium station1 station2
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961139/tmpb605a42fprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Computing reachable states... 559080 1285442 1295218 states
Reachable states exploration and model construction done in 6.042 secs.
Sorting reachable states list...
Time for model construction: 6.821 seconds.
Type: MDP
States: 1295218 (1 initial)
Transitions: 2929960
Choices: 1646074
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 1622 iterations and 18.256 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 22.92 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 41.2 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 41.254 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_wlan.5-0_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 43.495 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:19:41 GMT+02:00 2026
Hostname: r23m0198.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4965366/tmp4tmtnc9kprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965366/tmp4tmtnc9kprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965366/tmp4tmtnc9kprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism"...
Type: MDP
Modules: medium station1 station2
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965366/tmp4tmtnc9kprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Computing reachable states... 640951 1295218 states
Reachable states exploration and model construction done in 5.296 secs.
Sorting reachable states list...
Time for model construction: 6.004 seconds.
Type: MDP
States: 1295218 (1 initial)
Transitions: 2929960
Choices: 1646074
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 1622 iterations and 16.062 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 20.808 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 36.888 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 36.929 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_wlan.5-0_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 42.471 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:04:56 GMT+02:00 2026
Hostname: n23m0120.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961343/tmpzw8b3xm_prism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961343/tmpzw8b3xm_prism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961343/tmpzw8b3xm_prism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism"...
Type: MDP
Modules: medium station1 station2
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961343/tmpzw8b3xm_prism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Computing reachable states... 635360 1295218 states
Reachable states exploration and model construction done in 5.479 secs.
Sorting reachable states list...
Time for model construction: 6.304 seconds.
Type: MDP
States: 1295218 (1 initial)
Transitions: 2929960
Choices: 1646074
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 1622 iterations and 15.718 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 19.77 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 35.506 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 35.553 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_wlan.5-0_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 48.975 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:14:26 GMT+02:00 2026
Hostname: r23m0206.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4965130/tmpmxkzlxorprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965130/tmpmxkzlxorprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965130/tmpmxkzlxorprism_from-prism_check_ex_wlan.5-0_tmp_indir_/model.prism"...
Type: MDP
Modules: medium station1 station2
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965130/tmpmxkzlxorprism_from-prism_check_ex_wlan.5-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Computing reachable states... 557110 1280171 1295218 states
Reachable states exploration and model construction done in 6.061 secs.
Sorting reachable states list...
Time for model construction: 6.865 seconds.
Type: MDP
States: 1295218 (1 initial)
Transitions: 2929960
Choices: 1646074
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 1622 iterations and 18.411 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 22.946 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 41.378 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 41.435 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g