Log files for model wlan.6-0 and tool configuration prism_from-umb_check_ex
[281.662, 285.589, 276.759, 325.32, 355.564]
Log file: prism_from-umb_check_ex_wlan.6-0_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 281.662 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:53:38 GMT+02:00 2026
Hostname: n23m0125.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964174/tmpt6cl2bvyprism_from-umb_check_ex_wlan.6-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964174/tmpt6cl2bvyprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964174/tmpt6cl2bvyprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 0.616 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 3158 iterations and 123.345 seconds.
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 156.878 seconds.
target=1, yes=5007548, no=0, maybe=0
Probabilistic reachability took 280.248 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 280.432 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.6-0_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 285.589 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:49:37 GMT+02:00 2026
Hostname: n23m0110.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966850/tmpj00afhxkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966850/tmpj00afhxkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4966850/tmpj00afhxkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 0.611 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 3158 iterations and 130.516 seconds.
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 153.659 seconds.
target=1, yes=5007548, no=0, maybe=0
Probabilistic reachability took 284.199 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 284.356 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.6-0_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 276.759 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:16:27 GMT+02:00 2026
Hostname: n23m0107.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4961826/tmpecvb_ugkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961826/tmpecvb_ugkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961826/tmpecvb_ugkprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 0.657 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 3158 iterations and 119.196 seconds.
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 156.06 seconds.
target=1, yes=5007548, no=0, maybe=0
Probabilistic reachability took 275.28 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 275.439 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.6-0_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 325.320 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:03:26 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 -importmodel /w0/tmp/slurm_tq429871.4964641/tmp_dpu9abjprism_from-umb_check_ex_wlan.6-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964641/tmp_dpu9abjprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964641/tmp_dpu9abjprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 0.69 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 3158 iterations and 143.004 seconds.
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 180.702 seconds.
target=1, yes=5007548, no=0, maybe=0
Probabilistic reachability took 323.744 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 323.964 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.6-0_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 355.564 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:18:08 GMT+02:00 2026
Hostname: r23m0213.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965287/tmpl1s01j6fprism_from-umb_check_ex_wlan.6-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965287/tmpl1s01j6fprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [finish1] [finish2] [time]
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965287/tmpl1s01j6fprism_from-umb_check_ex_wlan.6-0_tmp_indir_/property.props"...
1 property:
(1) "sent": P>=1 [ F "target" ]
---------------------------------------------------------------------
Model checking: "sent": P>=1 [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 0.825 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 3158 iterations and 155.879 seconds.
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 197.808 seconds.
target=1, yes=5007548, no=0, maybe=0
Probabilistic reachability took 353.716 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 353.939 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g