Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:22 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_000.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_000.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.011 seconds. Type: DTMC States: 1 (1 initial) Transitions: 1 Transition matrix: 8 nodes (2 terminal), 1 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=8] [0.4 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.0 KB] Allocating iteration vectors... [3 x 0.0 KB] TOTAL: [0.4 KB] Starting iterations... Steady state detected at iteration 1 Iterative method: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=1.0 Time for transient probability computation: 0.03 seconds. initial state: 50 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:23 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_001.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_001.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.012 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.9999999999995011 1:(101)=4.934870675537516E-13 2:(102)=1.6440261673066279E-21 3:(103)=4.10587815538435E-20 4:(104)=1.1999925247250116E-17 5:(105)=1.4319416572435065E-16 6:(106)=2.5203606342992095E-25 7:(107)=5.08338901451491E-24 Time for transient probability computation: 0.032 seconds. initial state: 54 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:23 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_010.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_010.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.019 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.5205419084369148 1:(101)=3.337337397213325E-7 2:(102)=0.47917713253975736 3:(103)=2.7888581549513283E-4 4:(104)=1.447877168475924E-9 5:(105)=6.541921962062192E-13 6:(106)=1.7373331377700035E-6 7:(107)=6.924350128617097E-10 Time for transient probability computation: 0.029 seconds. initial state: 52 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:24 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_011.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_011.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.018 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.672728399987998 1:(101)=0.024564324188298934 2:(102)=0.003005676027223589 3:(103)=0.29887608827039447 4:(104)=6.327696410541329E-6 5:(105)=1.1700229409743474E-4 6:(106)=3.4071593785340407E-6 7:(107)=6.98774376252523E-4 Time for transient probability computation: 0.031 seconds. initial state: 56 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:24 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_100.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_100.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.02 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.9999999995418597 1:(101)=1.5539069773398004E-13 2:(102)=2.0606382216878674E-14 3:(103)=4.338334473208149E-15 4:(104)=4.5264325864783075E-10 5:(105)=4.486971746235687E-12 6:(106)=7.428296351940473E-13 7:(107)=8.526443572149208E-14 Time for transient probability computation: 0.032 seconds. initial state: 51 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:25 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_101.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_101.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.009 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.9999885075677458 1:(101)=1.0785780055788036E-7 2:(102)=1.49904673096517E-12 3:(103)=6.21301214608554E-12 4:(104)=8.471252208779905E-6 5:(105)=2.913077168078193E-6 6:(106)=6.470638472892961E-11 7:(107)=1.7266473483296114E-10 Time for transient probability computation: 0.029 seconds. initial state: 55 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:26 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_110.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_110.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.019 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.9790797626486916 1:(101)=6.645074464193762E-6 2:(102)=0.009716405603303441 3:(103)=5.108563702087483E-4 4:(104)=4.092935926272201E-5 5:(105)=1.913005962336131E-7 6:(106)=0.010394905908425494 7:(107)=2.503037350465576E-4 Time for transient probability computation: 0.028 seconds. initial state: 53 ---------------------------------------------------------------------------------------------------- Picked up _JAVA_OPTIONS: -Xmx512m PRISM ===== Version: 4.7 Date: Sat Jun 24 13:34:26 MDT 2023 Hostname: ERIC-LAPTOP Memory limits: cudd=1g, java(heap)=512m Command line: prism models/ngdbf_trapping_3symbol_111.prism -tr 600 Parsing model file "models/ngdbf_trapping_3symbol_111.prism"... Type: DTMC Modules: trapping_set Variables: state --------------------------------------------------------------------- Computing transient probabilities (time = 600)... Building model... Computing reachable states... Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00) Time for model construction: 0.021 seconds. Type: DTMC States: 8 (1 initial) Transitions: 57 Transition matrix: 118 nodes (58 terminal), 57 minterms, vars: 3r/3c Computing probabilities... Engine: Hybrid Building hybrid MTBDD matrix... [levels=3, nodes=118] [5.5 KB] Adding explicit sparse matrices... [levels=3, num=1, compact] [0.7 KB] Allocating iteration vectors... [3 x 0.1 KB] TOTAL: [6.4 KB] Starting iterations... Iterative method: 600 iterations in 0.00 seconds (average 0.000000, setup 0.00) Printing transient probabilities in plain text format below: 0:(100)=0.3016032782528583 1:(101)=0.014413170771458612 2:(102)=0.0010283029351075001 3:(103)=0.09972896507294915 4:(104)=0.01055857624823256 5:(105)=0.12125921461120806 6:(106)=0.001557911963985697 7:(107)=0.44985058014421175 Time for transient probability computation: 0.03 seconds. initial state: 57 ----------------------------------------------------------------------------------------------------