Log files for model kanban.5 and tool configuration prism_from-umb_check_ex
[2.921, 2.901, 2.788, 2.681, 2.915]
Log file: prism_from-umb_check_ex_kanban.5_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 126.817 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:34:24 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.4966177/tmpara29lfoprism_from-umb_check_ex_kanban.5_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966177/tmpara29lfoprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [in] [s1] [s2]
Variables: x
Rewards: "throughput"
Parsing properties file "/w0/tmp/slurm_tq429871.4966177/tmpara29lfoprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props"...
1 property:
(1) "throughput": R{"throughput"}=? [ S ]
---------------------------------------------------------------------
Model checking: "throughput": R{"throughput"}=? [ S ]
Building model (engine:explicit)...
Time for model construction: 2.921 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Building reward structure...
Building embedded DTMC...
Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...
Time for BSCC computation: 1.744 seconds, found 1 BSCCs.
Computing steady state probabilities for BSCC 1
Starting value iteration...
Power method: 607 iterations in 119.144 seconds.
Value for BSCC 1: 0.30712469484259713
All states are in BSCCs (so no reachability probabilities computed)
Value in the initial state: 0.30712469484259713
Time for model checking: 123.204 seconds.
Result: 0.30712469484259713
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_kanban.5_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 124.898 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:38:34 GMT+02:00 2026
Hostname: n23m0314.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966364/tmpkbb3jqdnprism_from-umb_check_ex_kanban.5_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966364/tmpkbb3jqdnprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [in] [s1] [s2]
Variables: x
Rewards: "throughput"
Parsing properties file "/w0/tmp/slurm_tq429871.4966364/tmpkbb3jqdnprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props"...
1 property:
(1) "throughput": R{"throughput"}=? [ S ]
---------------------------------------------------------------------
Model checking: "throughput": R{"throughput"}=? [ S ]
Building model (engine:explicit)...
Time for model construction: 2.901 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Building reward structure...
Building embedded DTMC...
Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...
Time for BSCC computation: 1.532 seconds, found 1 BSCCs.
Computing steady state probabilities for BSCC 1
Starting value iteration...
Power method: 607 iterations in 117.517 seconds.
Value for BSCC 1: 0.30712469484259713
All states are in BSCCs (so no reachability probabilities computed)
Value in the initial state: 0.30712469484259713
Time for model checking: 121.294 seconds.
Result: 0.30712469484259713
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_kanban.5_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 121.296 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:25:57 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.4965756/tmpijrxqrxrprism_from-umb_check_ex_kanban.5_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965756/tmpijrxqrxrprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [in] [s1] [s2]
Variables: x
Rewards: "throughput"
Parsing properties file "/w0/tmp/slurm_tq429871.4965756/tmpijrxqrxrprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props"...
1 property:
(1) "throughput": R{"throughput"}=? [ S ]
---------------------------------------------------------------------
Model checking: "throughput": R{"throughput"}=? [ S ]
Building model (engine:explicit)...
Time for model construction: 2.788 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Building reward structure...
Building embedded DTMC...
Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...
Time for BSCC computation: 1.708 seconds, found 1 BSCCs.
Computing steady state probabilities for BSCC 1
Starting value iteration...
Power method: 607 iterations in 114.147 seconds.
Value for BSCC 1: 0.30712469484259713
All states are in BSCCs (so no reachability probabilities computed)
Value in the initial state: 0.30712469484259713
Time for model checking: 117.84 seconds.
Result: 0.30712469484259713
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_kanban.5_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 118.996 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:23:50 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.4965599/tmpab4j8qnsprism_from-umb_check_ex_kanban.5_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965599/tmpab4j8qnsprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [in] [s1] [s2]
Variables: x
Rewards: "throughput"
Parsing properties file "/w0/tmp/slurm_tq429871.4965599/tmpab4j8qnsprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props"...
1 property:
(1) "throughput": R{"throughput"}=? [ S ]
---------------------------------------------------------------------
Model checking: "throughput": R{"throughput"}=? [ S ]
Building model (engine:explicit)...
Time for model construction: 2.681 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Building reward structure...
Building embedded DTMC...
Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...
Time for BSCC computation: 1.493 seconds, found 1 BSCCs.
Computing steady state probabilities for BSCC 1
Starting value iteration...
Power method: 607 iterations in 112.172 seconds.
Value for BSCC 1: 0.30712469484259713
All states are in BSCCs (so no reachability probabilities computed)
Value in the initial state: 0.30712469484259713
Time for model checking: 115.657 seconds.
Result: 0.30712469484259713
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_kanban.5_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 125.624 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:28:12 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.4962312/tmpstzc5o7uprism_from-umb_check_ex_kanban.5_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962312/tmpstzc5o7uprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [in] [s1] [s2]
Variables: x
Rewards: "throughput"
Parsing properties file "/w0/tmp/slurm_tq429871.4962312/tmpstzc5o7uprism_from-umb_check_ex_kanban.5_tmp_indir_/property.props"...
1 property:
(1) "throughput": R{"throughput"}=? [ S ]
---------------------------------------------------------------------
Model checking: "throughput": R{"throughput"}=? [ S ]
Building model (engine:explicit)...
Time for model construction: 2.915 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Building reward structure...
Building embedded DTMC...
Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...
Time for BSCC computation: 1.583 seconds, found 1 BSCCs.
Computing steady state probabilities for BSCC 1
Starting value iteration...
Power method: 607 iterations in 118.122 seconds.
Value for BSCC 1: 0.30712469484259713
All states are in BSCCs (so no reachability probabilities computed)
Value in the initial state: 0.30712469484259713
Time for model checking: 121.953 seconds.
Result: 0.30712469484259713
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g