*** This is NuSMV 2.3.1 (compiled on Mon Nov 21 15:48:12 UTC 2005) *** For more information on NuSMV see *** or email to . *** Please report bugs to . WARNING *** This version of NuSMV is linked to the MiniSat SAT solver *** WARNING *** See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat *** WARNING *** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson *** WARNING *** MiniSat is used in Bounded Model Checking when the *** WARNING *** environment variable sat_solver is set to 'minisat'. *** WARNING *** THE SOFTWARE IS PROVIDED 'AS IS', WITHOUT WARRANTY OF ANY KIND, *** WARNING *** EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES *** WARNING *** OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND *** WARNING *** NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT *** WARNING *** HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, *** WARNING *** WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *** WARNING *** FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR *** WARNING *** OTHER DEALINGS IN THE SOFTWARE. *** Starting the batch interaction. Parsing file /workspace/gabe/AMBA_AHB_Functional_Verification_3Masters_Final_Result.smv ......done. Flattening hierarchy ......done. Encoding variables ...... done. Building Model ...checking for multiple assignments... Done checking for circular assignments... Done ... done. ... done. evaluating specification AG master1.state != error Computing the set of fair x pairs size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 19019 BDD nodes size of Y2 = 5.90296e+20 x, 35056 BDD nodes size of Y3 = 5.90296e+20 x, 44271 BDD nodes size of Y4 = 5.90296e+20 x, 50308 BDD nodes size of Y5 = 5.90296e+20 x, 50476 BDD nodes size of Y6 = 5.90296e+20 x, 54760 BDD nodes size of Y7 = 5.90296e+20 x, 61881 BDD nodes size of Y8 = 5.90296e+20 x, 68150 BDD nodes size of Y9 = 5.90296e+20 x, 67806 BDD nodes size of Y10 = 5.90296e+20 x, 65871 BDD nodes size of Y11 = 5.90296e+20 x, 62701 BDD nodes size of Y12 = 5.90296e+20 x, 57732 BDD nodes size of Y13 = 5.90296e+20 x, 54520 BDD nodes size of Y14 = 5.90296e+20 x, 52707 BDD nodes size of Y15 = 5.90296e+20 x, 51013 BDD nodes size of Y16 = 5.90296e+20 x, 50576 BDD nodes size of Y17 = 5.90296e+20 x, 50702 BDD nodes size of Y18 = 5.90296e+20 x, 50694 BDD nodes size of Y19 = 5.90296e+20 x, 50335 BDD nodes size of Y20 = 5.90296e+20 x, 50187 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 20259 BDD nodes size of Y2 = 5.90296e+20 x, 35442 BDD nodes size of Y3 = 5.90296e+20 x, 46152 BDD nodes size of Y4 = 5.90296e+20 x, 50195 BDD nodes size of Y5 = 5.90296e+20 x, 49358 BDD nodes size of Y6 = 5.90296e+20 x, 53123 BDD nodes size of Y7 = 5.90296e+20 x, 59690 BDD nodes size of Y8 = 5.90296e+20 x, 66014 BDD nodes size of Y9 = 5.90296e+20 x, 66411 BDD nodes size of Y10 = 5.90296e+20 x, 65083 BDD nodes size of Y11 = 5.90296e+20 x, 61582 BDD nodes size of Y12 = 5.90296e+20 x, 56684 BDD nodes size of Y13 = 5.90296e+20 x, 53854 BDD nodes size of Y14 = 5.90296e+20 x, 52316 BDD nodes size of Y15 = 5.90296e+20 x, 50928 BDD nodes size of Y16 = 5.90296e+20 x, 50553 BDD nodes size of Y17 = 5.90296e+20 x, 50636 BDD nodes size of Y18 = 5.90296e+20 x, 50613 BDD nodes size of Y19 = 5.90296e+20 x, 50374 BDD nodes size of Y20 = 5.90296e+20 x, 50286 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21319 BDD nodes size of Y2 = 5.90296e+20 x, 33013 BDD nodes size of Y3 = 5.90296e+20 x, 45537 BDD nodes size of Y4 = 5.90296e+20 x, 48232 BDD nodes size of Y5 = 5.90296e+20 x, 47085 BDD nodes size of Y6 = 5.90296e+20 x, 51157 BDD nodes size of Y7 = 5.90296e+20 x, 57675 BDD nodes size of Y8 = 5.90296e+20 x, 64488 BDD nodes size of Y9 = 5.90296e+20 x, 64637 BDD nodes size of Y10 = 5.90296e+20 x, 63047 BDD nodes size of Y11 = 5.90296e+20 x, 59860 BDD nodes size of Y12 = 5.90296e+20 x, 55144 BDD nodes size of Y13 = 5.90296e+20 x, 52393 BDD nodes size of Y14 = 5.90296e+20 x, 51067 BDD nodes size of Y15 = 5.90296e+20 x, 49754 BDD nodes size of Y16 = 5.90296e+20 x, 49441 BDD nodes size of Y17 = 5.90296e+20 x, 49455 BDD nodes size of Y18 = 5.90296e+20 x, 49433 BDD nodes size of Y19 = 5.90296e+20 x, 49134 BDD nodes size of Y20 = 5.90296e+20 x, 49020 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16818 BDD nodes size of Y2 = 5.90296e+20 x, 8816 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 8025 BDD nodes size of res1 = 2.83594e+12 x, 82796 BDD nodes size of Y0 = 5.063e+11 x, 19920 BDD nodes size of Y1 = 8.18264e+11 x, 47335 BDD nodes size of Y2 = 1.0283e+12 x, 70523 BDD nodes size of Y3 = 1.24687e+12 x, 77288 BDD nodes size of Y4 = 1.31586e+12 x, 85491 BDD nodes size of Y5 = 1.35852e+12 x, 86384 BDD nodes size of Y6 = 1.41534e+12 x, 89066 BDD nodes size of Y7 = 1.49543e+12 x, 91942 BDD nodes size of Y8 = 1.55201e+12 x, 93613 BDD nodes size of Y9 = 1.59382e+12 x, 91972 BDD nodes size of Y10 = 1.62288e+12 x, 89347 BDD nodes size of Y11 = 1.63445e+12 x, 85060 BDD nodes size of Y12 = 1.64147e+12 x, 80502 BDD nodes size of Y13 = 1.6448e+12 x, 77537 BDD nodes size of Y14 = 1.64572e+12 x, 75589 BDD nodes size of Y15 = 1.6459e+12 x, 75287 BDD nodes size of Y16 = 1.64602e+12 x, 75295 BDD nodes size of Y17 = 1.6461e+12 x, 75250 BDD nodes size of Y18 = 1.64612e+12 x, 75222 BDD nodes size of Y0 = 5.063e+11 x, 19134 BDD nodes size of Y1 = 8.18264e+11 x, 45317 BDD nodes size of Y2 = 1.0283e+12 x, 65944 BDD nodes size of Y3 = 1.24687e+12 x, 72727 BDD nodes size of Y4 = 1.31586e+12 x, 82574 BDD nodes size of Y5 = 1.35852e+12 x, 83708 BDD nodes size of Y6 = 1.41534e+12 x, 85556 BDD nodes size of Y7 = 1.49543e+12 x, 87199 BDD nodes size of Y8 = 1.55201e+12 x, 88283 BDD nodes size of Y9 = 1.59382e+12 x, 87062 BDD nodes size of Y10 = 1.62288e+12 x, 84968 BDD nodes size of Y11 = 1.63445e+12 x, 80964 BDD nodes size of Y12 = 1.64147e+12 x, 76855 BDD nodes size of Y13 = 1.6448e+12 x, 74351 BDD nodes size of Y14 = 1.64572e+12 x, 72527 BDD nodes size of Y15 = 1.6459e+12 x, 72258 BDD nodes size of Y16 = 1.64602e+12 x, 72266 BDD nodes size of Y17 = 1.6461e+12 x, 72214 BDD nodes size of Y18 = 1.64612e+12 x, 72192 BDD nodes size of Y0 = 5.063e+11 x, 17912 BDD nodes size of Y1 = 8.18264e+11 x, 42660 BDD nodes size of Y2 = 1.0283e+12 x, 59844 BDD nodes size of Y3 = 1.24687e+12 x, 68095 BDD nodes size of Y4 = 1.31586e+12 x, 80570 BDD nodes size of Y5 = 1.35852e+12 x, 82161 BDD nodes size of Y6 = 1.41534e+12 x, 83284 BDD nodes size of Y7 = 1.49543e+12 x, 84087 BDD nodes size of Y8 = 1.55201e+12 x, 84429 BDD nodes size of Y9 = 1.59382e+12 x, 83073 BDD nodes size of Y10 = 1.62288e+12 x, 81187 BDD nodes size of Y11 = 1.63445e+12 x, 77367 BDD nodes size of Y12 = 1.64147e+12 x, 73152 BDD nodes size of Y13 = 1.6448e+12 x, 70815 BDD nodes size of Y14 = 1.64572e+12 x, 69396 BDD nodes size of Y15 = 1.6459e+12 x, 69164 BDD nodes size of Y16 = 1.64602e+12 x, 69180 BDD nodes size of Y17 = 1.6461e+12 x, 69148 BDD nodes size of Y18 = 1.64612e+12 x, 69113 BDD nodes size of Y0 = 1.23199e+12 x, 19324 BDD nodes size of Y1 = 1.87992e+12 x, 62043 BDD nodes size of Y2 = 2.6185e+12 x, 79459 BDD nodes size of Y3 = 2.83594e+12 x, 82796 BDD nodes size of Y0 = 2.14156e+12 x, 76613 BDD nodes size of Y1 = 2.83592e+12 x, 82718 BDD nodes size of res2 = 4.3279e+11 x, 57249 BDD nodes size of Y0 = 8.13955e+10 x, 15729 BDD nodes size of Y1 = 2.032e+11 x, 36696 BDD nodes size of Y2 = 2.58589e+11 x, 52817 BDD nodes size of Y3 = 3.06809e+11 x, 57504 BDD nodes size of Y4 = 3.213e+11 x, 62607 BDD nodes size of Y5 = 3.3453e+11 x, 62912 BDD nodes size of Y6 = 3.51436e+11 x, 63938 BDD nodes size of Y7 = 3.76366e+11 x, 66313 BDD nodes size of Y8 = 3.99001e+11 x, 66076 BDD nodes size of Y9 = 4.09379e+11 x, 65145 BDD nodes size of Y10 = 4.19907e+11 x, 64073 BDD nodes size of Y11 = 4.25954e+11 x, 62696 BDD nodes size of Y12 = 4.29287e+11 x, 59706 BDD nodes size of Y13 = 4.31661e+11 x, 58187 BDD nodes size of Y14 = 4.32368e+11 x, 57243 BDD nodes size of Y15 = 4.32525e+11 x, 57109 BDD nodes size of Y16 = 4.32665e+11 x, 57003 BDD nodes size of Y17 = 4.32756e+11 x, 56814 BDD nodes size of Y18 = 4.32769e+11 x, 56784 BDD nodes size of Y0 = 8.13955e+10 x, 16295 BDD nodes size of Y1 = 2.032e+11 x, 37409 BDD nodes size of Y2 = 2.58589e+11 x, 51890 BDD nodes size of Y3 = 3.06809e+11 x, 56682 BDD nodes size of Y4 = 3.213e+11 x, 63100 BDD nodes size of Y5 = 3.3453e+11 x, 63527 BDD nodes size of Y6 = 3.51436e+11 x, 64239 BDD nodes size of Y7 = 3.76366e+11 x, 65813 BDD nodes size of Y8 = 3.99001e+11 x, 65351 BDD nodes size of Y9 = 4.09379e+11 x, 64375 BDD nodes size of Y10 = 4.19907e+11 x, 63341 BDD nodes size of Y11 = 4.25954e+11 x, 62248 BDD nodes size of Y12 = 4.29287e+11 x, 59680 BDD nodes size of Y13 = 4.31661e+11 x, 58210 BDD nodes size of Y14 = 4.32368e+11 x, 57182 BDD nodes size of Y15 = 4.32525e+11 x, 57068 BDD nodes size of Y16 = 4.32665e+11 x, 56987 BDD nodes size of Y17 = 4.32756e+11 x, 56829 BDD nodes size of Y18 = 4.32769e+11 x, 56805 BDD nodes size of Y0 = 8.13955e+10 x, 16384 BDD nodes size of Y1 = 2.032e+11 x, 37007 BDD nodes size of Y2 = 2.58589e+11 x, 49624 BDD nodes size of Y3 = 3.06809e+11 x, 55515 BDD nodes size of Y4 = 3.213e+11 x, 63574 BDD nodes size of Y5 = 3.3453e+11 x, 64229 BDD nodes size of Y6 = 3.51436e+11 x, 64494 BDD nodes size of Y7 = 3.76366e+11 x, 65440 BDD nodes size of Y8 = 3.99001e+11 x, 64099 BDD nodes size of Y9 = 4.09379e+11 x, 62921 BDD nodes size of Y10 = 4.19907e+11 x, 62427 BDD nodes size of Y11 = 4.25954e+11 x, 61567 BDD nodes size of Y12 = 4.29287e+11 x, 59062 BDD nodes size of Y13 = 4.31661e+11 x, 57883 BDD nodes size of Y14 = 4.32368e+11 x, 57210 BDD nodes size of Y15 = 4.32525e+11 x, 57135 BDD nodes size of Y16 = 4.32665e+11 x, 57043 BDD nodes size of Y17 = 4.32756e+11 x, 56857 BDD nodes size of Y18 = 4.32769e+11 x, 56822 BDD nodes size of Y0 = 2.1877e+11 x, 12135 BDD nodes size of Y1 = 3.09462e+11 x, 39692 BDD nodes size of Y2 = 4.3279e+11 x, 57249 BDD nodes size of Y0 = 3.23105e+11 x, 55464 BDD nodes size of Y1 = 4.3278e+11 x, 57175 BDD nodes size of res3 = 4.32765e+11 x, 56764 BDD nodes size of Y0 = 8.13914e+10 x, 15709 BDD nodes size of Y1 = 2.03196e+11 x, 36676 BDD nodes size of Y2 = 2.58585e+11 x, 52799 BDD nodes size of Y3 = 3.06804e+11 x, 57484 BDD nodes size of Y4 = 3.21296e+11 x, 62587 BDD nodes size of Y5 = 3.34526e+11 x, 62892 BDD nodes size of Y6 = 3.51432e+11 x, 63918 BDD nodes size of Y7 = 3.76362e+11 x, 66293 BDD nodes size of Y8 = 3.98997e+11 x, 66056 BDD nodes size of Y9 = 4.09375e+11 x, 65125 BDD nodes size of Y10 = 4.19903e+11 x, 64053 BDD nodes size of Y11 = 4.25949e+11 x, 62676 BDD nodes size of Y12 = 4.29283e+11 x, 59686 BDD nodes size of Y13 = 4.31657e+11 x, 58167 BDD nodes size of Y14 = 4.32364e+11 x, 57223 BDD nodes size of Y15 = 4.32521e+11 x, 57089 BDD nodes size of Y16 = 4.32661e+11 x, 56983 BDD nodes size of Y17 = 4.32752e+11 x, 56794 BDD nodes size of Y18 = 4.32765e+11 x, 56764 BDD nodes size of Y0 = 8.13914e+10 x, 16254 BDD nodes size of Y1 = 2.03196e+11 x, 37368 BDD nodes size of Y2 = 2.58585e+11 x, 51849 BDD nodes size of Y3 = 3.06804e+11 x, 56641 BDD nodes size of Y4 = 3.21296e+11 x, 63059 BDD nodes size of Y5 = 3.34526e+11 x, 63486 BDD nodes size of Y6 = 3.51432e+11 x, 64198 BDD nodes size of Y7 = 3.76362e+11 x, 65772 BDD nodes size of Y8 = 3.98997e+11 x, 65310 BDD nodes size of Y9 = 4.09375e+11 x, 64334 BDD nodes size of Y10 = 4.19903e+11 x, 63300 BDD nodes size of Y11 = 4.25949e+11 x, 62207 BDD nodes size of Y12 = 4.29283e+11 x, 59639 BDD nodes size of Y13 = 4.31657e+11 x, 58169 BDD nodes size of Y14 = 4.32364e+11 x, 57141 BDD nodes size of Y15 = 4.32521e+11 x, 57027 BDD nodes size of Y16 = 4.32661e+11 x, 56946 BDD nodes size of Y17 = 4.32752e+11 x, 56788 BDD nodes size of Y18 = 4.32765e+11 x, 56764 BDD nodes size of Y0 = 8.13914e+10 x, 16324 BDD nodes size of Y1 = 2.03196e+11 x, 36947 BDD nodes size of Y2 = 2.58585e+11 x, 49566 BDD nodes size of Y3 = 3.06804e+11 x, 55457 BDD nodes size of Y4 = 3.21296e+11 x, 63516 BDD nodes size of Y5 = 3.34526e+11 x, 64171 BDD nodes size of Y6 = 3.51432e+11 x, 64436 BDD nodes size of Y7 = 3.76362e+11 x, 65382 BDD nodes size of Y8 = 3.98997e+11 x, 64041 BDD nodes size of Y9 = 4.09375e+11 x, 62863 BDD nodes size of Y10 = 4.19903e+11 x, 62369 BDD nodes size of Y11 = 4.25949e+11 x, 61509 BDD nodes size of Y12 = 4.29283e+11 x, 59004 BDD nodes size of Y13 = 4.31657e+11 x, 57825 BDD nodes size of Y14 = 4.32364e+11 x, 57152 BDD nodes size of Y15 = 4.32521e+11 x, 57077 BDD nodes size of Y16 = 4.32661e+11 x, 56985 BDD nodes size of Y17 = 4.32752e+11 x, 56799 BDD nodes size of Y18 = 4.32765e+11 x, 56764 BDD nodes size of Y0 = 2.18761e+11 x, 12053 BDD nodes size of Y1 = 3.09445e+11 x, 39253 BDD nodes size of Y2 = 4.32765e+11 x, 56764 BDD nodes size of Y0 = 3.23089e+11 x, 55053 BDD nodes size of Y1 = 4.32765e+11 x, 56764 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 1.13476e+10 states, 6630 BDD nodes size of Y2 = 1.73777e+10 states, 10538 BDD nodes size of Y3 = 2.18929e+10 states, 11198 BDD nodes size of Y4 = 2.28177e+10 states, 11506 BDD nodes -- specification AG master1.state != error is true evaluating specification AG master2.state != error eu: computing fixed point approximations for AG master2.state != error ... size of Y1 = 1.13476e+10 states, 5764 BDD nodes size of Y2 = 1.73777e+10 states, 9694 BDD nodes size of Y3 = 2.18929e+10 states, 10007 BDD nodes size of Y4 = 2.28177e+10 states, 10146 BDD nodes -- specification AG master2.state != error is true evaluating specification AG master3.state != error eu: computing fixed point approximations for AG master3.state != error ... size of Y1 = 1.13476e+10 states, 5033 BDD nodes size of Y2 = 1.73777e+10 states, 8985 BDD nodes size of Y3 = 2.18929e+10 states, 9131 BDD nodes size of Y4 = 2.28177e+10 states, 9184 BDD nodes -- specification AG master3.state != error is true evaluating specification AG slave.state != error eu: computing fixed point approximations for AG slave.state != error ... size of Y1 = 4.4897e+10 states, 15814 BDD nodes size of Y2 = 1.14462e+11 states, 36469 BDD nodes size of Y3 = 1.94974e+11 states, 49093 BDD nodes size of Y4 = 2.16002e+11 states, 53729 BDD nodes size of Y5 = 2.17229e+11 states, 53729 BDD nodes -- specification AG slave.state != error is true evaluating specification EF (arbiter.master1_state = mask & arbiter.master2_state = mask) eu: computing fixed point approximations for EF (arbiter.master1_state = mask & arbiter.master2_state = mask) ... size of Y1 = 1.74896e+10 states, 46605 BDD nodes size of Y2 = 2.15222e+10 states, 46790 BDD nodes size of Y3 = 2.58004e+10 states, 51287 BDD nodes size of Y4 = 3.28935e+10 states, 53200 BDD nodes size of Y5 = 3.61916e+10 states, 59681 BDD nodes size of Y6 = 4.32468e+10 states, 62654 BDD nodes size of Y7 = 6.32271e+10 states, 63971 BDD nodes size of Y8 = 1.20444e+11 states, 71380 BDD nodes size of Y9 = 1.86792e+11 states, 76772 BDD nodes size of Y10 = 2.20081e+11 states, 83829 BDD nodes size of Y11 = 2.53359e+11 states, 85143 BDD nodes size of Y12 = 3.12043e+11 states, 86194 BDD nodes size of Y13 = 3.61703e+11 states, 84263 BDD nodes size of Y14 = 3.98815e+11 states, 77515 BDD nodes size of Y15 = 4.13029e+11 states, 69899 BDD nodes size of Y16 = 4.2328e+11 states, 67261 BDD nodes size of Y17 = 4.30022e+11 states, 63601 BDD nodes size of Y18 = 4.32357e+11 states, 58180 BDD nodes size of Y19 = 4.32733e+11 states, 57098 BDD nodes size of Y20 = 4.32765e+11 states, 56764 BDD nodes -- specification EF (arbiter.master1_state = mask & arbiter.master2_state = mask) is true evaluating specification AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16147 BDD nodes size of Y2 = 5.90296e+20 x, 18250 BDD nodes size of Y3 = 5.90296e+20 x, 18887 BDD nodes size of Y4 = 5.90296e+20 x, 18943 BDD nodes size of Y5 = 5.90296e+20 x, 19034 BDD nodes size of Y6 = 5.90296e+20 x, 19137 BDD nodes size of Y7 = 5.90296e+20 x, 19841 BDD nodes size of Y8 = 5.90296e+20 x, 19753 BDD nodes size of Y9 = 5.90296e+20 x, 20300 BDD nodes size of Y10 = 5.90296e+20 x, 20509 BDD nodes size of Y11 = 5.90296e+20 x, 20656 BDD nodes size of Y12 = 5.90296e+20 x, 20373 BDD nodes size of Y13 = 5.90296e+20 x, 20311 BDD nodes size of Y14 = 5.90296e+20 x, 19980 BDD nodes size of Y15 = 5.90296e+20 x, 19844 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16738 BDD nodes size of Y2 = 5.90296e+20 x, 20285 BDD nodes size of Y3 = 5.90296e+20 x, 21445 BDD nodes size of Y4 = 5.90296e+20 x, 21657 BDD nodes size of Y5 = 5.90296e+20 x, 21744 BDD nodes size of Y6 = 5.90296e+20 x, 21805 BDD nodes size of Y7 = 5.90296e+20 x, 21664 BDD nodes size of Y8 = 5.90296e+20 x, 21664 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16454 BDD nodes size of Y2 = 5.90296e+20 x, 19486 BDD nodes size of Y3 = 5.90296e+20 x, 20683 BDD nodes size of Y4 = 5.90296e+20 x, 21138 BDD nodes size of Y5 = 5.90296e+20 x, 21370 BDD nodes size of Y6 = 5.90296e+20 x, 21483 BDD nodes size of Y7 = 5.90296e+20 x, 21303 BDD nodes size of Y8 = 5.90296e+20 x, 21303 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23056 BDD nodes size of Y2 = 5.90296e+20 x, 26261 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 5397 BDD nodes size of res1 = 6.1417e+09 x, 14828 BDD nodes size of Y0 = 2.60318e+09 x, 7086 BDD nodes size of Y1 = 3.7055e+09 x, 12528 BDD nodes size of Y2 = 3.94647e+09 x, 13629 BDD nodes size of Y3 = 4.1576e+09 x, 14715 BDD nodes size of Y4 = 4.23326e+09 x, 15113 BDD nodes size of Y5 = 4.36095e+09 x, 15443 BDD nodes size of Y6 = 4.55245e+09 x, 15602 BDD nodes size of Y7 = 4.87869e+09 x, 16047 BDD nodes size of Y8 = 5.2671e+09 x, 15726 BDD nodes size of Y9 = 5.47092e+09 x, 16258 BDD nodes size of Y10 = 5.6461e+09 x, 15964 BDD nodes size of Y11 = 5.84015e+09 x, 16051 BDD nodes size of Y12 = 5.87701e+09 x, 15776 BDD nodes size of Y13 = 5.89628e+09 x, 15803 BDD nodes size of Y14 = 5.90592e+09 x, 15474 BDD nodes size of Y15 = 5.90759e+09 x, 15404 BDD nodes size of Y0 = 8.34929e+07 x, 2053 BDD nodes size of Y0 = 8.34929e+07 x, 2143 BDD nodes size of Y0 = 3.36803e+09 x, 3579 BDD nodes size of Y1 = 4.43958e+09 x, 12558 BDD nodes size of Y2 = 6.02845e+09 x, 14844 BDD nodes size of Y0 = 4.45559e+09 x, 14639 BDD nodes size of Y1 = 6.1417e+09 x, 14828 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) ... -- specification AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) is true evaluating specification EF (arbiter.master1_state = mask & arbiter.master3_state = mask) eu: computing fixed point approximations for EF (arbiter.master1_state = mask & arbiter.master3_state = mask) ... size of Y1 = 1.74896e+10 states, 46995 BDD nodes size of Y2 = 2.15222e+10 states, 47161 BDD nodes size of Y3 = 2.58004e+10 states, 51760 BDD nodes size of Y4 = 3.28935e+10 states, 54107 BDD nodes size of Y5 = 3.61916e+10 states, 61162 BDD nodes size of Y6 = 4.32468e+10 states, 63827 BDD nodes size of Y7 = 6.32271e+10 states, 65536 BDD nodes size of Y8 = 1.20444e+11 states, 72911 BDD nodes size of Y9 = 1.86792e+11 states, 79184 BDD nodes size of Y10 = 2.20081e+11 states, 87022 BDD nodes size of Y11 = 2.53359e+11 states, 88722 BDD nodes size of Y12 = 3.12043e+11 states, 88535 BDD nodes size of Y13 = 3.61703e+11 states, 86536 BDD nodes size of Y14 = 3.98815e+11 states, 80186 BDD nodes size of Y15 = 4.13029e+11 states, 71778 BDD nodes size of Y16 = 4.2328e+11 states, 68771 BDD nodes size of Y17 = 4.30022e+11 states, 64474 BDD nodes size of Y18 = 4.32357e+11 states, 58324 BDD nodes size of Y19 = 4.32733e+11 states, 57088 BDD nodes size of Y20 = 4.32765e+11 states, 56764 BDD nodes -- specification EF (arbiter.master1_state = mask & arbiter.master3_state = mask) is true evaluating specification AG ((arbiter.master1_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master3_state != mask)) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16989 BDD nodes size of Y2 = 5.90296e+20 x, 20845 BDD nodes size of Y3 = 5.90296e+20 x, 21631 BDD nodes size of Y4 = 5.90296e+20 x, 21706 BDD nodes size of Y5 = 5.90296e+20 x, 21715 BDD nodes size of Y6 = 5.90296e+20 x, 21755 BDD nodes size of Y7 = 5.90296e+20 x, 21636 BDD nodes size of Y8 = 5.90296e+20 x, 21636 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16475 BDD nodes size of Y2 = 5.90296e+20 x, 18359 BDD nodes size of Y3 = 5.90296e+20 x, 18996 BDD nodes size of Y4 = 5.90296e+20 x, 19116 BDD nodes size of Y5 = 5.90296e+20 x, 19344 BDD nodes size of Y6 = 5.90296e+20 x, 19350 BDD nodes size of Y7 = 5.90296e+20 x, 20146 BDD nodes size of Y8 = 5.90296e+20 x, 20155 BDD nodes size of Y9 = 5.90296e+20 x, 20630 BDD nodes size of Y10 = 5.90296e+20 x, 20708 BDD nodes size of Y11 = 5.90296e+20 x, 20737 BDD nodes size of Y12 = 5.90296e+20 x, 20455 BDD nodes size of Y13 = 5.90296e+20 x, 20412 BDD nodes size of Y14 = 5.90296e+20 x, 20111 BDD nodes size of Y15 = 5.90296e+20 x, 20001 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16837 BDD nodes size of Y2 = 5.90296e+20 x, 19774 BDD nodes size of Y3 = 5.90296e+20 x, 20616 BDD nodes size of Y4 = 5.90296e+20 x, 21057 BDD nodes size of Y5 = 5.90296e+20 x, 21282 BDD nodes size of Y6 = 5.90296e+20 x, 21397 BDD nodes size of Y7 = 5.90296e+20 x, 21221 BDD nodes size of Y8 = 5.90296e+20 x, 21221 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23271 BDD nodes size of Y2 = 5.90296e+20 x, 26568 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 5428 BDD nodes size of res1 = 6.1417e+09 x, 14818 BDD nodes size of Y0 = 8.34929e+07 x, 2040 BDD nodes size of Y0 = 2.60318e+09 x, 7169 BDD nodes size of Y1 = 3.7055e+09 x, 12582 BDD nodes size of Y2 = 3.94647e+09 x, 13649 BDD nodes size of Y3 = 4.1576e+09 x, 14752 BDD nodes size of Y4 = 4.23326e+09 x, 15181 BDD nodes size of Y5 = 4.36095e+09 x, 15619 BDD nodes size of Y6 = 4.55245e+09 x, 15672 BDD nodes size of Y7 = 4.87869e+09 x, 16252 BDD nodes size of Y8 = 5.2671e+09 x, 16045 BDD nodes size of Y9 = 5.47092e+09 x, 16520 BDD nodes size of Y10 = 5.6461e+09 x, 16169 BDD nodes size of Y11 = 5.84015e+09 x, 16149 BDD nodes size of Y12 = 5.87701e+09 x, 15866 BDD nodes size of Y13 = 5.89628e+09 x, 15885 BDD nodes size of Y14 = 5.90592e+09 x, 15505 BDD nodes size of Y15 = 5.90759e+09 x, 15433 BDD nodes size of Y0 = 8.34929e+07 x, 2139 BDD nodes size of Y0 = 3.36803e+09 x, 3505 BDD nodes size of Y1 = 4.43958e+09 x, 12476 BDD nodes size of Y2 = 6.02845e+09 x, 14833 BDD nodes size of Y0 = 4.45559e+09 x, 14644 BDD nodes size of Y1 = 6.1417e+09 x, 14818 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((arbiter.master1_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master3_state != mask)) ... -- specification AG ((arbiter.master1_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master3_state != mask)) is true evaluating specification EF (arbiter.master2_state = mask & arbiter.master3_state = mask) eu: computing fixed point approximations for EF (arbiter.master2_state = mask & arbiter.master3_state = mask) ... size of Y1 = 1.74896e+10 states, 47466 BDD nodes size of Y2 = 2.15222e+10 states, 47608 BDD nodes size of Y3 = 2.58004e+10 states, 52304 BDD nodes size of Y4 = 3.28935e+10 states, 55297 BDD nodes size of Y5 = 3.61916e+10 states, 63205 BDD nodes size of Y6 = 4.32468e+10 states, 65472 BDD nodes size of Y7 = 6.32271e+10 states, 67747 BDD nodes size of Y8 = 1.20444e+11 states, 74766 BDD nodes size of Y9 = 1.86792e+11 states, 81207 BDD nodes size of Y10 = 2.20081e+11 states, 89086 BDD nodes size of Y11 = 2.53359e+11 states, 91009 BDD nodes size of Y12 = 3.12043e+11 states, 91064 BDD nodes size of Y13 = 3.61703e+11 states, 90176 BDD nodes size of Y14 = 3.98815e+11 states, 83656 BDD nodes size of Y15 = 4.13029e+11 states, 74069 BDD nodes size of Y16 = 4.2328e+11 states, 70528 BDD nodes size of Y17 = 4.30022e+11 states, 65510 BDD nodes size of Y18 = 4.32357e+11 states, 58567 BDD nodes size of Y19 = 4.32733e+11 states, 57078 BDD nodes size of Y20 = 4.32765e+11 states, 56764 BDD nodes -- specification EF (arbiter.master2_state = mask & arbiter.master3_state = mask) is true evaluating specification AG ((arbiter.master2_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master2_state != mask | arbiter.master3_state != mask)) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 17721 BDD nodes size of Y2 = 5.90296e+20 x, 21377 BDD nodes size of Y3 = 5.90296e+20 x, 21721 BDD nodes size of Y4 = 5.90296e+20 x, 21784 BDD nodes size of Y5 = 5.90296e+20 x, 21784 BDD nodes size of Y6 = 5.90296e+20 x, 21826 BDD nodes size of Y7 = 5.90296e+20 x, 21703 BDD nodes size of Y8 = 5.90296e+20 x, 21703 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 17860 BDD nodes size of Y2 = 5.90296e+20 x, 21091 BDD nodes size of Y3 = 5.90296e+20 x, 21453 BDD nodes size of Y4 = 5.90296e+20 x, 21637 BDD nodes size of Y5 = 5.90296e+20 x, 21708 BDD nodes size of Y6 = 5.90296e+20 x, 21774 BDD nodes size of Y7 = 5.90296e+20 x, 21633 BDD nodes size of Y8 = 5.90296e+20 x, 21633 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 16466 BDD nodes size of Y2 = 5.90296e+20 x, 18064 BDD nodes size of Y3 = 5.90296e+20 x, 18728 BDD nodes size of Y4 = 5.90296e+20 x, 18970 BDD nodes size of Y5 = 5.90296e+20 x, 19402 BDD nodes size of Y6 = 5.90296e+20 x, 19286 BDD nodes size of Y7 = 5.90296e+20 x, 20252 BDD nodes size of Y8 = 5.90296e+20 x, 20251 BDD nodes size of Y9 = 5.90296e+20 x, 20560 BDD nodes size of Y10 = 5.90296e+20 x, 20468 BDD nodes size of Y11 = 5.90296e+20 x, 20440 BDD nodes size of Y12 = 5.90296e+20 x, 20204 BDD nodes size of Y13 = 5.90296e+20 x, 20188 BDD nodes size of Y14 = 5.90296e+20 x, 19919 BDD nodes size of Y15 = 5.90296e+20 x, 19835 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23617 BDD nodes size of Y2 = 5.90296e+20 x, 26897 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 5509 BDD nodes size of res1 = 6.1417e+09 x, 15120 BDD nodes size of Y0 = 8.34929e+07 x, 1994 BDD nodes size of Y0 = 8.34929e+07 x, 1973 BDD nodes size of Y0 = 2.60318e+09 x, 7373 BDD nodes size of Y1 = 3.7055e+09 x, 12909 BDD nodes size of Y2 = 3.94647e+09 x, 13889 BDD nodes size of Y3 = 4.1576e+09 x, 15136 BDD nodes size of Y4 = 4.23326e+09 x, 15654 BDD nodes size of Y5 = 4.36095e+09 x, 16254 BDD nodes size of Y6 = 4.55245e+09 x, 16182 BDD nodes size of Y7 = 4.87869e+09 x, 17026 BDD nodes size of Y8 = 5.2671e+09 x, 16885 BDD nodes size of Y9 = 5.47092e+09 x, 17207 BDD nodes size of Y10 = 5.6461e+09 x, 16772 BDD nodes size of Y11 = 5.84015e+09 x, 16705 BDD nodes size of Y12 = 5.87701e+09 x, 16457 BDD nodes size of Y13 = 5.89628e+09 x, 16475 BDD nodes size of Y14 = 5.90592e+09 x, 15983 BDD nodes size of Y15 = 5.90759e+09 x, 15902 BDD nodes size of Y0 = 3.36803e+09 x, 3752 BDD nodes size of Y1 = 4.43958e+09 x, 13023 BDD nodes size of Y2 = 6.02845e+09 x, 15134 BDD nodes size of Y0 = 4.45559e+09 x, 14958 BDD nodes size of Y1 = 6.1417e+09 x, 15120 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((arbiter.master2_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master2_state != mask | arbiter.master3_state != mask)) ... -- specification AG ((arbiter.master2_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master2_state != mask | arbiter.master3_state != mask)) is true evaluating specification EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) eu: computing fixed point approximations for EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) ... size of Y1 = 3.33928e+09 states, 42894 BDD nodes size of Y2 = 3.7857e+09 states, 43123 BDD nodes size of Y3 = 4.38339e+09 states, 46471 BDD nodes size of Y4 = 5.39152e+09 states, 45581 BDD nodes size of Y5 = 5.87717e+09 states, 48451 BDD nodes size of Y6 = 7.55153e+09 states, 50723 BDD nodes size of Y7 = 1.09806e+10 states, 52262 BDD nodes size of Y8 = 2.18933e+10 states, 57401 BDD nodes size of Y9 = 3.75088e+10 states, 63612 BDD nodes size of Y10 = 4.67402e+10 states, 76857 BDD nodes size of Y11 = 6.64321e+10 states, 79424 BDD nodes size of Y12 = 1.1731e+11 states, 79408 BDD nodes size of Y13 = 2.04948e+11 states, 85401 BDD nodes size of Y14 = 3.01434e+11 states, 76785 BDD nodes size of Y15 = 3.37369e+11 states, 71008 BDD nodes size of Y16 = 3.66966e+11 states, 68425 BDD nodes size of Y17 = 4.10931e+11 states, 67284 BDD nodes size of Y18 = 4.28081e+11 states, 59570 BDD nodes size of Y19 = 4.3099e+11 states, 58148 BDD nodes size of Y20 = 4.32765e+11 states, 56764 BDD nodes -- specification EF ((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) is true evaluating specification AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 14774 BDD nodes size of Y2 = 5.90296e+20 x, 16830 BDD nodes size of Y3 = 5.90296e+20 x, 17322 BDD nodes size of Y4 = 5.90296e+20 x, 17368 BDD nodes size of Y5 = 5.90296e+20 x, 17390 BDD nodes size of Y6 = 5.90296e+20 x, 17419 BDD nodes size of Y7 = 5.90296e+20 x, 17342 BDD nodes size of Y8 = 5.90296e+20 x, 17342 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 14862 BDD nodes size of Y2 = 5.90296e+20 x, 16702 BDD nodes size of Y3 = 5.90296e+20 x, 17212 BDD nodes size of Y4 = 5.90296e+20 x, 17321 BDD nodes size of Y5 = 5.90296e+20 x, 17379 BDD nodes size of Y6 = 5.90296e+20 x, 17418 BDD nodes size of Y7 = 5.90296e+20 x, 17333 BDD nodes size of Y8 = 5.90296e+20 x, 17333 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 14589 BDD nodes size of Y2 = 5.90296e+20 x, 16158 BDD nodes size of Y3 = 5.90296e+20 x, 16710 BDD nodes size of Y4 = 5.90296e+20 x, 16941 BDD nodes size of Y5 = 5.90296e+20 x, 17071 BDD nodes size of Y6 = 5.90296e+20 x, 17134 BDD nodes size of Y7 = 5.90296e+20 x, 17030 BDD nodes size of Y8 = 5.90296e+20 x, 17030 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 19507 BDD nodes size of Y2 = 5.90296e+20 x, 23267 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 4266 BDD nodes size of res1 = 4.84319e+08 x, 8942 BDD nodes size of Y0 = 1.74408e+07 x, 1677 BDD nodes size of Y0 = 1.74408e+07 x, 1798 BDD nodes size of Y0 = 1.74408e+07 x, 2060 BDD nodes size of Y0 = 2.64241e+08 x, 1769 BDD nodes size of Y1 = 2.98746e+08 x, 5909 BDD nodes size of Y2 = 3.33324e+08 x, 6326 BDD nodes size of Y0 = 3.52199e+08 x, 8926 BDD nodes size of Y1 = 4.84319e+08 x, 8942 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) ... -- specification AG (((arbiter.master1_state = mask & arbiter.master2_state = mask) & arbiter.master3_state = mask) -> AF ((arbiter.master1_state != mask | arbiter.master2_state != mask) | arbiter.master3_state != mask)) is true evaluating specification AG (master1.state = busreq -> AF HGRANT1) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 15569 BDD nodes size of Y2 = 5.90296e+20 x, 26438 BDD nodes size of Y3 = 5.90296e+20 x, 29560 BDD nodes size of Y4 = 5.90296e+20 x, 33800 BDD nodes size of Y5 = 5.90296e+20 x, 33428 BDD nodes size of Y6 = 5.90296e+20 x, 34046 BDD nodes size of Y7 = 5.90296e+20 x, 34566 BDD nodes size of Y8 = 5.90296e+20 x, 36088 BDD nodes size of Y9 = 5.90296e+20 x, 36324 BDD nodes size of Y10 = 5.90296e+20 x, 36013 BDD nodes size of Y11 = 5.90296e+20 x, 35873 BDD nodes size of Y12 = 5.90296e+20 x, 34560 BDD nodes size of Y13 = 5.90296e+20 x, 33924 BDD nodes size of Y14 = 5.90296e+20 x, 33886 BDD nodes size of Y15 = 5.90296e+20 x, 33582 BDD nodes size of Y16 = 5.90296e+20 x, 33338 BDD nodes size of Y17 = 5.90296e+20 x, 33277 BDD nodes size of Y18 = 5.90296e+20 x, 33260 BDD nodes size of Y19 = 5.90296e+20 x, 33212 BDD nodes size of Y20 = 5.90296e+20 x, 33179 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 15729 BDD nodes size of Y2 = 5.90296e+20 x, 24800 BDD nodes size of Y3 = 5.90296e+20 x, 28603 BDD nodes size of Y4 = 5.90296e+20 x, 34451 BDD nodes size of Y5 = 5.90296e+20 x, 34292 BDD nodes size of Y6 = 5.90296e+20 x, 34449 BDD nodes size of Y7 = 5.90296e+20 x, 34139 BDD nodes size of Y8 = 5.90296e+20 x, 34812 BDD nodes size of Y9 = 5.90296e+20 x, 34145 BDD nodes size of Y10 = 5.90296e+20 x, 33834 BDD nodes size of Y11 = 5.90296e+20 x, 33729 BDD nodes size of Y12 = 5.90296e+20 x, 32595 BDD nodes size of Y13 = 5.90296e+20 x, 32174 BDD nodes size of Y14 = 5.90296e+20 x, 32124 BDD nodes size of Y15 = 5.90296e+20 x, 31777 BDD nodes size of Y16 = 5.90296e+20 x, 31561 BDD nodes size of Y17 = 5.90296e+20 x, 31483 BDD nodes size of Y18 = 5.90296e+20 x, 31430 BDD nodes size of Y19 = 5.90296e+20 x, 31395 BDD nodes size of Y20 = 5.90296e+20 x, 31375 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21604 BDD nodes size of Y2 = 5.90296e+20 x, 30336 BDD nodes size of Y3 = 5.90296e+20 x, 30125 BDD nodes size of Y4 = 5.90296e+20 x, 30479 BDD nodes size of Y5 = 5.90296e+20 x, 29913 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 20398 BDD nodes size of Y2 = 5.90296e+20 x, 30413 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 7467 BDD nodes size of res1 = 1.00472e+11 x, 35107 BDD nodes size of Y0 = 2.67711e+10 x, 13255 BDD nodes size of Y1 = 4.53814e+10 x, 23621 BDD nodes size of Y2 = 5.65968e+10 x, 31661 BDD nodes size of Y3 = 6.8734e+10 x, 33361 BDD nodes size of Y4 = 7.29256e+10 x, 36176 BDD nodes size of Y5 = 7.55228e+10 x, 36275 BDD nodes size of Y6 = 7.88101e+10 x, 36365 BDD nodes size of Y7 = 8.26648e+10 x, 36429 BDD nodes size of Y8 = 8.55353e+10 x, 37456 BDD nodes size of Y9 = 8.79869e+10 x, 37274 BDD nodes size of Y10 = 8.97805e+10 x, 36796 BDD nodes size of Y11 = 9.05454e+10 x, 36023 BDD nodes size of Y12 = 9.0915e+10 x, 35001 BDD nodes size of Y13 = 9.10576e+10 x, 34441 BDD nodes size of Y14 = 9.11342e+10 x, 34137 BDD nodes size of Y15 = 9.12049e+10 x, 33745 BDD nodes size of Y16 = 9.12312e+10 x, 33460 BDD nodes size of Y17 = 9.12348e+10 x, 33368 BDD nodes size of Y18 = 9.1238e+10 x, 33248 BDD nodes size of Y19 = 9.12401e+10 x, 33101 BDD nodes size of Y20 = 9.12406e+10 x, 33017 BDD nodes size of Y0 = 2.61986e+10 x, 12319 BDD nodes size of Y1 = 4.35128e+10 x, 21461 BDD nodes size of Y2 = 5.41842e+10 x, 26598 BDD nodes size of Y3 = 6.60757e+10 x, 29036 BDD nodes size of Y4 = 7.02296e+10 x, 32364 BDD nodes size of Y5 = 7.27654e+10 x, 32794 BDD nodes size of Y6 = 7.60291e+10 x, 32475 BDD nodes size of Y7 = 7.98838e+10 x, 32006 BDD nodes size of Y8 = 8.27543e+10 x, 32372 BDD nodes size of Y9 = 8.52058e+10 x, 32099 BDD nodes size of Y10 = 8.69994e+10 x, 31760 BDD nodes size of Y11 = 8.77644e+10 x, 31105 BDD nodes size of Y12 = 8.8134e+10 x, 29949 BDD nodes size of Y13 = 8.82766e+10 x, 29430 BDD nodes size of Y14 = 8.83531e+10 x, 29275 BDD nodes size of Y15 = 8.84239e+10 x, 28651 BDD nodes size of Y16 = 8.84501e+10 x, 28545 BDD nodes size of Y17 = 8.84538e+10 x, 28509 BDD nodes size of Y18 = 8.8457e+10 x, 28467 BDD nodes size of Y19 = 8.84591e+10 x, 28309 BDD nodes size of Y20 = 8.84596e+10 x, 28256 BDD nodes size of Y0 = 4.92873e+10 x, 9706 BDD nodes size of Y1 = 7.19147e+10 x, 25911 BDD nodes size of Y2 = 9.98683e+10 x, 35107 BDD nodes size of Y0 = 7.4777e+10 x, 32359 BDD nodes size of Y1 = 9.88082e+10 x, 33777 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master1.state = busreq -> AF HGRANT1) ... -- specification AG (master1.state = busreq -> AF HGRANT1) is true evaluating specification AG (master2.state = busreq -> AF HGRANT2) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 15302 BDD nodes size of Y2 = 5.90296e+20 x, 28078 BDD nodes size of Y3 = 5.90296e+20 x, 31643 BDD nodes size of Y4 = 5.90296e+20 x, 36529 BDD nodes size of Y5 = 5.90296e+20 x, 36369 BDD nodes size of Y6 = 5.90296e+20 x, 36637 BDD nodes size of Y7 = 5.90296e+20 x, 36927 BDD nodes size of Y8 = 5.90296e+20 x, 38190 BDD nodes size of Y9 = 5.90296e+20 x, 37638 BDD nodes size of Y10 = 5.90296e+20 x, 36894 BDD nodes size of Y11 = 5.90296e+20 x, 36433 BDD nodes size of Y12 = 5.90296e+20 x, 34782 BDD nodes size of Y13 = 5.90296e+20 x, 33941 BDD nodes size of Y14 = 5.90296e+20 x, 33805 BDD nodes size of Y15 = 5.90296e+20 x, 33409 BDD nodes size of Y16 = 5.90296e+20 x, 33006 BDD nodes size of Y17 = 5.90296e+20 x, 32890 BDD nodes size of Y18 = 5.90296e+20 x, 32825 BDD nodes size of Y19 = 5.90296e+20 x, 32785 BDD nodes size of Y20 = 5.90296e+20 x, 32758 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21402 BDD nodes size of Y2 = 5.90296e+20 x, 31981 BDD nodes size of Y3 = 5.90296e+20 x, 31713 BDD nodes size of Y4 = 5.90296e+20 x, 32100 BDD nodes size of Y5 = 5.90296e+20 x, 31509 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 15032 BDD nodes size of Y2 = 5.90296e+20 x, 23936 BDD nodes size of Y3 = 5.90296e+20 x, 29040 BDD nodes size of Y4 = 5.90296e+20 x, 36789 BDD nodes size of Y5 = 5.90296e+20 x, 37029 BDD nodes size of Y6 = 5.90296e+20 x, 36903 BDD nodes size of Y7 = 5.90296e+20 x, 36061 BDD nodes size of Y8 = 5.90296e+20 x, 36568 BDD nodes size of Y9 = 5.90296e+20 x, 36135 BDD nodes size of Y10 = 5.90296e+20 x, 36040 BDD nodes size of Y11 = 5.90296e+20 x, 35901 BDD nodes size of Y12 = 5.90296e+20 x, 34715 BDD nodes size of Y13 = 5.90296e+20 x, 34275 BDD nodes size of Y14 = 5.90296e+20 x, 34222 BDD nodes size of Y15 = 5.90296e+20 x, 33931 BDD nodes size of Y16 = 5.90296e+20 x, 33766 BDD nodes size of Y17 = 5.90296e+20 x, 33730 BDD nodes size of Y18 = 5.90296e+20 x, 33712 BDD nodes size of Y19 = 5.90296e+20 x, 33665 BDD nodes size of Y20 = 5.90296e+20 x, 33633 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 19861 BDD nodes size of Y2 = 5.90296e+20 x, 32296 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 7643 BDD nodes size of res1 = 1.00472e+11 x, 35132 BDD nodes size of Y0 = 2.61986e+10 x, 11557 BDD nodes size of Y1 = 4.35128e+10 x, 19782 BDD nodes size of Y2 = 5.41842e+10 x, 25852 BDD nodes size of Y3 = 6.60757e+10 x, 28240 BDD nodes size of Y4 = 7.02296e+10 x, 31416 BDD nodes size of Y5 = 7.27654e+10 x, 31860 BDD nodes size of Y6 = 7.60291e+10 x, 32043 BDD nodes size of Y7 = 7.98838e+10 x, 32230 BDD nodes size of Y8 = 8.27543e+10 x, 33221 BDD nodes size of Y9 = 8.52058e+10 x, 33334 BDD nodes size of Y10 = 8.69994e+10 x, 32850 BDD nodes size of Y11 = 8.77644e+10 x, 31833 BDD nodes size of Y12 = 8.8134e+10 x, 30385 BDD nodes size of Y13 = 8.82766e+10 x, 29518 BDD nodes size of Y14 = 8.83531e+10 x, 29087 BDD nodes size of Y15 = 8.84239e+10 x, 28046 BDD nodes size of Y16 = 8.84501e+10 x, 27832 BDD nodes size of Y17 = 8.84538e+10 x, 27832 BDD nodes size of Y18 = 8.8457e+10 x, 27791 BDD nodes size of Y19 = 8.84591e+10 x, 27508 BDD nodes size of Y20 = 8.84596e+10 x, 27392 BDD nodes size of Y0 = 2.67711e+10 x, 14058 BDD nodes size of Y1 = 4.53814e+10 x, 23263 BDD nodes size of Y2 = 5.65968e+10 x, 29346 BDD nodes size of Y3 = 6.8734e+10 x, 32381 BDD nodes size of Y4 = 7.29256e+10 x, 37202 BDD nodes size of Y5 = 7.55228e+10 x, 37769 BDD nodes size of Y6 = 7.88101e+10 x, 37221 BDD nodes size of Y7 = 8.26648e+10 x, 36357 BDD nodes size of Y8 = 8.55353e+10 x, 36785 BDD nodes size of Y9 = 8.79869e+10 x, 36174 BDD nodes size of Y10 = 8.97805e+10 x, 35829 BDD nodes size of Y11 = 9.05454e+10 x, 35033 BDD nodes size of Y12 = 9.0915e+10 x, 33856 BDD nodes size of Y13 = 9.10576e+10 x, 33372 BDD nodes size of Y14 = 9.11342e+10 x, 33145 BDD nodes size of Y15 = 9.12049e+10 x, 32774 BDD nodes size of Y16 = 9.12312e+10 x, 32593 BDD nodes size of Y17 = 9.12348e+10 x, 32527 BDD nodes size of Y18 = 9.1238e+10 x, 32408 BDD nodes size of Y19 = 9.12401e+10 x, 32271 BDD nodes size of Y20 = 9.12406e+10 x, 32204 BDD nodes size of Y0 = 4.92873e+10 x, 9214 BDD nodes size of Y1 = 7.19147e+10 x, 24460 BDD nodes size of Y2 = 9.98683e+10 x, 35132 BDD nodes size of Y0 = 7.4777e+10 x, 32335 BDD nodes size of Y1 = 9.88082e+10 x, 33705 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master2.state = busreq -> AF HGRANT2) ... -- specification AG (master2.state = busreq -> AF HGRANT2) is true evaluating specification AG (master3.state = busreq -> AF HGRANT3) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 20838 BDD nodes size of Y2 = 5.90296e+20 x, 33336 BDD nodes size of Y3 = 5.90296e+20 x, 33082 BDD nodes size of Y4 = 5.90296e+20 x, 33486 BDD nodes size of Y5 = 5.90296e+20 x, 32885 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 14565 BDD nodes size of Y2 = 5.90296e+20 x, 27202 BDD nodes size of Y3 = 5.90296e+20 x, 31479 BDD nodes size of Y4 = 5.90296e+20 x, 37894 BDD nodes size of Y5 = 5.90296e+20 x, 37953 BDD nodes size of Y6 = 5.90296e+20 x, 38142 BDD nodes size of Y7 = 5.90296e+20 x, 38064 BDD nodes size of Y8 = 5.90296e+20 x, 39472 BDD nodes size of Y9 = 5.90296e+20 x, 39422 BDD nodes size of Y10 = 5.90296e+20 x, 38740 BDD nodes size of Y11 = 5.90296e+20 x, 38386 BDD nodes size of Y12 = 5.90296e+20 x, 36945 BDD nodes size of Y13 = 5.90296e+20 x, 36174 BDD nodes size of Y14 = 5.90296e+20 x, 36075 BDD nodes size of Y15 = 5.90296e+20 x, 35757 BDD nodes size of Y16 = 5.90296e+20 x, 35462 BDD nodes size of Y17 = 5.90296e+20 x, 35386 BDD nodes size of Y18 = 5.90296e+20 x, 35374 BDD nodes size of Y19 = 5.90296e+20 x, 35326 BDD nodes size of Y20 = 5.90296e+20 x, 35297 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 14370 BDD nodes size of Y2 = 5.90296e+20 x, 25007 BDD nodes size of Y3 = 5.90296e+20 x, 30437 BDD nodes size of Y4 = 5.90296e+20 x, 38628 BDD nodes size of Y5 = 5.90296e+20 x, 38979 BDD nodes size of Y6 = 5.90296e+20 x, 38591 BDD nodes size of Y7 = 5.90296e+20 x, 37605 BDD nodes size of Y8 = 5.90296e+20 x, 38241 BDD nodes size of Y9 = 5.90296e+20 x, 37302 BDD nodes size of Y10 = 5.90296e+20 x, 36739 BDD nodes size of Y11 = 5.90296e+20 x, 36425 BDD nodes size of Y12 = 5.90296e+20 x, 35048 BDD nodes size of Y13 = 5.90296e+20 x, 34445 BDD nodes size of Y14 = 5.90296e+20 x, 34320 BDD nodes size of Y15 = 5.90296e+20 x, 33966 BDD nodes size of Y16 = 5.90296e+20 x, 33666 BDD nodes size of Y17 = 5.90296e+20 x, 33581 BDD nodes size of Y18 = 5.90296e+20 x, 33533 BDD nodes size of Y19 = 5.90296e+20 x, 33496 BDD nodes size of Y20 = 5.90296e+20 x, 33476 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 18937 BDD nodes size of Y2 = 5.90296e+20 x, 33623 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 7740 BDD nodes size of res1 = 1.00472e+11 x, 36695 BDD nodes size of Y0 = 2.67711e+10 x, 14052 BDD nodes size of Y1 = 4.53814e+10 x, 22904 BDD nodes size of Y2 = 5.65968e+10 x, 31547 BDD nodes size of Y3 = 6.8734e+10 x, 33856 BDD nodes size of Y4 = 7.29256e+10 x, 37988 BDD nodes size of Y5 = 7.55228e+10 x, 38329 BDD nodes size of Y6 = 7.88101e+10 x, 38281 BDD nodes size of Y7 = 8.26648e+10 x, 38175 BDD nodes size of Y8 = 8.55353e+10 x, 39568 BDD nodes size of Y9 = 8.79869e+10 x, 39246 BDD nodes size of Y10 = 8.97805e+10 x, 38722 BDD nodes size of Y11 = 9.05454e+10 x, 37644 BDD nodes size of Y12 = 9.0915e+10 x, 36367 BDD nodes size of Y13 = 9.10576e+10 x, 35611 BDD nodes size of Y14 = 9.11342e+10 x, 35184 BDD nodes size of Y15 = 9.12049e+10 x, 34716 BDD nodes size of Y16 = 9.12312e+10 x, 34361 BDD nodes size of Y17 = 9.12348e+10 x, 34252 BDD nodes size of Y18 = 9.1238e+10 x, 34094 BDD nodes size of Y19 = 9.12401e+10 x, 33883 BDD nodes size of Y20 = 9.12406e+10 x, 33775 BDD nodes size of Y0 = 2.61986e+10 x, 12815 BDD nodes size of Y1 = 4.35128e+10 x, 20244 BDD nodes size of Y2 = 5.41842e+10 x, 25219 BDD nodes size of Y3 = 6.60757e+10 x, 28368 BDD nodes size of Y4 = 7.02296e+10 x, 33090 BDD nodes size of Y5 = 7.27654e+10 x, 33816 BDD nodes size of Y6 = 7.60291e+10 x, 33339 BDD nodes size of Y7 = 7.98838e+10 x, 32695 BDD nodes size of Y8 = 8.27543e+10 x, 33469 BDD nodes size of Y9 = 8.52058e+10 x, 33106 BDD nodes size of Y10 = 8.69994e+10 x, 32674 BDD nodes size of Y11 = 8.77644e+10 x, 31584 BDD nodes size of Y12 = 8.8134e+10 x, 30140 BDD nodes size of Y13 = 8.82766e+10 x, 29421 BDD nodes size of Y14 = 8.83531e+10 x, 29146 BDD nodes size of Y15 = 8.84239e+10 x, 28324 BDD nodes size of Y16 = 8.84501e+10 x, 28150 BDD nodes size of Y17 = 8.84538e+10 x, 28128 BDD nodes size of Y18 = 8.8457e+10 x, 28092 BDD nodes size of Y19 = 8.84591e+10 x, 27879 BDD nodes size of Y20 = 8.84596e+10 x, 27802 BDD nodes size of Y0 = 4.92873e+10 x, 9020 BDD nodes size of Y1 = 7.19147e+10 x, 23257 BDD nodes size of Y2 = 9.98683e+10 x, 36695 BDD nodes size of Y0 = 7.4777e+10 x, 33865 BDD nodes size of Y1 = 9.88082e+10 x, 35269 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master3.state = busreq -> AF HGRANT3) ... -- specification AG (master3.state = busreq -> AF HGRANT3) is true evaluating specification AG (master1.state = busreq -> AF master1.state = write) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 22266 BDD nodes size of Y2 = 5.90296e+20 x, 39193 BDD nodes size of Y3 = 5.90296e+20 x, 42714 BDD nodes size of Y4 = 5.90296e+20 x, 47535 BDD nodes size of Y5 = 5.90296e+20 x, 47199 BDD nodes size of Y6 = 5.90296e+20 x, 47881 BDD nodes size of Y7 = 5.90296e+20 x, 50178 BDD nodes size of Y8 = 5.90296e+20 x, 49817 BDD nodes size of Y9 = 5.90296e+20 x, 49676 BDD nodes size of Y10 = 5.90296e+20 x, 49357 BDD nodes size of Y11 = 5.90296e+20 x, 49183 BDD nodes size of Y12 = 5.90296e+20 x, 47672 BDD nodes size of Y13 = 5.90296e+20 x, 47318 BDD nodes size of Y14 = 5.90296e+20 x, 47375 BDD nodes size of Y15 = 5.90296e+20 x, 47147 BDD nodes size of Y16 = 5.90296e+20 x, 47116 BDD nodes size of Y17 = 5.90296e+20 x, 47071 BDD nodes size of Y18 = 5.90296e+20 x, 47054 BDD nodes size of Y19 = 5.90296e+20 x, 47006 BDD nodes size of Y20 = 5.90296e+20 x, 46975 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 22303 BDD nodes size of Y2 = 5.90296e+20 x, 37280 BDD nodes size of Y3 = 5.90296e+20 x, 41401 BDD nodes size of Y4 = 5.90296e+20 x, 47688 BDD nodes size of Y5 = 5.90296e+20 x, 47611 BDD nodes size of Y6 = 5.90296e+20 x, 47894 BDD nodes size of Y7 = 5.90296e+20 x, 49450 BDD nodes size of Y8 = 5.90296e+20 x, 48137 BDD nodes size of Y9 = 5.90296e+20 x, 47265 BDD nodes size of Y10 = 5.90296e+20 x, 47005 BDD nodes size of Y11 = 5.90296e+20 x, 46939 BDD nodes size of Y12 = 5.90296e+20 x, 46091 BDD nodes size of Y13 = 5.90296e+20 x, 45422 BDD nodes size of Y14 = 5.90296e+20 x, 44715 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23104 BDD nodes size of Y2 = 5.90296e+20 x, 35652 BDD nodes size of Y3 = 5.90296e+20 x, 40288 BDD nodes size of Y4 = 5.90296e+20 x, 46326 BDD nodes size of Y5 = 5.90296e+20 x, 46090 BDD nodes size of Y6 = 5.90296e+20 x, 46105 BDD nodes size of Y7 = 5.90296e+20 x, 46055 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 26231 BDD nodes size of Y2 = 5.90296e+20 x, 43493 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 9861 BDD nodes size of res1 = 2.12597e+11 x, 55834 BDD nodes size of Y0 = 5.21912e+10 x, 17436 BDD nodes size of Y1 = 1.06262e+11 x, 36652 BDD nodes size of Y2 = 1.29383e+11 x, 53137 BDD nodes size of Y3 = 1.49692e+11 x, 55536 BDD nodes size of Y4 = 1.56313e+11 x, 58162 BDD nodes size of Y5 = 1.62025e+11 x, 58055 BDD nodes size of Y6 = 1.71525e+11 x, 58520 BDD nodes size of Y7 = 1.86106e+11 x, 60430 BDD nodes size of Y8 = 1.99605e+11 x, 59758 BDD nodes size of Y9 = 2.04766e+11 x, 59863 BDD nodes size of Y10 = 2.08157e+11 x, 59545 BDD nodes size of Y11 = 2.09596e+11 x, 59031 BDD nodes size of Y12 = 2.10079e+11 x, 57803 BDD nodes size of Y13 = 2.10229e+11 x, 57512 BDD nodes size of Y14 = 2.10307e+11 x, 57421 BDD nodes size of Y15 = 2.10378e+11 x, 57045 BDD nodes size of Y16 = 2.10404e+11 x, 57050 BDD nodes size of Y17 = 2.10408e+11 x, 57023 BDD nodes size of Y18 = 2.10411e+11 x, 57035 BDD nodes size of Y19 = 2.10413e+11 x, 56944 BDD nodes size of Y20 = 2.10414e+11 x, 56866 BDD nodes size of Y0 = 5.45584e+10 x, 16639 BDD nodes size of Y1 = 1.08387e+11 x, 34105 BDD nodes size of Y2 = 1.31111e+11 x, 47883 BDD nodes size of Y3 = 1.49015e+11 x, 51740 BDD nodes size of Y4 = 1.54692e+11 x, 56881 BDD nodes size of Y5 = 1.60581e+11 x, 57221 BDD nodes size of Y6 = 1.68766e+11 x, 57696 BDD nodes size of Y7 = 1.81449e+11 x, 59297 BDD nodes size of Y8 = 1.93543e+11 x, 59344 BDD nodes size of Y9 = 1.9971e+11 x, 59207 BDD nodes size of Y10 = 2.03327e+11 x, 58767 BDD nodes size of Y11 = 2.06594e+11 x, 58677 BDD nodes size of Y12 = 2.08663e+11 x, 58338 BDD nodes size of Y13 = 2.10677e+11 x, 57626 BDD nodes size of Y14 = 2.11278e+11 x, 57326 BDD nodes size of Y15 = 2.1141e+11 x, 56844 BDD nodes size of Y16 = 2.11473e+11 x, 56589 BDD nodes size of Y17 = 2.11494e+11 x, 56267 BDD nodes size of Y18 = 2.115e+11 x, 56057 BDD nodes size of Y19 = 2.11502e+11 x, 55904 BDD nodes size of Y20 = 2.11502e+11 x, 55839 BDD nodes size of Y0 = 9.08309e+09 x, 8592 BDD nodes size of Y1 = 1.22341e+10 x, 12428 BDD nodes size of Y2 = 1.31398e+10 x, 13549 BDD nodes size of Y3 = 1.32698e+10 x, 13460 BDD nodes size of Y0 = 1.0375e+11 x, 11766 BDD nodes size of Y1 = 1.44075e+11 x, 35418 BDD nodes size of Y2 = 2.11993e+11 x, 55836 BDD nodes size of Y0 = 1.60419e+11 x, 53821 BDD nodes size of Y1 = 2.12588e+11 x, 55823 BDD nodes size of Y2 = 2.12597e+11 x, 55834 BDD nodes size of res2 = 4.1867e+09 x, 5733 BDD nodes size of Y0 = 1.09052e+09 x, 1991 BDD nodes size of Y1 = 1.55189e+09 x, 2830 BDD nodes size of Y2 = 1.70184e+09 x, 3163 BDD nodes size of Y3 = 1.71862e+09 x, 3137 BDD nodes size of Y0 = 1.14583e+09 x, 2800 BDD nodes size of Y1 = 2.06858e+09 x, 4070 BDD nodes size of Y2 = 2.36847e+09 x, 4270 BDD nodes size of Y3 = 2.40203e+09 x, 4234 BDD nodes size of Y0 = 2.39914e+09 x, 1360 BDD nodes size of Y1 = 3.28099e+09 x, 4611 BDD nodes size of Y2 = 4.1867e+09 x, 5733 BDD nodes size of Y0 = 2.54253e+09 x, 4714 BDD nodes size of Y1 = 3.50722e+09 x, 5081 BDD nodes size of res3 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master1.state = busreq -> AF master1.state = write) ... -- specification AG (master1.state = busreq -> AF master1.state = write) is true evaluating specification AG (master2.state = busreq -> AF master2.state = write) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 22032 BDD nodes size of Y2 = 5.90296e+20 x, 39009 BDD nodes size of Y3 = 5.90296e+20 x, 42619 BDD nodes size of Y4 = 5.90296e+20 x, 47749 BDD nodes size of Y5 = 5.90296e+20 x, 47689 BDD nodes size of Y6 = 5.90296e+20 x, 48209 BDD nodes size of Y7 = 5.90296e+20 x, 50480 BDD nodes size of Y8 = 5.90296e+20 x, 49498 BDD nodes size of Y9 = 5.90296e+20 x, 48592 BDD nodes size of Y10 = 5.90296e+20 x, 47952 BDD nodes size of Y11 = 5.90296e+20 x, 47408 BDD nodes size of Y12 = 5.90296e+20 x, 46171 BDD nodes size of Y13 = 5.90296e+20 x, 45455 BDD nodes size of Y14 = 5.90296e+20 x, 44736 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23272 BDD nodes size of Y2 = 5.90296e+20 x, 37715 BDD nodes size of Y3 = 5.90296e+20 x, 41301 BDD nodes size of Y4 = 5.90296e+20 x, 46396 BDD nodes size of Y5 = 5.90296e+20 x, 46297 BDD nodes size of Y6 = 5.90296e+20 x, 46289 BDD nodes size of Y7 = 5.90296e+20 x, 46251 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21809 BDD nodes size of Y2 = 5.90296e+20 x, 34804 BDD nodes size of Y3 = 5.90296e+20 x, 40094 BDD nodes size of Y4 = 5.90296e+20 x, 48118 BDD nodes size of Y5 = 5.90296e+20 x, 48387 BDD nodes size of Y6 = 5.90296e+20 x, 48315 BDD nodes size of Y7 = 5.90296e+20 x, 49193 BDD nodes size of Y8 = 5.90296e+20 x, 47923 BDD nodes size of Y9 = 5.90296e+20 x, 47155 BDD nodes size of Y10 = 5.90296e+20 x, 47073 BDD nodes size of Y11 = 5.90296e+20 x, 46997 BDD nodes size of Y12 = 5.90296e+20 x, 45595 BDD nodes size of Y13 = 5.90296e+20 x, 45343 BDD nodes size of Y14 = 5.90296e+20 x, 45405 BDD nodes size of Y15 = 5.90296e+20 x, 45193 BDD nodes size of Y16 = 5.90296e+20 x, 45179 BDD nodes size of Y17 = 5.90296e+20 x, 45155 BDD nodes size of Y18 = 5.90296e+20 x, 45137 BDD nodes size of Y19 = 5.90296e+20 x, 45090 BDD nodes size of Y20 = 5.90296e+20 x, 45058 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 25973 BDD nodes size of Y2 = 5.90296e+20 x, 43308 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 9834 BDD nodes size of res1 = 2.12597e+11 x, 55845 BDD nodes size of Y0 = 5.45584e+10 x, 15948 BDD nodes size of Y1 = 1.08387e+11 x, 33674 BDD nodes size of Y2 = 1.31111e+11 x, 49944 BDD nodes size of Y3 = 1.49015e+11 x, 53059 BDD nodes size of Y4 = 1.54692e+11 x, 56536 BDD nodes size of Y5 = 1.60581e+11 x, 56522 BDD nodes size of Y6 = 1.68766e+11 x, 57536 BDD nodes size of Y7 = 1.81449e+11 x, 59808 BDD nodes size of Y8 = 1.93543e+11 x, 60234 BDD nodes size of Y9 = 1.9971e+11 x, 60733 BDD nodes size of Y10 = 2.03327e+11 x, 60024 BDD nodes size of Y11 = 2.06594e+11 x, 59674 BDD nodes size of Y12 = 2.08663e+11 x, 59132 BDD nodes size of Y13 = 2.10677e+11 x, 58361 BDD nodes size of Y14 = 2.11278e+11 x, 58045 BDD nodes size of Y15 = 2.1141e+11 x, 57424 BDD nodes size of Y16 = 2.11473e+11 x, 56932 BDD nodes size of Y17 = 2.11494e+11 x, 56514 BDD nodes size of Y18 = 2.115e+11 x, 56261 BDD nodes size of Y19 = 2.11502e+11 x, 56078 BDD nodes size of Y20 = 2.11502e+11 x, 55986 BDD nodes size of Y0 = 9.08309e+09 x, 8689 BDD nodes size of Y1 = 1.22341e+10 x, 13945 BDD nodes size of Y2 = 1.31398e+10 x, 15779 BDD nodes size of Y3 = 1.32698e+10 x, 15654 BDD nodes size of Y0 = 5.21912e+10 x, 17789 BDD nodes size of Y1 = 1.06262e+11 x, 36615 BDD nodes size of Y2 = 1.29383e+11 x, 48871 BDD nodes size of Y3 = 1.49692e+11 x, 52810 BDD nodes size of Y4 = 1.56313e+11 x, 58554 BDD nodes size of Y5 = 1.62025e+11 x, 58940 BDD nodes size of Y6 = 1.71525e+11 x, 58980 BDD nodes size of Y7 = 1.86106e+11 x, 60230 BDD nodes size of Y8 = 1.99605e+11 x, 59418 BDD nodes size of Y9 = 2.04766e+11 x, 59305 BDD nodes size of Y10 = 2.08157e+11 x, 59168 BDD nodes size of Y11 = 2.09596e+11 x, 58801 BDD nodes size of Y12 = 2.10079e+11 x, 57741 BDD nodes size of Y13 = 2.10229e+11 x, 57447 BDD nodes size of Y14 = 2.10307e+11 x, 57383 BDD nodes size of Y15 = 2.10378e+11 x, 57056 BDD nodes size of Y16 = 2.10404e+11 x, 57058 BDD nodes size of Y17 = 2.10408e+11 x, 57028 BDD nodes size of Y18 = 2.10411e+11 x, 57041 BDD nodes size of Y19 = 2.10413e+11 x, 56968 BDD nodes size of Y20 = 2.10414e+11 x, 56905 BDD nodes size of Y0 = 1.0375e+11 x, 11849 BDD nodes size of Y1 = 1.44075e+11 x, 35556 BDD nodes size of Y2 = 2.11993e+11 x, 55847 BDD nodes size of Y0 = 1.60419e+11 x, 53691 BDD nodes size of Y1 = 2.12588e+11 x, 55826 BDD nodes size of Y2 = 2.12597e+11 x, 55845 BDD nodes size of res2 = 4.1867e+09 x, 7847 BDD nodes size of Y0 = 1.14583e+09 x, 3531 BDD nodes size of Y1 = 2.06858e+09 x, 5289 BDD nodes size of Y2 = 2.36847e+09 x, 6185 BDD nodes size of Y3 = 2.40203e+09 x, 6126 BDD nodes size of Y0 = 1.09052e+09 x, 2695 BDD nodes size of Y1 = 1.55189e+09 x, 3795 BDD nodes size of Y2 = 1.70184e+09 x, 3995 BDD nodes size of Y3 = 1.71862e+09 x, 3959 BDD nodes size of Y0 = 2.39914e+09 x, 1596 BDD nodes size of Y1 = 3.28099e+09 x, 6011 BDD nodes size of Y2 = 4.1867e+09 x, 7847 BDD nodes size of Y0 = 2.54253e+09 x, 6695 BDD nodes size of Y1 = 3.50722e+09 x, 7156 BDD nodes size of res3 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master2.state = busreq -> AF master2.state = write) ... -- specification AG (master2.state = busreq -> AF master2.state = write) is true evaluating specification AG (master3.state = busreq -> AF master3.state = write) size of res0 = 2.36118e+21 x, 1 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 23094 BDD nodes size of Y2 = 5.90296e+20 x, 39417 BDD nodes size of Y3 = 5.90296e+20 x, 42488 BDD nodes size of Y4 = 5.90296e+20 x, 46781 BDD nodes size of Y5 = 5.90296e+20 x, 46856 BDD nodes size of Y6 = 5.90296e+20 x, 46832 BDD nodes size of Y7 = 5.90296e+20 x, 46802 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21821 BDD nodes size of Y2 = 5.90296e+20 x, 36941 BDD nodes size of Y3 = 5.90296e+20 x, 41154 BDD nodes size of Y4 = 5.90296e+20 x, 47685 BDD nodes size of Y5 = 5.90296e+20 x, 47783 BDD nodes size of Y6 = 5.90296e+20 x, 48129 BDD nodes size of Y7 = 5.90296e+20 x, 49614 BDD nodes size of Y8 = 5.90296e+20 x, 49308 BDD nodes size of Y9 = 5.90296e+20 x, 48610 BDD nodes size of Y10 = 5.90296e+20 x, 47930 BDD nodes size of Y11 = 5.90296e+20 x, 47571 BDD nodes size of Y12 = 5.90296e+20 x, 46001 BDD nodes size of Y13 = 5.90296e+20 x, 45547 BDD nodes size of Y14 = 5.90296e+20 x, 45589 BDD nodes size of Y15 = 5.90296e+20 x, 45349 BDD nodes size of Y16 = 5.90296e+20 x, 45335 BDD nodes size of Y17 = 5.90296e+20 x, 45289 BDD nodes size of Y18 = 5.90296e+20 x, 45277 BDD nodes size of Y19 = 5.90296e+20 x, 45229 BDD nodes size of Y20 = 5.90296e+20 x, 45200 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 21527 BDD nodes size of Y2 = 5.90296e+20 x, 34639 BDD nodes size of Y3 = 5.90296e+20 x, 39989 BDD nodes size of Y4 = 5.90296e+20 x, 48236 BDD nodes size of Y5 = 5.90296e+20 x, 48667 BDD nodes size of Y6 = 5.90296e+20 x, 48465 BDD nodes size of Y7 = 5.90296e+20 x, 49346 BDD nodes size of Y8 = 5.90296e+20 x, 47531 BDD nodes size of Y9 = 5.90296e+20 x, 46381 BDD nodes size of Y10 = 5.90296e+20 x, 46090 BDD nodes size of Y11 = 5.90296e+20 x, 45751 BDD nodes size of Y12 = 5.90296e+20 x, 44687 BDD nodes size of Y13 = 5.90296e+20 x, 44092 BDD nodes size of Y14 = 5.90296e+20 x, 43517 BDD nodes size of Y0 = 5.90296e+20 x, 3 BDD nodes size of Y1 = 5.90296e+20 x, 25653 BDD nodes size of Y2 = 5.90296e+20 x, 43149 BDD nodes size of Y0 = 1.18059e+21 x, 2 BDD nodes size of Y1 = 1.18059e+21 x, 9824 BDD nodes size of res1 = 2.12597e+11 x, 56108 BDD nodes size of Y0 = 9.08309e+09 x, 8261 BDD nodes size of Y1 = 1.22341e+10 x, 12905 BDD nodes size of Y2 = 1.31398e+10 x, 15284 BDD nodes size of Y3 = 1.32698e+10 x, 15161 BDD nodes size of Y0 = 5.21912e+10 x, 17593 BDD nodes size of Y1 = 1.06262e+11 x, 36329 BDD nodes size of Y2 = 1.29383e+11 x, 51623 BDD nodes size of Y3 = 1.49692e+11 x, 54365 BDD nodes size of Y4 = 1.56313e+11 x, 58530 BDD nodes size of Y5 = 1.62025e+11 x, 58593 BDD nodes size of Y6 = 1.71525e+11 x, 59201 BDD nodes size of Y7 = 1.86106e+11 x, 61026 BDD nodes size of Y8 = 1.99605e+11 x, 60739 BDD nodes size of Y9 = 2.04766e+11 x, 60960 BDD nodes size of Y10 = 2.08157e+11 x, 60546 BDD nodes size of Y11 = 2.09596e+11 x, 59864 BDD nodes size of Y12 = 2.10079e+11 x, 58506 BDD nodes size of Y13 = 2.10229e+11 x, 58094 BDD nodes size of Y14 = 2.10307e+11 x, 57994 BDD nodes size of Y15 = 2.10378e+11 x, 57554 BDD nodes size of Y16 = 2.10404e+11 x, 57576 BDD nodes size of Y17 = 2.10408e+11 x, 57547 BDD nodes size of Y18 = 2.10411e+11 x, 57565 BDD nodes size of Y19 = 2.10413e+11 x, 57474 BDD nodes size of Y20 = 2.10414e+11 x, 57398 BDD nodes size of Y0 = 5.45584e+10 x, 16331 BDD nodes size of Y1 = 1.08387e+11 x, 32995 BDD nodes size of Y2 = 1.31111e+11 x, 44716 BDD nodes size of Y3 = 1.49015e+11 x, 49652 BDD nodes size of Y4 = 1.54692e+11 x, 56684 BDD nodes size of Y5 = 1.60581e+11 x, 57404 BDD nodes size of Y6 = 1.68766e+11 x, 57890 BDD nodes size of Y7 = 1.81449e+11 x, 59504 BDD nodes size of Y8 = 1.93543e+11 x, 60059 BDD nodes size of Y9 = 1.9971e+11 x, 60181 BDD nodes size of Y10 = 2.03327e+11 x, 59721 BDD nodes size of Y11 = 2.06594e+11 x, 59525 BDD nodes size of Y12 = 2.08663e+11 x, 59072 BDD nodes size of Y13 = 2.10677e+11 x, 58308 BDD nodes size of Y14 = 2.11278e+11 x, 57973 BDD nodes size of Y15 = 2.1141e+11 x, 57461 BDD nodes size of Y16 = 2.11473e+11 x, 57092 BDD nodes size of Y17 = 2.11494e+11 x, 56738 BDD nodes size of Y18 = 2.115e+11 x, 56486 BDD nodes size of Y19 = 2.11502e+11 x, 56263 BDD nodes size of Y20 = 2.11502e+11 x, 56166 BDD nodes size of Y0 = 1.0375e+11 x, 11605 BDD nodes size of Y1 = 1.44075e+11 x, 34582 BDD nodes size of Y2 = 2.11993e+11 x, 56109 BDD nodes size of Y0 = 1.60419e+11 x, 53980 BDD nodes size of Y1 = 2.12588e+11 x, 56104 BDD nodes size of Y2 = 2.12597e+11 x, 56108 BDD nodes size of res2 = 4.1867e+09 x, 7797 BDD nodes size of Y0 = 1.09052e+09 x, 2462 BDD nodes size of Y1 = 1.55189e+09 x, 3551 BDD nodes size of Y2 = 1.70184e+09 x, 4249 BDD nodes size of Y3 = 1.71862e+09 x, 4210 BDD nodes size of Y0 = 1.14583e+09 x, 3674 BDD nodes size of Y1 = 2.06858e+09 x, 5045 BDD nodes size of Y2 = 2.36847e+09 x, 5477 BDD nodes size of Y3 = 2.40203e+09 x, 5435 BDD nodes size of Y0 = 2.39914e+09 x, 1467 BDD nodes size of Y1 = 3.28099e+09 x, 5418 BDD nodes size of Y2 = 4.1867e+09 x, 7797 BDD nodes size of Y0 = 2.54253e+09 x, 6767 BDD nodes size of Y1 = 3.50722e+09 x, 7223 BDD nodes size of res3 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (master3.state = busreq -> AF master3.state = write) ... -- specification AG (master3.state = busreq -> AF master3.state = write) is true ###################################################################### Runtime Statistics ------------------ Machine name: node-xeon-8 User time 1015.850 seconds System time 1.240 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 26385K data size initialized = 234K data size uninitialized = 362K data size sbrk = 25789K Virtual memory limit = 4194304K (4194304K) Major page faults = 400 Minor page faults = 80707 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 521485 -------------------- BDD nodes representing init set of states: 44 BDD nodes representing state constraints: 8806 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2181 cluster 3 : 1927 cluster 4 : 4667 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 45 cluster 2 : 2181 cluster 3 : 1927 cluster 4 : 4667