Log files for model csma.3-4 and tool configuration prism_from-umb_check_ex
[0.257, 0.247, 0.247, 0.687, 0.296]
Log file: prism_from-umb_check_ex_csma.3-4_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 14.251 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:39:13 GMT+02:00 2026
Hostname: n23m0255.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962805/tmpu0rb34diprism_from-umb_check_ex_csma.3-4_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962805/tmpu0rb34diprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [send3] [end1] [end2] [end3] [busy1] [busy2] [busy3] [cd] [time]
Variables: x
Labels: "all_delivered" "collision_max_backoff"
Parsing properties file "/w0/tmp/slurm_tq429871.4962805/tmpu0rb34diprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props"...
1 property:
(1) "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
---------------------------------------------------------------------
Model checking: "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
Building model (engine:explicit)...
Time for model construction: 0.257 seconds.
Type: MDP
States: 1460287 (1 initial)
Transitions: 2396727
Choices: 1471059
Max/avg: 3/1.01
Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 133 iterations and 1.786 seconds.
Starting Prob1 (max)...
Prob1 (max) took 662 iterations and 10.704 seconds.
target=13, yes=710317, no=31622, maybe=718348
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 97 iterations, 141758031 multiplications and 0.724 seconds.
Probabilistic reachability took 13.235 seconds.
Value in the initial state: 0.9324464641692023
Time for model checking: 13.301 seconds.
Result: 0.9324464641692023 (+/- 3.784718669938797E-6 estimated; rel err 4.058912565356696E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_csma.3-4_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 12.958 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:13:56 GMT+02:00 2026
Hostname: r23m0211.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965108/tmp7hcy86zoprism_from-umb_check_ex_csma.3-4_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965108/tmp7hcy86zoprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [send3] [end1] [end2] [end3] [busy1] [busy2] [busy3] [cd] [time]
Variables: x
Labels: "all_delivered" "collision_max_backoff"
Parsing properties file "/w0/tmp/slurm_tq429871.4965108/tmp7hcy86zoprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props"...
1 property:
(1) "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
---------------------------------------------------------------------
Model checking: "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
Building model (engine:explicit)...
Time for model construction: 0.247 seconds.
Type: MDP
States: 1460287 (1 initial)
Transitions: 2396727
Choices: 1471059
Max/avg: 3/1.01
Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 133 iterations and 1.601 seconds.
Starting Prob1 (max)...
Prob1 (max) took 662 iterations and 9.618 seconds.
target=13, yes=710317, no=31622, maybe=718348
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 97 iterations, 141758031 multiplications and 0.714 seconds.
Probabilistic reachability took 11.955 seconds.
Value in the initial state: 0.9324464641692023
Time for model checking: 12.022 seconds.
Result: 0.9324464641692023 (+/- 3.784718669938797E-6 estimated; rel err 4.058912565356696E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_csma.3-4_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 12.611 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:08:41 GMT+02:00 2026
Hostname: r23m0197.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964877/tmpdbcrvy3iprism_from-umb_check_ex_csma.3-4_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964877/tmpdbcrvy3iprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [send3] [end1] [end2] [end3] [busy1] [busy2] [busy3] [cd] [time]
Variables: x
Labels: "all_delivered" "collision_max_backoff"
Parsing properties file "/w0/tmp/slurm_tq429871.4964877/tmpdbcrvy3iprism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props"...
1 property:
(1) "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
---------------------------------------------------------------------
Model checking: "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
Building model (engine:explicit)...
Time for model construction: 0.247 seconds.
Type: MDP
States: 1460287 (1 initial)
Transitions: 2396727
Choices: 1471059
Max/avg: 3/1.01
Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 133 iterations and 1.506 seconds.
Starting Prob1 (max)...
Prob1 (max) took 662 iterations and 9.387 seconds.
target=13, yes=710317, no=31622, maybe=718348
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 97 iterations, 141758031 multiplications and 0.698 seconds.
Probabilistic reachability took 11.61 seconds.
Value in the initial state: 0.9324464641692023
Time for model checking: 11.672 seconds.
Result: 0.9324464641692023 (+/- 3.784718669938797E-6 estimated; rel err 4.058912565356696E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_csma.3-4_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 16.267 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:46:31 GMT+02:00 2026
Hostname: n23m0113.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966770/tmplaxvjhx8prism_from-umb_check_ex_csma.3-4_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966770/tmplaxvjhx8prism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [send3] [end1] [end2] [end3] [busy1] [busy2] [busy3] [cd] [time]
Variables: x
Labels: "all_delivered" "collision_max_backoff"
Parsing properties file "/w0/tmp/slurm_tq429871.4966770/tmplaxvjhx8prism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props"...
1 property:
(1) "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
---------------------------------------------------------------------
Model checking: "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
Building model (engine:explicit)...
Time for model construction: 0.687 seconds.
Type: MDP
States: 1460287 (1 initial)
Transitions: 2396727
Choices: 1471059
Max/avg: 3/1.01
Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 133 iterations and 1.736 seconds.
Starting Prob1 (max)...
Prob1 (max) took 662 iterations and 10.708 seconds.
target=13, yes=710317, no=31622, maybe=718348
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 97 iterations, 141758031 multiplications and 0.729 seconds.
Probabilistic reachability took 13.215 seconds.
Value in the initial state: 0.9324464641692023
Time for model checking: 13.31 seconds.
Result: 0.9324464641692023 (+/- 3.784718669938797E-6 estimated; rel err 4.058912565356696E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_csma.3-4_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 13.955 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:09:13 GMT+02:00 2026
Hostname: n23m0135.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964022/tmpwkg9iem6prism_from-umb_check_ex_csma.3-4_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964022/tmpwkg9iem6prism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [] [send1] [send2] [send3] [end1] [end2] [end3] [busy1] [busy2] [busy3] [cd] [time]
Variables: x
Labels: "all_delivered" "collision_max_backoff"
Parsing properties file "/w0/tmp/slurm_tq429871.4964022/tmpwkg9iem6prism_from-umb_check_ex_csma.3-4_tmp_indir_/property.props"...
1 property:
(1) "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
---------------------------------------------------------------------
Model checking: "all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ]
Building model (engine:explicit)...
Time for model construction: 0.296 seconds.
Type: MDP
States: 1460287 (1 initial)
Transitions: 2396727
Choices: 1471059
Max/avg: 3/1.01
Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 133 iterations and 1.825 seconds.
Starting Prob1 (max)...
Prob1 (max) took 662 iterations and 10.125 seconds.
target=13, yes=710317, no=31622, maybe=718348
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 97 iterations, 141758031 multiplications and 0.797 seconds.
Probabilistic reachability took 12.769 seconds.
Value in the initial state: 0.9324464641692023
Time for model checking: 12.841 seconds.
Result: 0.9324464641692023 (+/- 3.784718669938797E-6 estimated; rel err 4.058912565356696E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g