Log files for model wlan.4-0 and tool configuration prism_from-umb_check_ex
[0.144, 0.11, 0.109, 0.122, 0.114]
Log file: prism_from-umb_check_ex_wlan.4-0_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 7.010 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:18:08 GMT+02:00 2026
Hostname: n23m0237.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965273/tmp34m1i_cjprism_from-umb_check_ex_wlan.4-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965273/tmp34m1i_cjprism_from-umb_check_ex_wlan.4-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.4965273/tmp34m1i_cjprism_from-umb_check_ex_wlan.4-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.144 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 854 iterations and 2.683 seconds.
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 3.321 seconds.
target=1, yes=345000, no=0, maybe=0
Probabilistic reachability took 6.018 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 6.048 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.4-0_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.207 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:40:40 GMT+02:00 2026
Hostname: n23m0111.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966446/tmp_deffpjdprism_from-umb_check_ex_wlan.4-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966446/tmp_deffpjdprism_from-umb_check_ex_wlan.4-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.4966446/tmp_deffpjdprism_from-umb_check_ex_wlan.4-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.11 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 854 iterations and 2.396 seconds.
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 2.979 seconds.
target=1, yes=345000, no=0, maybe=0
Probabilistic reachability took 5.389 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 5.417 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.4-0_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.152 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:52:54 GMT+02:00 2026
Hostname: r23m0204.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4967019/tmp4ph9jvgqprism_from-umb_check_ex_wlan.4-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967019/tmp4ph9jvgqprism_from-umb_check_ex_wlan.4-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.4967019/tmp4ph9jvgqprism_from-umb_check_ex_wlan.4-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.109 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 854 iterations and 2.373 seconds.
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 2.945 seconds.
target=1, yes=345000, no=0, maybe=0
Probabilistic reachability took 5.339 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 5.368 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.4-0_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.789 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:20:18 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 -importmodel /w0/tmp/slurm_tq429871.4961986/tmpr3p0pbvzprism_from-umb_check_ex_wlan.4-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961986/tmpr3p0pbvzprism_from-umb_check_ex_wlan.4-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.4961986/tmpr3p0pbvzprism_from-umb_check_ex_wlan.4-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.122 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 854 iterations and 2.627 seconds.
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 3.255 seconds.
target=1, yes=345000, no=0, maybe=0
Probabilistic reachability took 5.895 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 5.924 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.4-0_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.489 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:23:20 GMT+02:00 2026
Hostname: n23m0259.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965558/tmp65998bhiprism_from-umb_check_ex_wlan.4-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965558/tmp65998bhiprism_from-umb_check_ex_wlan.4-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.4965558/tmp65998bhiprism_from-umb_check_ex_wlan.4-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.114 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Starting probabilistic reachability (min)...
Starting Prob0 (min)...
Prob0 (min) took 854 iterations and 2.516 seconds.
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 3.115 seconds.
target=1, yes=345000, no=0, maybe=0
Probabilistic reachability took 5.644 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 5.673 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g