Log files for model wlan.5-0 and tool configuration prism_from-umb_check_ex
[43.324, 43.377, 42.462, 40.702, 41.97]
Log file: prism_from-umb_check_ex_wlan.5-0_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 43.324 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:17:34 GMT+02:00 2026
Hostname: n23m0060.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4961882/tmpdyfcx1joprism_from-umb_check_ex_wlan.5-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961882/tmpdyfcx1joprism_from-umb_check_ex_wlan.5-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.4961882/tmpdyfcx1joprism_from-umb_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)...
Time for model construction: 0.296 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.837 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 23.254 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 42.111 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 42.215 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.5-0_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 43.377 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:30:58 GMT+02:00 2026
Hostname: n23m0049.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962435/tmpyn05x09sprism_from-umb_check_ex_wlan.5-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962435/tmpyn05x09sprism_from-umb_check_ex_wlan.5-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.4962435/tmpyn05x09sprism_from-umb_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)...
Time for model construction: 0.239 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.667 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 23.665 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 42.351 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 42.449 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.5-0_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 42.462 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:27:38 GMT+02:00 2026
Hostname: n23m0049.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962294/tmp64p3t27pprism_from-umb_check_ex_wlan.5-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962294/tmp64p3t27pprism_from-umb_check_ex_wlan.5-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.4962294/tmp64p3t27pprism_from-umb_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)...
Time for model construction: 0.245 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.533 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 22.792 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 41.346 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 41.458 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.5-0_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 40.702 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:13:24 GMT+02:00 2026
Hostname: r23m0202.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965084/tmpoyi3bf3_prism_from-umb_check_ex_wlan.5-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965084/tmpoyi3bf3_prism_from-umb_check_ex_wlan.5-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.4965084/tmpoyi3bf3_prism_from-umb_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)...
Time for model construction: 0.243 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 17.017 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 22.616 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 39.656 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 39.763 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_wlan.5-0_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 41.970 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:30:24 GMT+02:00 2026
Hostname: n23m0248.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962417/tmpj_d080g_prism_from-umb_check_ex_wlan.5-0_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962417/tmpj_d080g_prism_from-umb_check_ex_wlan.5-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.4962417/tmpj_d080g_prism_from-umb_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)...
Time for model construction: 0.226 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.127 seconds.
Starting Prob1 (min)...
Prob1 (min) took 1622 iterations and 22.799 seconds.
target=1, yes=1295218, no=0, maybe=0
Probabilistic reachability took 40.966 seconds.
Property satisfied in 1 of 1 initial states.
Time for model checking: 41.069 seconds.
Result: true
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g