[15.914, 22.088, 19.345, 16.246, 18.33]

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 15.914 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:23:19 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 /w0/tmp/slurm_tq429871.4965562/tmp5a99b4m_prism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965562/tmp5a99b4m_prism_from-prism_check_ex_csma.4-2_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965562/tmp5a99b4m_prism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism"...

Type:        MDP
Modules:     bus station1 station2 station3 station4
Actions:     [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables:   b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels:      "all_delivered" "collision_max_backoff"

Parsing properties file "/w0/tmp/slurm_tq429871.4965562/tmp5a99b4m_prism_from-prism_check_ex_csma.4-2_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)...

Computing reachable states... 625445 761962 states
Reachable states exploration and model construction done in 3.63 secs.
Sorting reachable states list...

Time for model construction: 4.367 seconds.

Type:        MDP
States:      761962 (1 initial)
Transitions: 1327068
Choices:     825504
Max/avg:     4/1.08

Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 186 iterations and 1.111 seconds.
Starting Prob1 (max)...
Prob1 (max) took 1197 iterations and 8.567 seconds.
target=9, yes=142601, no=25408, maybe=593953
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 172 iterations, 190125188 multiplications and 1.188 seconds.
Probabilistic reachability took 10.88 seconds.

Value in the initial state: 0.776459404375732

Time for model checking: 10.918 seconds.

Result: 0.776459404375732 (+/- 6.170079467349154E-6 estimated; rel err 7.946428921560754E-6)


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 22.088 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:29:44 GMT+02:00 2026
Hostname: n23m0186.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4965936/tmph5b3bp1eprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965936/tmph5b3bp1eprism_from-prism_check_ex_csma.4-2_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965936/tmph5b3bp1eprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism"...

Type:        MDP
Modules:     bus station1 station2 station3 station4
Actions:     [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables:   b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels:      "all_delivered" "collision_max_backoff"

Parsing properties file "/w0/tmp/slurm_tq429871.4965936/tmph5b3bp1eprism_from-prism_check_ex_csma.4-2_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)...

Computing reachable states... 518313 761962 states
Reachable states exploration and model construction done in 4.424 secs.
Sorting reachable states list...

Time for model construction: 5.579 seconds.

Type:        MDP
States:      761962 (1 initial)
Transitions: 1327068
Choices:     825504
Max/avg:     4/1.08

Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 186 iterations and 1.474 seconds.
Starting Prob1 (max)...
Prob1 (max) took 1197 iterations and 11.266 seconds.
target=9, yes=142601, no=25408, maybe=593953
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 172 iterations, 190125188 multiplications and 1.381 seconds.
Probabilistic reachability took 14.142 seconds.

Value in the initial state: 0.776459404375732

Time for model checking: 14.19 seconds.

Result: 0.776459404375732 (+/- 6.170079467349154E-6 estimated; rel err 7.946428921560754E-6)


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 19.345 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:32:04 GMT+02:00 2026
Hostname: n23m0058.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4962486/tmp4vzd20euprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962486/tmp4vzd20euprism_from-prism_check_ex_csma.4-2_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962486/tmp4vzd20euprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism"...

Type:        MDP
Modules:     bus station1 station2 station3 station4
Actions:     [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables:   b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels:      "all_delivered" "collision_max_backoff"

Parsing properties file "/w0/tmp/slurm_tq429871.4962486/tmp4vzd20euprism_from-prism_check_ex_csma.4-2_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)...

Computing reachable states... 549733 761962 states
Reachable states exploration and model construction done in 4.281 secs.
Sorting reachable states list...

Time for model construction: 5.002 seconds.

Type:        MDP
States:      761962 (1 initial)
Transitions: 1327068
Choices:     825504
Max/avg:     4/1.08

Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 186 iterations and 1.408 seconds.
Starting Prob1 (max)...
Prob1 (max) took 1197 iterations and 10.713 seconds.
target=9, yes=142601, no=25408, maybe=593953
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 172 iterations, 190125188 multiplications and 1.424 seconds.
Probabilistic reachability took 13.563 seconds.

Value in the initial state: 0.776459404375732

Time for model checking: 13.604 seconds.

Result: 0.776459404375732 (+/- 6.170079467349154E-6 estimated; rel err 7.946428921560754E-6)


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 16.246 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:59:20 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 /w0/tmp/slurm_tq429871.4967312/tmp8yu4_56aprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4967312/tmp8yu4_56aprism_from-prism_check_ex_csma.4-2_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4967312/tmp8yu4_56aprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism"...

Type:        MDP
Modules:     bus station1 station2 station3 station4
Actions:     [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables:   b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels:      "all_delivered" "collision_max_backoff"

Parsing properties file "/w0/tmp/slurm_tq429871.4967312/tmp8yu4_56aprism_from-prism_check_ex_csma.4-2_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)...

Computing reachable states... 659609 761962 states
Reachable states exploration and model construction done in 3.459 secs.
Sorting reachable states list...

Time for model construction: 4.165 seconds.

Type:        MDP
States:      761962 (1 initial)
Transitions: 1327068
Choices:     825504
Max/avg:     4/1.08

Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 186 iterations and 1.205 seconds.
Starting Prob1 (max)...
Prob1 (max) took 1197 iterations and 9.177 seconds.
target=9, yes=142601, no=25408, maybe=593953
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 172 iterations, 190125188 multiplications and 1.114 seconds.
Probabilistic reachability took 11.511 seconds.

Value in the initial state: 0.776459404375732

Time for model checking: 11.545 seconds.

Result: 0.776459404375732 (+/- 6.170079467349154E-6 estimated; rel err 7.946428921560754E-6)


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 18.330 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:30:11 GMT+02:00 2026
Hostname: n23m0186.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4965958/tmp5efn48_aprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965958/tmp5efn48_aprism_from-prism_check_ex_csma.4-2_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965958/tmp5efn48_aprism_from-prism_check_ex_csma.4-2_tmp_indir_/model.prism"...

Type:        MDP
Modules:     bus station1 station2 station3 station4
Actions:     [] [send1] [send2] [send3] [send4] [end1] [end2] [end3] [end4] [busy1] [busy2] [busy3] [busy4] [cd] [time]
Variables:   b y1 y2 s1 x1 bc1 cd1 s2 x2 bc2 cd2 s3 x3 bc3 cd3 s4 x4 bc4 cd4
Labels:      "all_delivered" "collision_max_backoff"

Parsing properties file "/w0/tmp/slurm_tq429871.4965958/tmp5efn48_aprism_from-prism_check_ex_csma.4-2_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)...

Computing reachable states... 529211 761962 states
Reachable states exploration and model construction done in 4.335 secs.
Sorting reachable states list...

Time for model construction: 5.091 seconds.

Type:        MDP
States:      761962 (1 initial)
Transitions: 1327068
Choices:     825504
Max/avg:     4/1.08

Starting probabilistic reachability (max)...
Starting Prob0 (max)...
Prob0 (max) took 186 iterations and 1.312 seconds.
Starting Prob1 (max)...
Prob1 (max) took 1197 iterations and 9.807 seconds.
target=9, yes=142601, no=25408, maybe=593953
Starting value iteration (max, with Power method)...
Value iteration (max, with Power method) took 172 iterations, 190125188 multiplications and 1.381 seconds.
Probabilistic reachability took 12.518 seconds.

Value in the initial state: 0.776459404375732

Time for model checking: 12.561 seconds.

Result: 0.776459404375732 (+/- 6.170079467349154E-6 estimated; rel err 7.946428921560754E-6)


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g