*** 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_Dedicated_State_Wires.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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 27458 BDD nodes size of Y2 = 3.68935e+19 x, 49250 BDD nodes size of Y3 = 3.68935e+19 x, 63906 BDD nodes size of Y4 = 3.68935e+19 x, 74327 BDD nodes size of Y5 = 3.68935e+19 x, 82990 BDD nodes size of Y6 = 3.68935e+19 x, 91797 BDD nodes size of Y7 = 3.68935e+19 x, 89857 BDD nodes size of Y8 = 3.68935e+19 x, 91463 BDD nodes size of Y9 = 3.68935e+19 x, 90796 BDD nodes size of Y10 = 3.68935e+19 x, 88979 BDD nodes size of Y11 = 3.68935e+19 x, 86044 BDD nodes size of Y12 = 3.68935e+19 x, 83426 BDD nodes size of Y13 = 3.68935e+19 x, 82953 BDD nodes size of Y14 = 3.68935e+19 x, 82884 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 28228 BDD nodes size of Y2 = 3.68935e+19 x, 49788 BDD nodes size of Y3 = 3.68935e+19 x, 63640 BDD nodes size of Y4 = 3.68935e+19 x, 74771 BDD nodes size of Y5 = 3.68935e+19 x, 84222 BDD nodes size of Y6 = 3.68935e+19 x, 92987 BDD nodes size of Y7 = 3.68935e+19 x, 90678 BDD nodes size of Y8 = 3.68935e+19 x, 92308 BDD nodes size of Y9 = 3.68935e+19 x, 91387 BDD nodes size of Y10 = 3.68935e+19 x, 89528 BDD nodes size of Y11 = 3.68935e+19 x, 86211 BDD nodes size of Y12 = 3.68935e+19 x, 83217 BDD nodes size of Y13 = 3.68935e+19 x, 82623 BDD nodes size of Y14 = 3.68935e+19 x, 82544 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 28242 BDD nodes size of Y2 = 3.68935e+19 x, 49778 BDD nodes size of Y3 = 3.68935e+19 x, 65456 BDD nodes size of Y4 = 3.68935e+19 x, 78650 BDD nodes size of Y5 = 3.68935e+19 x, 89110 BDD nodes size of Y6 = 3.68935e+19 x, 96545 BDD nodes size of Y7 = 3.68935e+19 x, 92631 BDD nodes size of Y8 = 3.68935e+19 x, 93999 BDD nodes size of Y9 = 3.68935e+19 x, 91143 BDD nodes size of Y10 = 3.68935e+19 x, 88546 BDD nodes size of Y11 = 3.68935e+19 x, 85191 BDD nodes size of Y12 = 3.68935e+19 x, 83154 BDD nodes size of Y13 = 3.68935e+19 x, 82776 BDD nodes size of Y14 = 3.68935e+19 x, 82666 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 42441 BDD nodes size of Y2 = 3.68935e+19 x, 21245 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 21220 BDD nodes size of res1 = 8.76372e+08 x, 123438 BDD nodes size of Y0 = 1.63398e+08 x, 33549 BDD nodes size of Y1 = 2.76972e+08 x, 56064 BDD nodes size of Y2 = 3.25198e+08 x, 66093 BDD nodes size of Y3 = 3.96583e+08 x, 89596 BDD nodes size of Y4 = 4.4313e+08 x, 100627 BDD nodes size of Y5 = 4.70204e+08 x, 111666 BDD nodes size of Y6 = 5.14224e+08 x, 126691 BDD nodes size of Y7 = 5.82685e+08 x, 130900 BDD nodes size of Y8 = 6.1993e+08 x, 133882 BDD nodes size of Y9 = 6.44301e+08 x, 131570 BDD nodes size of Y10 = 6.58735e+08 x, 131557 BDD nodes size of Y11 = 6.67255e+08 x, 130737 BDD nodes size of Y12 = 6.76442e+08 x, 129440 BDD nodes size of Y13 = 6.83307e+08 x, 124918 BDD nodes size of Y14 = 6.84884e+08 x, 123645 BDD nodes size of Y15 = 6.85613e+08 x, 122852 BDD nodes size of Y16 = 6.85654e+08 x, 122738 BDD nodes size of Y0 = 1.63398e+08 x, 32321 BDD nodes size of Y1 = 2.76972e+08 x, 54118 BDD nodes size of Y2 = 3.25198e+08 x, 64394 BDD nodes size of Y3 = 3.96583e+08 x, 87812 BDD nodes size of Y4 = 4.4313e+08 x, 99605 BDD nodes size of Y5 = 4.70204e+08 x, 110929 BDD nodes size of Y6 = 5.14224e+08 x, 127039 BDD nodes size of Y7 = 5.82685e+08 x, 131633 BDD nodes size of Y8 = 6.1993e+08 x, 134735 BDD nodes size of Y9 = 6.44301e+08 x, 132460 BDD nodes size of Y10 = 6.58735e+08 x, 132712 BDD nodes size of Y11 = 6.67255e+08 x, 131616 BDD nodes size of Y12 = 6.76442e+08 x, 129954 BDD nodes size of Y13 = 6.83307e+08 x, 124869 BDD nodes size of Y14 = 6.84884e+08 x, 123362 BDD nodes size of Y15 = 6.85613e+08 x, 122606 BDD nodes size of Y16 = 6.85654e+08 x, 122520 BDD nodes size of Y0 = 1.63398e+08 x, 31282 BDD nodes size of Y1 = 2.76972e+08 x, 52694 BDD nodes size of Y2 = 3.25198e+08 x, 64445 BDD nodes size of Y3 = 3.96583e+08 x, 88427 BDD nodes size of Y4 = 4.4313e+08 x, 101653 BDD nodes size of Y5 = 4.70204e+08 x, 114255 BDD nodes size of Y6 = 5.14224e+08 x, 131248 BDD nodes size of Y7 = 5.82685e+08 x, 135719 BDD nodes size of Y8 = 6.1993e+08 x, 137705 BDD nodes size of Y9 = 6.44301e+08 x, 133935 BDD nodes size of Y10 = 6.58735e+08 x, 133088 BDD nodes size of Y11 = 6.67255e+08 x, 130340 BDD nodes size of Y12 = 6.76442e+08 x, 128647 BDD nodes size of Y13 = 6.83307e+08 x, 125034 BDD nodes size of Y14 = 6.84884e+08 x, 123733 BDD nodes size of Y15 = 6.85613e+08 x, 122904 BDD nodes size of Y16 = 6.85654e+08 x, 122868 BDD nodes size of Y0 = 4.08232e+08 x, 38150 BDD nodes size of Y1 = 6.08338e+08 x, 114548 BDD nodes size of Y2 = 8.00506e+08 x, 117925 BDD nodes size of Y0 = 6.80059e+08 x, 121290 BDD nodes size of Y1 = 8.7158e+08 x, 122896 BDD nodes size of Y2 = 8.72759e+08 x, 122987 BDD nodes size of res2 = 4.57376e+08 x, 109600 BDD nodes size of Y0 = 7.87988e+07 x, 27801 BDD nodes size of Y1 = 1.47644e+08 x, 45927 BDD nodes size of Y2 = 1.77521e+08 x, 55485 BDD nodes size of Y3 = 2.30859e+08 x, 74307 BDD nodes size of Y4 = 2.67149e+08 x, 82589 BDD nodes size of Y5 = 2.86503e+08 x, 89555 BDD nodes size of Y6 = 3.06688e+08 x, 97549 BDD nodes size of Y7 = 3.36814e+08 x, 101548 BDD nodes size of Y8 = 3.59485e+08 x, 103320 BDD nodes size of Y9 = 3.75382e+08 x, 103558 BDD nodes size of Y10 = 3.87662e+08 x, 104218 BDD nodes size of Y11 = 3.95526e+08 x, 103454 BDD nodes size of Y12 = 4.02469e+08 x, 103268 BDD nodes size of Y13 = 4.09113e+08 x, 98807 BDD nodes size of Y14 = 4.10976e+08 x, 97572 BDD nodes size of Y15 = 4.12303e+08 x, 95817 BDD nodes size of Y16 = 4.12795e+08 x, 95183 BDD nodes size of Y0 = 7.87988e+07 x, 27383 BDD nodes size of Y1 = 1.47644e+08 x, 45021 BDD nodes size of Y2 = 1.77521e+08 x, 54574 BDD nodes size of Y3 = 2.30859e+08 x, 73696 BDD nodes size of Y4 = 2.67149e+08 x, 82986 BDD nodes size of Y5 = 2.86503e+08 x, 90317 BDD nodes size of Y6 = 3.06688e+08 x, 98904 BDD nodes size of Y7 = 3.36814e+08 x, 103405 BDD nodes size of Y8 = 3.59485e+08 x, 104739 BDD nodes size of Y9 = 3.75382e+08 x, 105194 BDD nodes size of Y10 = 3.87662e+08 x, 106234 BDD nodes size of Y11 = 3.95526e+08 x, 104945 BDD nodes size of Y12 = 4.02469e+08 x, 104585 BDD nodes size of Y13 = 4.09113e+08 x, 99658 BDD nodes size of Y14 = 4.10976e+08 x, 98442 BDD nodes size of Y15 = 4.12303e+08 x, 96816 BDD nodes size of Y16 = 4.12795e+08 x, 96272 BDD nodes size of Y0 = 7.87988e+07 x, 26577 BDD nodes size of Y1 = 1.47644e+08 x, 44013 BDD nodes size of Y2 = 1.77521e+08 x, 53824 BDD nodes size of Y3 = 2.30859e+08 x, 73304 BDD nodes size of Y4 = 2.67149e+08 x, 83760 BDD nodes size of Y5 = 2.86503e+08 x, 92290 BDD nodes size of Y6 = 3.06688e+08 x, 101388 BDD nodes size of Y7 = 3.36814e+08 x, 105051 BDD nodes size of Y8 = 3.59485e+08 x, 104932 BDD nodes size of Y9 = 3.75382e+08 x, 105040 BDD nodes size of Y10 = 3.87662e+08 x, 105862 BDD nodes size of Y11 = 3.95526e+08 x, 103414 BDD nodes size of Y12 = 4.02469e+08 x, 102669 BDD nodes size of Y13 = 4.09113e+08 x, 98771 BDD nodes size of Y14 = 4.10976e+08 x, 97601 BDD nodes size of Y15 = 4.12303e+08 x, 96214 BDD nodes size of Y16 = 4.12795e+08 x, 95934 BDD nodes size of Y0 = 2.34406e+08 x, 29328 BDD nodes size of Y1 = 3.46542e+08 x, 95055 BDD nodes size of Y2 = 4.54722e+08 x, 107282 BDD nodes size of Y0 = 3.41549e+08 x, 106883 BDD nodes size of Y1 = 4.55803e+08 x, 109291 BDD nodes size of Y2 = 4.57376e+08 x, 109600 BDD nodes size of res3 = 3.73498e+08 x, 76780 BDD nodes size of Y0 = 6.44055e+07 x, 19160 BDD nodes size of Y1 = 1.2981e+08 x, 36608 BDD nodes size of Y2 = 1.55558e+08 x, 45717 BDD nodes size of Y3 = 1.99131e+08 x, 60929 BDD nodes size of Y4 = 2.304e+08 x, 67642 BDD nodes size of Y5 = 2.49344e+08 x, 74446 BDD nodes size of Y6 = 2.68333e+08 x, 80519 BDD nodes size of Y7 = 2.97673e+08 x, 83463 BDD nodes size of Y8 = 3.19894e+08 x, 84900 BDD nodes size of Y9 = 3.35839e+08 x, 84853 BDD nodes size of Y10 = 3.48127e+08 x, 86721 BDD nodes size of Y11 = 3.55983e+08 x, 85441 BDD nodes size of Y12 = 3.62951e+08 x, 85365 BDD nodes size of Y13 = 3.6975e+08 x, 80718 BDD nodes size of Y14 = 3.7163e+08 x, 79051 BDD nodes size of Y15 = 3.72957e+08 x, 77174 BDD nodes size of Y16 = 3.73449e+08 x, 76540 BDD nodes size of Y0 = 6.44055e+07 x, 18628 BDD nodes size of Y1 = 1.2981e+08 x, 35308 BDD nodes size of Y2 = 1.55558e+08 x, 44425 BDD nodes size of Y3 = 1.99131e+08 x, 59749 BDD nodes size of Y4 = 2.304e+08 x, 67268 BDD nodes size of Y5 = 2.49344e+08 x, 74464 BDD nodes size of Y6 = 2.68333e+08 x, 80998 BDD nodes size of Y7 = 2.97673e+08 x, 84211 BDD nodes size of Y8 = 3.19894e+08 x, 85459 BDD nodes size of Y9 = 3.35839e+08 x, 85585 BDD nodes size of Y10 = 3.48127e+08 x, 87328 BDD nodes size of Y11 = 3.55983e+08 x, 85686 BDD nodes size of Y12 = 3.62951e+08 x, 85426 BDD nodes size of Y13 = 3.6975e+08 x, 80405 BDD nodes size of Y14 = 3.7163e+08 x, 78793 BDD nodes size of Y15 = 3.72957e+08 x, 77070 BDD nodes size of Y16 = 3.73449e+08 x, 76526 BDD nodes size of Y0 = 6.44055e+07 x, 18242 BDD nodes size of Y1 = 1.2981e+08 x, 34554 BDD nodes size of Y2 = 1.55558e+08 x, 44011 BDD nodes size of Y3 = 1.99131e+08 x, 59164 BDD nodes size of Y4 = 2.304e+08 x, 67776 BDD nodes size of Y5 = 2.49344e+08 x, 75916 BDD nodes size of Y6 = 2.68333e+08 x, 83031 BDD nodes size of Y7 = 2.97673e+08 x, 85765 BDD nodes size of Y8 = 3.19894e+08 x, 85859 BDD nodes size of Y9 = 3.35839e+08 x, 85892 BDD nodes size of Y10 = 3.48127e+08 x, 87089 BDD nodes size of Y11 = 3.55983e+08 x, 84554 BDD nodes size of Y12 = 3.62951e+08 x, 83610 BDD nodes size of Y13 = 3.6975e+08 x, 79588 BDD nodes size of Y14 = 3.7163e+08 x, 78263 BDD nodes size of Y15 = 3.72957e+08 x, 76796 BDD nodes size of Y16 = 3.73449e+08 x, 76516 BDD nodes size of Y0 = 1.91644e+08 x, 21011 BDD nodes size of Y1 = 2.85692e+08 x, 69520 BDD nodes size of Y2 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 2.76005e+08 x, 75604 BDD nodes size of Y1 = 3.71925e+08 x, 76476 BDD nodes size of Y2 = 3.73498e+08 x, 76780 BDD nodes size of res4 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 6.43809e+07 x, 18996 BDD nodes size of Y1 = 1.29786e+08 x, 36473 BDD nodes size of Y2 = 1.55533e+08 x, 45591 BDD nodes size of Y3 = 1.99107e+08 x, 60794 BDD nodes size of Y4 = 2.30375e+08 x, 67507 BDD nodes size of Y5 = 2.49319e+08 x, 74398 BDD nodes size of Y6 = 2.68308e+08 x, 80471 BDD nodes size of Y7 = 2.97648e+08 x, 83415 BDD nodes size of Y8 = 3.19869e+08 x, 84852 BDD nodes size of Y9 = 3.35815e+08 x, 84805 BDD nodes size of Y10 = 3.48103e+08 x, 86673 BDD nodes size of Y11 = 3.55959e+08 x, 85393 BDD nodes size of Y12 = 3.62926e+08 x, 85313 BDD nodes size of Y13 = 3.69725e+08 x, 80579 BDD nodes size of Y14 = 3.71606e+08 x, 78912 BDD nodes size of Y15 = 3.72933e+08 x, 77035 BDD nodes size of Y16 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 6.43809e+07 x, 18482 BDD nodes size of Y1 = 1.29786e+08 x, 35183 BDD nodes size of Y2 = 1.55533e+08 x, 44323 BDD nodes size of Y3 = 1.99107e+08 x, 59624 BDD nodes size of Y4 = 2.30375e+08 x, 67143 BDD nodes size of Y5 = 2.49319e+08 x, 74412 BDD nodes size of Y6 = 2.68308e+08 x, 80946 BDD nodes size of Y7 = 2.97648e+08 x, 84159 BDD nodes size of Y8 = 3.19869e+08 x, 85407 BDD nodes size of Y9 = 3.35815e+08 x, 85533 BDD nodes size of Y10 = 3.48103e+08 x, 87276 BDD nodes size of Y11 = 3.55959e+08 x, 85634 BDD nodes size of Y12 = 3.62926e+08 x, 85374 BDD nodes size of Y13 = 3.69725e+08 x, 80280 BDD nodes size of Y14 = 3.71606e+08 x, 78668 BDD nodes size of Y15 = 3.72933e+08 x, 76945 BDD nodes size of Y16 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 6.43809e+07 x, 18110 BDD nodes size of Y1 = 1.29786e+08 x, 34439 BDD nodes size of Y2 = 1.55533e+08 x, 43927 BDD nodes size of Y3 = 1.99107e+08 x, 59049 BDD nodes size of Y4 = 2.30375e+08 x, 67661 BDD nodes size of Y5 = 2.49319e+08 x, 75860 BDD nodes size of Y6 = 2.68308e+08 x, 82975 BDD nodes size of Y7 = 2.97648e+08 x, 85709 BDD nodes size of Y8 = 3.19869e+08 x, 85803 BDD nodes size of Y9 = 3.35815e+08 x, 85836 BDD nodes size of Y10 = 3.48103e+08 x, 87033 BDD nodes size of Y11 = 3.55959e+08 x, 84498 BDD nodes size of Y12 = 3.62926e+08 x, 83554 BDD nodes size of Y13 = 3.69725e+08 x, 79473 BDD nodes size of Y14 = 3.71606e+08 x, 78148 BDD nodes size of Y15 = 3.72933e+08 x, 76681 BDD nodes size of Y16 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 1.91644e+08 x, 21011 BDD nodes size of Y1 = 2.85692e+08 x, 69520 BDD nodes size of Y2 = 3.73424e+08 x, 76401 BDD nodes size of Y0 = 2.75931e+08 x, 75225 BDD nodes size of Y1 = 3.71851e+08 x, 76097 BDD nodes size of Y2 = 3.73424e+08 x, 76401 BDD nodes done eu: computing fixed point approximations for AG master1.state != error ... size of Y1 = 1.15558e+06 states, 2698 BDD nodes size of Y2 = 6.17984e+06 states, 8994 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.15558e+06 states, 1798 BDD nodes size of Y2 = 6.17984e+06 states, 8221 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.15558e+06 states, 1662 BDD nodes size of Y2 = 6.17984e+06 states, 8588 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 = 6.93053e+07 states, 32531 BDD nodes size of Y2 = 9.32229e+07 states, 54742 BDD nodes size of Y3 = 1.18575e+08 states, 62567 BDD nodes size of Y4 = 1.37563e+08 states, 71830 BDD nodes size of Y5 = 1.39956e+08 states, 73220 BDD nodes -- specification AG slave.state != error is true evaluating specification EF (MASK_MASTER1 & MASK_MASTER2) eu: computing fixed point approximations for EF (MASK_MASTER1 & MASK_MASTER2) ... size of Y1 = 1.83828e+08 states, 29628 BDD nodes size of Y2 = 2.00212e+08 states, 36072 BDD nodes size of Y3 = 2.14958e+08 states, 42951 BDD nodes size of Y4 = 2.37126e+08 states, 57897 BDD nodes size of Y5 = 2.53297e+08 states, 65312 BDD nodes size of Y6 = 2.63127e+08 states, 72270 BDD nodes size of Y7 = 2.77266e+08 states, 79258 BDD nodes size of Y8 = 2.98492e+08 states, 78137 BDD nodes size of Y9 = 3.13352e+08 states, 82379 BDD nodes size of Y10 = 3.28372e+08 states, 83222 BDD nodes size of Y11 = 3.40271e+08 states, 84664 BDD nodes size of Y12 = 3.50765e+08 states, 87923 BDD nodes size of Y13 = 3.5983e+08 states, 86186 BDD nodes size of Y14 = 3.65515e+08 states, 83977 BDD nodes size of Y15 = 3.68792e+08 states, 82800 BDD nodes size of Y16 = 3.71778e+08 states, 79100 BDD nodes size of Y17 = 3.73047e+08 states, 77396 BDD nodes size of Y18 = 3.73383e+08 states, 76517 BDD nodes size of Y19 = 3.73424e+08 states, 76401 BDD nodes -- specification EF (MASK_MASTER1 & MASK_MASTER2) is true evaluating specification AG ((MASK_MASTER1 & MASK_MASTER2) -> AF (!MASK_MASTER1 | !MASK_MASTER2)) size of res0 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 14412 BDD nodes size of Y2 = 3.68935e+19 x, 17244 BDD nodes size of Y3 = 3.68935e+19 x, 21921 BDD nodes size of Y4 = 3.68935e+19 x, 22050 BDD nodes size of Y5 = 3.68935e+19 x, 22115 BDD nodes size of Y6 = 3.68935e+19 x, 22772 BDD nodes size of Y7 = 3.68935e+19 x, 22527 BDD nodes size of Y8 = 3.68935e+19 x, 22673 BDD nodes size of Y9 = 3.68935e+19 x, 21776 BDD nodes size of Y10 = 3.68935e+19 x, 21660 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 23364 BDD nodes size of Y2 = 3.68935e+19 x, 24683 BDD nodes size of Y3 = 3.68935e+19 x, 23926 BDD nodes size of Y4 = 3.68935e+19 x, 23912 BDD nodes size of Y5 = 3.68935e+19 x, 23769 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 23592 BDD nodes size of Y2 = 3.68935e+19 x, 24935 BDD nodes size of Y3 = 3.68935e+19 x, 24156 BDD nodes size of Y4 = 3.68935e+19 x, 24143 BDD nodes size of Y5 = 3.68935e+19 x, 24000 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 14264 BDD nodes size of Y2 = 3.68935e+19 x, 20162 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 7471 BDD nodes size of res1 = 7.66607e+07 x, 18459 BDD nodes size of Y0 = 4.17219e+07 x, 8283 BDD nodes size of Y1 = 4.73416e+07 x, 11410 BDD nodes size of Y2 = 5.21585e+07 x, 14238 BDD nodes size of Y3 = 6.04815e+07 x, 18763 BDD nodes size of Y4 = 6.47905e+07 x, 18878 BDD nodes size of Y5 = 6.61955e+07 x, 18938 BDD nodes size of Y6 = 6.93166e+07 x, 19841 BDD nodes size of Y7 = 7.29211e+07 x, 19330 BDD nodes size of Y8 = 7.47438e+07 x, 19472 BDD nodes size of Y9 = 7.63658e+07 x, 18575 BDD nodes size of Y10 = 7.66607e+07 x, 18459 BDD nodes size of Y0 = 3.96657e+07 x, 5776 BDD nodes size of Y1 = 5.97811e+07 x, 15841 BDD nodes size of Y2 = 7.66607e+07 x, 18459 BDD nodes size of Y0 = 5.68279e+07 x, 18445 BDD nodes size of Y1 = 7.66607e+07 x, 18459 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((MASK_MASTER1 & MASK_MASTER2) -> AF (!MASK_MASTER1 | !MASK_MASTER2)) ... -- specification AG ((MASK_MASTER1 & MASK_MASTER2) -> AF (!MASK_MASTER1 | !MASK_MASTER2)) is true evaluating specification EF (MASK_MASTER1 & MASK_MASTER3) eu: computing fixed point approximations for EF (MASK_MASTER1 & MASK_MASTER3) ... size of Y1 = 1.83828e+08 states, 28977 BDD nodes size of Y2 = 2.00212e+08 states, 35503 BDD nodes size of Y3 = 2.14958e+08 states, 42401 BDD nodes size of Y4 = 2.37126e+08 states, 57213 BDD nodes size of Y5 = 2.53297e+08 states, 64157 BDD nodes size of Y6 = 2.63127e+08 states, 71275 BDD nodes size of Y7 = 2.77266e+08 states, 78563 BDD nodes size of Y8 = 2.98492e+08 states, 77518 BDD nodes size of Y9 = 3.13352e+08 states, 82170 BDD nodes size of Y10 = 3.28372e+08 states, 83892 BDD nodes size of Y11 = 3.40271e+08 states, 85389 BDD nodes size of Y12 = 3.50765e+08 states, 88353 BDD nodes size of Y13 = 3.5983e+08 states, 86586 BDD nodes size of Y14 = 3.65515e+08 states, 84392 BDD nodes size of Y15 = 3.68792e+08 states, 83369 BDD nodes size of Y16 = 3.71778e+08 states, 79481 BDD nodes size of Y17 = 3.73047e+08 states, 77534 BDD nodes size of Y18 = 3.73383e+08 states, 76562 BDD nodes size of Y19 = 3.73424e+08 states, 76401 BDD nodes -- specification EF (MASK_MASTER1 & MASK_MASTER3) is true evaluating specification AG ((MASK_MASTER1 & MASK_MASTER3) -> AF (!MASK_MASTER1 | !MASK_MASTER3)) size of res0 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 22297 BDD nodes size of Y2 = 3.68935e+19 x, 23518 BDD nodes size of Y3 = 3.68935e+19 x, 22850 BDD nodes size of Y4 = 3.68935e+19 x, 22802 BDD nodes size of Y5 = 3.68935e+19 x, 22649 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 14470 BDD nodes size of Y2 = 3.68935e+19 x, 17055 BDD nodes size of Y3 = 3.68935e+19 x, 21533 BDD nodes size of Y4 = 3.68935e+19 x, 22260 BDD nodes size of Y5 = 3.68935e+19 x, 22467 BDD nodes size of Y6 = 3.68935e+19 x, 23172 BDD nodes size of Y7 = 3.68935e+19 x, 22901 BDD nodes size of Y8 = 3.68935e+19 x, 22972 BDD nodes size of Y9 = 3.68935e+19 x, 21745 BDD nodes size of Y10 = 3.68935e+19 x, 21545 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 23218 BDD nodes size of Y2 = 3.68935e+19 x, 24453 BDD nodes size of Y3 = 3.68935e+19 x, 23769 BDD nodes size of Y4 = 3.68935e+19 x, 23721 BDD nodes size of Y5 = 3.68935e+19 x, 23568 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 13530 BDD nodes size of Y2 = 3.68935e+19 x, 19542 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 7043 BDD nodes size of res1 = 7.66607e+07 x, 17645 BDD nodes size of Y0 = 4.17219e+07 x, 8030 BDD nodes size of Y1 = 4.73416e+07 x, 10859 BDD nodes size of Y2 = 5.21585e+07 x, 13440 BDD nodes size of Y3 = 6.04815e+07 x, 17803 BDD nodes size of Y4 = 6.47905e+07 x, 18450 BDD nodes size of Y5 = 6.61955e+07 x, 18614 BDD nodes size of Y6 = 6.93166e+07 x, 19557 BDD nodes size of Y7 = 7.29211e+07 x, 19021 BDD nodes size of Y8 = 7.47438e+07 x, 19072 BDD nodes size of Y9 = 7.63658e+07 x, 17845 BDD nodes size of Y10 = 7.66607e+07 x, 17645 BDD nodes size of Y0 = 3.96657e+07 x, 5433 BDD nodes size of Y1 = 5.97811e+07 x, 14962 BDD nodes size of Y2 = 7.66607e+07 x, 17645 BDD nodes size of Y0 = 5.68279e+07 x, 17631 BDD nodes size of Y1 = 7.66607e+07 x, 17645 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((MASK_MASTER1 & MASK_MASTER3) -> AF (!MASK_MASTER1 | !MASK_MASTER3)) ... -- specification AG ((MASK_MASTER1 & MASK_MASTER3) -> AF (!MASK_MASTER1 | !MASK_MASTER3)) is true evaluating specification EF (MASK_MASTER2 & MASK_MASTER3) eu: computing fixed point approximations for EF (MASK_MASTER2 & MASK_MASTER3) ... size of Y1 = 1.83828e+08 states, 30231 BDD nodes size of Y2 = 2.00212e+08 states, 36733 BDD nodes size of Y3 = 2.14958e+08 states, 43276 BDD nodes size of Y4 = 2.37126e+08 states, 56626 BDD nodes size of Y5 = 2.53297e+08 states, 61832 BDD nodes size of Y6 = 2.63127e+08 states, 68246 BDD nodes size of Y7 = 2.77266e+08 states, 76258 BDD nodes size of Y8 = 2.98492e+08 states, 76511 BDD nodes size of Y9 = 3.13352e+08 states, 81821 BDD nodes size of Y10 = 3.28372e+08 states, 85740 BDD nodes size of Y11 = 3.40271e+08 states, 87158 BDD nodes size of Y12 = 3.50765e+08 states, 88343 BDD nodes size of Y13 = 3.5983e+08 states, 84821 BDD nodes size of Y14 = 3.65515e+08 states, 83083 BDD nodes size of Y15 = 3.68792e+08 states, 82682 BDD nodes size of Y16 = 3.71778e+08 states, 79469 BDD nodes size of Y17 = 3.73047e+08 states, 77779 BDD nodes size of Y18 = 3.73383e+08 states, 76529 BDD nodes size of Y19 = 3.73424e+08 states, 76401 BDD nodes -- specification EF (MASK_MASTER2 & MASK_MASTER3) is true evaluating specification AG ((MASK_MASTER2 & MASK_MASTER3) -> AF (!MASK_MASTER2 | !MASK_MASTER3)) size of res0 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 23451 BDD nodes size of Y2 = 3.68935e+19 x, 24930 BDD nodes size of Y3 = 3.68935e+19 x, 24145 BDD nodes size of Y4 = 3.68935e+19 x, 24018 BDD nodes size of Y5 = 3.68935e+19 x, 23829 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 24159 BDD nodes size of Y2 = 3.68935e+19 x, 25636 BDD nodes size of Y3 = 3.68935e+19 x, 24849 BDD nodes size of Y4 = 3.68935e+19 x, 24721 BDD nodes size of Y5 = 3.68935e+19 x, 24532 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 14466 BDD nodes size of Y2 = 3.68935e+19 x, 17162 BDD nodes size of Y3 = 3.68935e+19 x, 22704 BDD nodes size of Y4 = 3.68935e+19 x, 26199 BDD nodes size of Y5 = 3.68935e+19 x, 27039 BDD nodes size of Y6 = 3.68935e+19 x, 28036 BDD nodes size of Y7 = 3.68935e+19 x, 27769 BDD nodes size of Y8 = 3.68935e+19 x, 27296 BDD nodes size of Y9 = 3.68935e+19 x, 24857 BDD nodes size of Y10 = 3.68935e+19 x, 24233 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 13874 BDD nodes size of Y2 = 3.68935e+19 x, 20834 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 6829 BDD nodes size of res1 = 7.66607e+07 x, 19637 BDD nodes size of Y0 = 4.17219e+07 x, 8069 BDD nodes size of Y1 = 4.73416e+07 x, 10786 BDD nodes size of Y2 = 5.21585e+07 x, 13478 BDD nodes size of Y3 = 6.04815e+07 x, 18917 BDD nodes size of Y4 = 6.47905e+07 x, 22002 BDD nodes size of Y5 = 6.61955e+07 x, 22609 BDD nodes size of Y6 = 6.93166e+07 x, 23750 BDD nodes size of Y7 = 7.29211e+07 x, 23273 BDD nodes size of Y8 = 7.47438e+07 x, 22764 BDD nodes size of Y9 = 7.63658e+07 x, 20261 BDD nodes size of Y10 = 7.66607e+07 x, 19637 BDD nodes size of Y0 = 3.96657e+07 x, 5378 BDD nodes size of Y1 = 5.97811e+07 x, 15947 BDD nodes size of Y2 = 7.66607e+07 x, 19637 BDD nodes size of Y0 = 5.68279e+07 x, 19623 BDD nodes size of Y1 = 7.66607e+07 x, 19637 BDD nodes size of res2 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG ((MASK_MASTER2 & MASK_MASTER3) -> AF (!MASK_MASTER2 | !MASK_MASTER3)) ... -- specification AG ((MASK_MASTER2 & MASK_MASTER3) -> AF (!MASK_MASTER2 | !MASK_MASTER3)) is true evaluating specification EF ((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) eu: computing fixed point approximations for EF ((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) ... size of Y1 = 1.29393e+08 states, 15237 BDD nodes size of Y2 = 1.46252e+08 states, 23792 BDD nodes size of Y3 = 1.60702e+08 states, 31684 BDD nodes size of Y4 = 1.85672e+08 states, 45648 BDD nodes size of Y5 = 1.98599e+08 states, 49482 BDD nodes size of Y6 = 2.05517e+08 states, 54663 BDD nodes size of Y7 = 2.18124e+08 states, 59236 BDD nodes size of Y8 = 2.37785e+08 states, 56201 BDD nodes size of Y9 = 2.5505e+08 states, 60038 BDD nodes size of Y10 = 2.69943e+08 states, 62660 BDD nodes size of Y11 = 2.87343e+08 states, 69512 BDD nodes size of Y12 = 3.01314e+08 states, 75949 BDD nodes size of Y13 = 3.14917e+08 states, 82902 BDD nodes size of Y14 = 3.33926e+08 states, 78972 BDD nodes size of Y15 = 3.41189e+08 states, 81817 BDD nodes size of Y16 = 3.52297e+08 states, 81333 BDD nodes size of Y17 = 3.60796e+08 states, 82836 BDD nodes size of Y18 = 3.67071e+08 states, 83169 BDD nodes size of Y19 = 3.72003e+08 states, 78924 BDD nodes size of Y20 = 3.72998e+08 states, 77203 BDD nodes size of Y21 = 3.73424e+08 states, 76401 BDD nodes -- specification EF ((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) is true evaluating specification AG (((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) -> AF ((!MASK_MASTER1 | !MASK_MASTER2) | !MASK_MASTER3)) size of res0 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 11194 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 11564 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 11688 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 3373 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 3369 BDD nodes size of res1 = 0 x, 1 BDD nodes eu: computing fixed point approximations for AG (((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) -> AF ((!MASK_MASTER1 | !MASK_MASTER2) | !MASK_MASTER3)) ... -- specification AG (((MASK_MASTER1 & MASK_MASTER2) & MASK_MASTER3) -> AF ((!MASK_MASTER1 | !MASK_MASTER2) | !MASK_MASTER3)) is true evaluating specification AG (master1.state = busreq -> AF HGRANT1) size of res0 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 25513 BDD nodes size of Y2 = 3.68935e+19 x, 34882 BDD nodes size of Y3 = 3.68935e+19 x, 41271 BDD nodes size of Y4 = 3.68935e+19 x, 44609 BDD nodes size of Y5 = 3.68935e+19 x, 47424 BDD nodes size of Y6 = 3.68935e+19 x, 52508 BDD nodes size of Y7 = 3.68935e+19 x, 52101 BDD nodes size of Y8 = 3.68935e+19 x, 53684 BDD nodes size of Y9 = 3.68935e+19 x, 53577 BDD nodes size of Y10 = 3.68935e+19 x, 52451 BDD nodes size of Y11 = 3.68935e+19 x, 52074 BDD nodes size of Y12 = 3.68935e+19 x, 51291 BDD nodes size of Y13 = 3.68935e+19 x, 51238 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 26408 BDD nodes size of Y2 = 3.68935e+19 x, 35771 BDD nodes size of Y3 = 3.68935e+19 x, 42024 BDD nodes size of Y4 = 3.68935e+19 x, 45926 BDD nodes size of Y5 = 3.68935e+19 x, 49012 BDD nodes size of Y6 = 3.68935e+19 x, 53559 BDD nodes size of Y7 = 3.68935e+19 x, 52949 BDD nodes size of Y8 = 3.68935e+19 x, 54239 BDD nodes size of Y9 = 3.68935e+19 x, 53376 BDD nodes size of Y10 = 3.68935e+19 x, 52350 BDD nodes size of Y11 = 3.68935e+19 x, 52007 BDD nodes size of Y12 = 3.68935e+19 x, 51544 BDD nodes size of Y13 = 3.68935e+19 x, 51548 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 39285 BDD nodes size of Y2 = 3.68935e+19 x, 44848 BDD nodes size of Y3 = 3.68935e+19 x, 42228 BDD nodes size of Y4 = 3.68935e+19 x, 42093 BDD nodes size of Y5 = 3.68935e+19 x, 41762 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 34463 BDD nodes size of Y2 = 3.68935e+19 x, 45542 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 14991 BDD nodes size of res1 = 1.97837e+08 x, 42478 BDD nodes size of Y0 = 5.12082e+07 x, 12213 BDD nodes size of Y1 = 8.22231e+07 x, 21913 BDD nodes size of Y2 = 9.67229e+07 x, 27876 BDD nodes size of Y3 = 1.21946e+08 x, 37524 BDD nodes size of Y4 = 1.39485e+08 x, 40084 BDD nodes size of Y5 = 1.48668e+08 x, 43232 BDD nodes size of Y6 = 1.58024e+08 x, 46159 BDD nodes size of Y7 = 1.71987e+08 x, 46245 BDD nodes size of Y8 = 1.80724e+08 x, 46853 BDD nodes size of Y9 = 1.87474e+08 x, 45631 BDD nodes size of Y10 = 1.90685e+08 x, 45421 BDD nodes size of Y11 = 1.91594e+08 x, 45261 BDD nodes size of Y12 = 1.92467e+08 x, 44677 BDD nodes size of Y13 = 1.92971e+08 x, 44137 BDD nodes size of Y14 = 1.93028e+08 x, 44071 BDD nodes size of Y0 = 5.11918e+07 x, 11890 BDD nodes size of Y1 = 8.22067e+07 x, 21297 BDD nodes size of Y2 = 9.67066e+07 x, 27225 BDD nodes size of Y3 = 1.2193e+08 x, 37156 BDD nodes size of Y4 = 1.39469e+08 x, 40201 BDD nodes size of Y5 = 1.48652e+08 x, 43457 BDD nodes size of Y6 = 1.58007e+08 x, 46324 BDD nodes size of Y7 = 1.71971e+08 x, 46368 BDD nodes size of Y8 = 1.80707e+08 x, 46696 BDD nodes size of Y9 = 1.87458e+08 x, 45388 BDD nodes size of Y10 = 1.90669e+08 x, 45114 BDD nodes size of Y11 = 1.91578e+08 x, 44949 BDD nodes size of Y12 = 1.92451e+08 x, 44412 BDD nodes size of Y13 = 1.92954e+08 x, 44155 BDD nodes size of Y14 = 1.93012e+08 x, 44111 BDD nodes size of Y0 = 1.01581e+08 x, 12685 BDD nodes size of Y1 = 1.51724e+08 x, 38879 BDD nodes size of Y2 = 1.97591e+08 x, 42906 BDD nodes size of Y0 = 1.46342e+08 x, 41768 BDD nodes size of Y1 = 1.96952e+08 x, 42201 BDD nodes size of Y2 = 1.97411e+08 x, 42325 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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 26987 BDD nodes size of Y2 = 3.68935e+19 x, 36641 BDD nodes size of Y3 = 3.68935e+19 x, 43152 BDD nodes size of Y4 = 3.68935e+19 x, 46865 BDD nodes size of Y5 = 3.68935e+19 x, 49476 BDD nodes size of Y6 = 3.68935e+19 x, 53825 BDD nodes size of Y7 = 3.68935e+19 x, 53275 BDD nodes size of Y8 = 3.68935e+19 x, 54395 BDD nodes size of Y9 = 3.68935e+19 x, 54566 BDD nodes size of Y10 = 3.68935e+19 x, 53619 BDD nodes size of Y11 = 3.68935e+19 x, 52852 BDD nodes size of Y12 = 3.68935e+19 x, 51443 BDD nodes size of Y13 = 3.68935e+19 x, 51324 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 39773 BDD nodes size of Y2 = 3.68935e+19 x, 45359 BDD nodes size of Y3 = 3.68935e+19 x, 42500 BDD nodes size of Y4 = 3.68935e+19 x, 42227 BDD nodes size of Y5 = 3.68935e+19 x, 41855 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 26806 BDD nodes size of Y2 = 3.68935e+19 x, 36430 BDD nodes size of Y3 = 3.68935e+19 x, 43951 BDD nodes size of Y4 = 3.68935e+19 x, 50971 BDD nodes size of Y5 = 3.68935e+19 x, 55471 BDD nodes size of Y6 = 3.68935e+19 x, 60467 BDD nodes size of Y7 = 3.68935e+19 x, 58901 BDD nodes size of Y8 = 3.68935e+19 x, 59523 BDD nodes size of Y9 = 3.68935e+19 x, 57570 BDD nodes size of Y10 = 3.68935e+19 x, 55566 BDD nodes size of Y11 = 3.68935e+19 x, 54946 BDD nodes size of Y12 = 3.68935e+19 x, 54054 BDD nodes size of Y13 = 3.68935e+19 x, 53973 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35115 BDD nodes size of Y2 = 3.68935e+19 x, 47292 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 14810 BDD nodes size of res1 = 1.97837e+08 x, 42713 BDD nodes size of Y0 = 5.11918e+07 x, 12538 BDD nodes size of Y1 = 8.22067e+07 x, 22178 BDD nodes size of Y2 = 9.67066e+07 x, 28068 BDD nodes size of Y3 = 1.2193e+08 x, 38405 BDD nodes size of Y4 = 1.39469e+08 x, 43014 BDD nodes size of Y5 = 1.48652e+08 x, 46528 BDD nodes size of Y6 = 1.58007e+08 x, 49916 BDD nodes size of Y7 = 1.71971e+08 x, 50153 BDD nodes size of Y8 = 1.80707e+08 x, 50900 BDD nodes size of Y9 = 1.87458e+08 x, 49121 BDD nodes size of Y10 = 1.90669e+08 x, 48403 BDD nodes size of Y11 = 1.91578e+08 x, 47744 BDD nodes size of Y12 = 1.92451e+08 x, 46753 BDD nodes size of Y13 = 1.92954e+08 x, 45367 BDD nodes size of Y14 = 1.93012e+08 x, 45209 BDD nodes size of Y0 = 5.12082e+07 x, 11764 BDD nodes size of Y1 = 8.22231e+07 x, 20789 BDD nodes size of Y2 = 9.67229e+07 x, 26873 BDD nodes size of Y3 = 1.21946e+08 x, 37562 BDD nodes size of Y4 = 1.39485e+08 x, 43344 BDD nodes size of Y5 = 1.48668e+08 x, 47748 BDD nodes size of Y6 = 1.58024e+08 x, 51259 BDD nodes size of Y7 = 1.71987e+08 x, 51265 BDD nodes size of Y8 = 1.80724e+08 x, 50737 BDD nodes size of Y9 = 1.87474e+08 x, 48201 BDD nodes size of Y10 = 1.90685e+08 x, 47355 BDD nodes size of Y11 = 1.91594e+08 x, 46879 BDD nodes size of Y12 = 1.92467e+08 x, 46265 BDD nodes size of Y13 = 1.92971e+08 x, 45578 BDD nodes size of Y14 = 1.93028e+08 x, 45439 BDD nodes size of Y0 = 1.01581e+08 x, 12147 BDD nodes size of Y1 = 1.51724e+08 x, 37865 BDD nodes size of Y2 = 1.97591e+08 x, 43119 BDD nodes size of Y0 = 1.46342e+08 x, 42074 BDD nodes size of Y1 = 1.96952e+08 x, 42466 BDD nodes size of Y2 = 1.97411e+08 x, 42570 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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 38061 BDD nodes size of Y2 = 3.68935e+19 x, 43297 BDD nodes size of Y3 = 3.68935e+19 x, 40415 BDD nodes size of Y4 = 3.68935e+19 x, 40119 BDD nodes size of Y5 = 3.68935e+19 x, 39752 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 27347 BDD nodes size of Y2 = 3.68935e+19 x, 37099 BDD nodes size of Y3 = 3.68935e+19 x, 43495 BDD nodes size of Y4 = 3.68935e+19 x, 47963 BDD nodes size of Y5 = 3.68935e+19 x, 50951 BDD nodes size of Y6 = 3.68935e+19 x, 55962 BDD nodes size of Y7 = 3.68935e+19 x, 55003 BDD nodes size of Y8 = 3.68935e+19 x, 56110 BDD nodes size of Y9 = 3.68935e+19 x, 56271 BDD nodes size of Y10 = 3.68935e+19 x, 55097 BDD nodes size of Y11 = 3.68935e+19 x, 54049 BDD nodes size of Y12 = 3.68935e+19 x, 52263 BDD nodes size of Y13 = 3.68935e+19 x, 51999 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 26322 BDD nodes size of Y2 = 3.68935e+19 x, 36018 BDD nodes size of Y3 = 3.68935e+19 x, 43697 BDD nodes size of Y4 = 3.68935e+19 x, 50901 BDD nodes size of Y5 = 3.68935e+19 x, 55242 BDD nodes size of Y6 = 3.68935e+19 x, 59443 BDD nodes size of Y7 = 3.68935e+19 x, 57753 BDD nodes size of Y8 = 3.68935e+19 x, 58066 BDD nodes size of Y9 = 3.68935e+19 x, 56167 BDD nodes size of Y10 = 3.68935e+19 x, 54581 BDD nodes size of Y11 = 3.68935e+19 x, 53691 BDD nodes size of Y12 = 3.68935e+19 x, 52799 BDD nodes size of Y13 = 3.68935e+19 x, 52639 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 34571 BDD nodes size of Y2 = 3.68935e+19 x, 46811 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 14498 BDD nodes size of res1 = 1.97837e+08 x, 40543 BDD nodes size of Y0 = 5.12082e+07 x, 12016 BDD nodes size of Y1 = 8.22231e+07 x, 20768 BDD nodes size of Y2 = 9.67229e+07 x, 26395 BDD nodes size of Y3 = 1.21946e+08 x, 36322 BDD nodes size of Y4 = 1.39485e+08 x, 41784 BDD nodes size of Y5 = 1.48668e+08 x, 45536 BDD nodes size of Y6 = 1.58024e+08 x, 49163 BDD nodes size of Y7 = 1.71987e+08 x, 49507 BDD nodes size of Y8 = 1.80724e+08 x, 49894 BDD nodes size of Y9 = 1.87474e+08 x, 47982 BDD nodes size of Y10 = 1.90685e+08 x, 46939 BDD nodes size of Y11 = 1.91594e+08 x, 46234 BDD nodes size of Y12 = 1.92467e+08 x, 45154 BDD nodes size of Y13 = 1.92971e+08 x, 43566 BDD nodes size of Y14 = 1.93028e+08 x, 43257 BDD nodes size of Y0 = 5.11918e+07 x, 11755 BDD nodes size of Y1 = 8.22067e+07 x, 20297 BDD nodes size of Y2 = 9.67066e+07 x, 26118 BDD nodes size of Y3 = 1.2193e+08 x, 36147 BDD nodes size of Y4 = 1.39469e+08 x, 42370 BDD nodes size of Y5 = 1.48652e+08 x, 46660 BDD nodes size of Y6 = 1.58007e+08 x, 50147 BDD nodes size of Y7 = 1.71971e+08 x, 50298 BDD nodes size of Y8 = 1.80707e+08 x, 49493 BDD nodes size of Y9 = 1.87458e+08 x, 47103 BDD nodes size of Y10 = 1.90669e+08 x, 46159 BDD nodes size of Y11 = 1.91578e+08 x, 45374 BDD nodes size of Y12 = 1.92451e+08 x, 44535 BDD nodes size of Y13 = 1.92954e+08 x, 43707 BDD nodes size of Y14 = 1.93012e+08 x, 43456 BDD nodes size of Y0 = 1.01581e+08 x, 11396 BDD nodes size of Y1 = 1.51724e+08 x, 35530 BDD nodes size of Y2 = 1.97591e+08 x, 40935 BDD nodes size of Y0 = 1.46342e+08 x, 39951 BDD nodes size of Y1 = 1.96952e+08 x, 40303 BDD nodes size of Y2 = 1.97411e+08 x, 40379 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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 34351 BDD nodes size of Y2 = 3.68935e+19 x, 44336 BDD nodes size of Y3 = 3.68935e+19 x, 49830 BDD nodes size of Y4 = 3.68935e+19 x, 53004 BDD nodes size of Y5 = 3.68935e+19 x, 56249 BDD nodes size of Y6 = 3.68935e+19 x, 62735 BDD nodes size of Y7 = 3.68935e+19 x, 62745 BDD nodes size of Y8 = 3.68935e+19 x, 64658 BDD nodes size of Y9 = 3.68935e+19 x, 64818 BDD nodes size of Y10 = 3.68935e+19 x, 63711 BDD nodes size of Y11 = 3.68935e+19 x, 63938 BDD nodes size of Y12 = 3.68935e+19 x, 63257 BDD nodes size of Y13 = 3.68935e+19 x, 63204 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35429 BDD nodes size of Y2 = 3.68935e+19 x, 45484 BDD nodes size of Y3 = 3.68935e+19 x, 50982 BDD nodes size of Y4 = 3.68935e+19 x, 54829 BDD nodes size of Y5 = 3.68935e+19 x, 58454 BDD nodes size of Y6 = 3.68935e+19 x, 64912 BDD nodes size of Y7 = 3.68935e+19 x, 64716 BDD nodes size of Y8 = 3.68935e+19 x, 66625 BDD nodes size of Y9 = 3.68935e+19 x, 66766 BDD nodes size of Y10 = 3.68935e+19 x, 65818 BDD nodes size of Y11 = 3.68935e+19 x, 65856 BDD nodes size of Y12 = 3.68935e+19 x, 64655 BDD nodes size of Y13 = 3.68935e+19 x, 64535 BDD nodes size of Y14 = 3.68935e+19 x, 64533 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 34470 BDD nodes size of Y2 = 3.68935e+19 x, 42986 BDD nodes size of Y3 = 3.68935e+19 x, 49446 BDD nodes size of Y4 = 3.68935e+19 x, 52190 BDD nodes size of Y5 = 3.68935e+19 x, 51984 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 40606 BDD nodes size of Y2 = 3.68935e+19 x, 52962 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 15945 BDD nodes size of res1 = 2.09549e+08 x, 55360 BDD nodes size of Y0 = 4.66708e+07 x, 13129 BDD nodes size of Y1 = 8.18647e+07 x, 25981 BDD nodes size of Y2 = 1.02294e+08 x, 33874 BDD nodes size of Y3 = 1.28091e+08 x, 43736 BDD nodes size of Y4 = 1.46328e+08 x, 46697 BDD nodes size of Y5 = 1.5479e+08 x, 50151 BDD nodes size of Y6 = 1.63576e+08 x, 53719 BDD nodes size of Y7 = 1.77162e+08 x, 55041 BDD nodes size of Y8 = 1.86968e+08 x, 55834 BDD nodes size of Y9 = 1.95167e+08 x, 57252 BDD nodes size of Y10 = 1.99236e+08 x, 56714 BDD nodes size of Y11 = 2.00292e+08 x, 56219 BDD nodes size of Y12 = 2.01087e+08 x, 55752 BDD nodes size of Y13 = 2.01521e+08 x, 55270 BDD nodes size of Y14 = 2.0157e+08 x, 55207 BDD nodes size of Y0 = 4.66954e+07 x, 12902 BDD nodes size of Y1 = 8.18893e+07 x, 25148 BDD nodes size of Y2 = 1.02318e+08 x, 32882 BDD nodes size of Y3 = 1.28116e+08 x, 43038 BDD nodes size of Y4 = 1.46352e+08 x, 46479 BDD nodes size of Y5 = 1.54814e+08 x, 50171 BDD nodes size of Y6 = 1.6365e+08 x, 53770 BDD nodes size of Y7 = 1.77187e+08 x, 54893 BDD nodes size of Y8 = 1.86878e+08 x, 55462 BDD nodes size of Y9 = 1.94903e+08 x, 57252 BDD nodes size of Y10 = 1.98945e+08 x, 56473 BDD nodes size of Y11 = 1.99966e+08 x, 55964 BDD nodes size of Y12 = 2.00809e+08 x, 55425 BDD nodes size of Y13 = 2.01358e+08 x, 55271 BDD nodes size of Y14 = 2.01511e+08 x, 55387 BDD nodes size of Y15 = 2.0157e+08 x, 55236 BDD nodes size of Y0 = 8.11827e+06 x, 6552 BDD nodes size of Y1 = 8.79002e+06 x, 9535 BDD nodes size of Y2 = 9.58464e+06 x, 12380 BDD nodes size of Y3 = 9.97786e+06 x, 12615 BDD nodes size of Y0 = 1.06037e+08 x, 14549 BDD nodes size of Y1 = 1.57497e+08 x, 47225 BDD nodes size of Y2 = 2.09222e+08 x, 56055 BDD nodes size of Y0 = 1.59382e+08 x, 54342 BDD nodes size of Y1 = 2.08697e+08 x, 55089 BDD nodes size of Y2 = 2.09091e+08 x, 55193 BDD nodes size of res2 = 1.77766e+06 x, 7846 BDD nodes size of Y0 = 245760 x, 916 BDD nodes size of Y1 = 253952 x, 960 BDD nodes size of Y2 = 266240 x, 1309 BDD nodes size of Y3 = 278528 x, 1342 BDD nodes size of Y0 = 253952 x, 1051 BDD nodes size of Y1 = 262144 x, 1095 BDD nodes size of Y2 = 274432 x, 1495 BDD nodes size of Y3 = 286720 x, 1520 BDD nodes size of Y0 = 737280 x, 946 BDD nodes size of Y1 = 1.00762e+06 x, 6138 BDD nodes size of Y2 = 1.77766e+06 x, 7846 BDD nodes size of Y0 = 1.23699e+06 x, 7263 BDD nodes size of Y1 = 1.4336e+06 x, 7265 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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 34800 BDD nodes size of Y2 = 3.68935e+19 x, 44717 BDD nodes size of Y3 = 3.68935e+19 x, 50553 BDD nodes size of Y4 = 3.68935e+19 x, 53881 BDD nodes size of Y5 = 3.68935e+19 x, 57046 BDD nodes size of Y6 = 3.68935e+19 x, 63168 BDD nodes size of Y7 = 3.68935e+19 x, 62984 BDD nodes size of Y8 = 3.68935e+19 x, 65017 BDD nodes size of Y9 = 3.68935e+19 x, 65216 BDD nodes size of Y10 = 3.68935e+19 x, 64142 BDD nodes size of Y11 = 3.68935e+19 x, 64083 BDD nodes size of Y12 = 3.68935e+19 x, 62779 BDD nodes size of Y13 = 3.68935e+19 x, 62618 BDD nodes size of Y14 = 3.68935e+19 x, 62528 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35593 BDD nodes size of Y2 = 3.68935e+19 x, 43997 BDD nodes size of Y3 = 3.68935e+19 x, 50040 BDD nodes size of Y4 = 3.68935e+19 x, 51972 BDD nodes size of Y5 = 3.68935e+19 x, 51719 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35542 BDD nodes size of Y2 = 3.68935e+19 x, 45626 BDD nodes size of Y3 = 3.68935e+19 x, 52423 BDD nodes size of Y4 = 3.68935e+19 x, 58365 BDD nodes size of Y5 = 3.68935e+19 x, 63211 BDD nodes size of Y6 = 3.68935e+19 x, 69468 BDD nodes size of Y7 = 3.68935e+19 x, 67815 BDD nodes size of Y8 = 3.68935e+19 x, 69312 BDD nodes size of Y9 = 3.68935e+19 x, 68162 BDD nodes size of Y10 = 3.68935e+19 x, 66246 BDD nodes size of Y11 = 3.68935e+19 x, 65780 BDD nodes size of Y12 = 3.68935e+19 x, 65064 BDD nodes size of Y13 = 3.68935e+19 x, 65011 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 41428 BDD nodes size of Y2 = 3.68935e+19 x, 53273 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 16398 BDD nodes size of res1 = 2.09549e+08 x, 55558 BDD nodes size of Y0 = 4.66954e+07 x, 13517 BDD nodes size of Y1 = 8.18893e+07 x, 26744 BDD nodes size of Y2 = 1.02318e+08 x, 34696 BDD nodes size of Y3 = 1.28116e+08 x, 45035 BDD nodes size of Y4 = 1.46352e+08 x, 48807 BDD nodes size of Y5 = 1.54814e+08 x, 52798 BDD nodes size of Y6 = 1.6365e+08 x, 56592 BDD nodes size of Y7 = 1.77187e+08 x, 57818 BDD nodes size of Y8 = 1.86878e+08 x, 58750 BDD nodes size of Y9 = 1.94903e+08 x, 60224 BDD nodes size of Y10 = 1.98945e+08 x, 59103 BDD nodes size of Y11 = 1.99966e+08 x, 58269 BDD nodes size of Y12 = 2.00809e+08 x, 57441 BDD nodes size of Y13 = 2.01358e+08 x, 56366 BDD nodes size of Y14 = 2.01511e+08 x, 56418 BDD nodes size of Y15 = 2.0157e+08 x, 56229 BDD nodes size of Y0 = 8.11827e+06 x, 6497 BDD nodes size of Y1 = 8.79002e+06 x, 8975 BDD nodes size of Y2 = 9.58464e+06 x, 11595 BDD nodes size of Y3 = 9.97786e+06 x, 11895 BDD nodes size of Y0 = 4.66708e+07 x, 12830 BDD nodes size of Y1 = 8.18647e+07 x, 25252 BDD nodes size of Y2 = 1.02294e+08 x, 33378 BDD nodes size of Y3 = 1.28091e+08 x, 44009 BDD nodes size of Y4 = 1.46328e+08 x, 48641 BDD nodes size of Y5 = 1.5479e+08 x, 53505 BDD nodes size of Y6 = 1.63576e+08 x, 57433 BDD nodes size of Y7 = 1.77162e+08 x, 58506 BDD nodes size of Y8 = 1.86968e+08 x, 58423 BDD nodes size of Y9 = 1.95167e+08 x, 59429 BDD nodes size of Y10 = 1.99236e+08 x, 58307 BDD nodes size of Y11 = 2.00292e+08 x, 57486 BDD nodes size of Y12 = 2.01087e+08 x, 56965 BDD nodes size of Y13 = 2.01521e+08 x, 56554 BDD nodes size of Y14 = 2.0157e+08 x, 56476 BDD nodes size of Y0 = 1.06037e+08 x, 14428 BDD nodes size of Y1 = 1.57497e+08 x, 47168 BDD nodes size of Y2 = 2.09222e+08 x, 56213 BDD nodes size of Y0 = 1.59382e+08 x, 54614 BDD nodes size of Y1 = 2.08697e+08 x, 55310 BDD nodes size of Y2 = 2.09091e+08 x, 55402 BDD nodes size of res2 = 1.77766e+06 x, 7035 BDD nodes size of Y0 = 253952 x, 890 BDD nodes size of Y1 = 262144 x, 934 BDD nodes size of Y2 = 274432 x, 1229 BDD nodes size of Y3 = 286720 x, 1269 BDD nodes size of Y0 = 245760 x, 1019 BDD nodes size of Y1 = 253952 x, 1063 BDD nodes size of Y2 = 266240 x, 1466 BDD nodes size of Y3 = 278528 x, 1490 BDD nodes size of Y0 = 737280 x, 906 BDD nodes size of Y1 = 1.00762e+06 x, 5256 BDD nodes size of Y2 = 1.77766e+06 x, 7035 BDD nodes size of Y0 = 1.23699e+06 x, 6492 BDD nodes size of Y1 = 1.4336e+06 x, 6494 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 = 1.47574e+20 x, 1 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35212 BDD nodes size of Y2 = 3.68935e+19 x, 43602 BDD nodes size of Y3 = 3.68935e+19 x, 49841 BDD nodes size of Y4 = 3.68935e+19 x, 51559 BDD nodes size of Y5 = 3.68935e+19 x, 51292 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 36446 BDD nodes size of Y2 = 3.68935e+19 x, 46601 BDD nodes size of Y3 = 3.68935e+19 x, 52538 BDD nodes size of Y4 = 3.68935e+19 x, 56398 BDD nodes size of Y5 = 3.68935e+19 x, 59894 BDD nodes size of Y6 = 3.68935e+19 x, 66343 BDD nodes size of Y7 = 3.68935e+19 x, 65584 BDD nodes size of Y8 = 3.68935e+19 x, 67709 BDD nodes size of Y9 = 3.68935e+19 x, 67760 BDD nodes size of Y10 = 3.68935e+19 x, 66196 BDD nodes size of Y11 = 3.68935e+19 x, 65139 BDD nodes size of Y12 = 3.68935e+19 x, 63647 BDD nodes size of Y13 = 3.68935e+19 x, 63451 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 35994 BDD nodes size of Y2 = 3.68935e+19 x, 46224 BDD nodes size of Y3 = 3.68935e+19 x, 53266 BDD nodes size of Y4 = 3.68935e+19 x, 59390 BDD nodes size of Y5 = 3.68935e+19 x, 64258 BDD nodes size of Y6 = 3.68935e+19 x, 70206 BDD nodes size of Y7 = 3.68935e+19 x, 68708 BDD nodes size of Y8 = 3.68935e+19 x, 69994 BDD nodes size of Y9 = 3.68935e+19 x, 68930 BDD nodes size of Y10 = 3.68935e+19 x, 67214 BDD nodes size of Y11 = 3.68935e+19 x, 66667 BDD nodes size of Y12 = 3.68935e+19 x, 65403 BDD nodes size of Y13 = 3.68935e+19 x, 65163 BDD nodes size of Y14 = 3.68935e+19 x, 65017 BDD nodes size of Y0 = 3.68935e+19 x, 3 BDD nodes size of Y1 = 3.68935e+19 x, 42210 BDD nodes size of Y2 = 3.68935e+19 x, 54086 BDD nodes size of Y0 = 7.3787e+19 x, 2 BDD nodes size of Y1 = 7.3787e+19 x, 16772 BDD nodes size of res1 = 2.09549e+08 x, 55564 BDD nodes size of Y0 = 8.11827e+06 x, 6753 BDD nodes size of Y1 = 8.79002e+06 x, 9229 BDD nodes size of Y2 = 9.58464e+06 x, 11839 BDD nodes size of Y3 = 9.97786e+06 x, 12187 BDD nodes size of Y0 = 4.66708e+07 x, 13225 BDD nodes size of Y1 = 8.18647e+07 x, 26109 BDD nodes size of Y2 = 1.02294e+08 x, 34158 BDD nodes size of Y3 = 1.28091e+08 x, 44668 BDD nodes size of Y4 = 1.46328e+08 x, 49215 BDD nodes size of Y5 = 1.5479e+08 x, 53616 BDD nodes size of Y6 = 1.63576e+08 x, 57591 BDD nodes size of Y7 = 1.77162e+08 x, 58886 BDD nodes size of Y8 = 1.86968e+08 x, 59549 BDD nodes size of Y9 = 1.95167e+08 x, 60822 BDD nodes size of Y10 = 1.99236e+08 x, 59570 BDD nodes size of Y11 = 2.00292e+08 x, 58561 BDD nodes size of Y12 = 2.01087e+08 x, 57712 BDD nodes size of Y13 = 2.01521e+08 x, 56548 BDD nodes size of Y14 = 2.0157e+08 x, 56326 BDD nodes size of Y0 = 4.66954e+07 x, 13105 BDD nodes size of Y1 = 8.18893e+07 x, 25679 BDD nodes size of Y2 = 1.02318e+08 x, 33847 BDD nodes size of Y3 = 1.28116e+08 x, 44451 BDD nodes size of Y4 = 1.46352e+08 x, 49593 BDD nodes size of Y5 = 1.54814e+08 x, 54502 BDD nodes size of Y6 = 1.6365e+08 x, 58460 BDD nodes size of Y7 = 1.77187e+08 x, 59298 BDD nodes size of Y8 = 1.86878e+08 x, 59073 BDD nodes size of Y9 = 1.94903e+08 x, 60369 BDD nodes size of Y10 = 1.98945e+08 x, 59048 BDD nodes size of Y11 = 1.99966e+08 x, 57942 BDD nodes size of Y12 = 2.00809e+08 x, 57150 BDD nodes size of Y13 = 2.01358e+08 x, 56685 BDD nodes size of Y14 = 2.01511e+08 x, 56769 BDD nodes size of Y15 = 2.0157e+08 x, 56542 BDD nodes size of Y0 = 1.06037e+08 x, 14329 BDD nodes size of Y1 = 1.57497e+08 x, 46889 BDD nodes size of Y2 = 2.09222e+08 x, 56169 BDD nodes size of Y0 = 1.59382e+08 x, 54631 BDD nodes size of Y1 = 2.08697e+08 x, 55315 BDD nodes size of Y2 = 2.09091e+08 x, 55387 BDD nodes size of res2 = 1.77766e+06 x, 6960 BDD nodes size of Y0 = 245760 x, 848 BDD nodes size of Y1 = 253952 x, 892 BDD nodes size of Y2 = 266240 x, 1184 BDD nodes size of Y3 = 278528 x, 1225 BDD nodes size of Y0 = 253952 x, 1034 BDD nodes size of Y1 = 262144 x, 1078 BDD nodes size of Y2 = 274432 x, 1427 BDD nodes size of Y3 = 286720 x, 1460 BDD nodes size of Y0 = 737280 x, 888 BDD nodes size of Y1 = 1.00762e+06 x, 5258 BDD nodes size of Y2 = 1.77766e+06 x, 6960 BDD nodes size of Y0 = 1.23699e+06 x, 6425 BDD nodes size of Y1 = 1.4336e+06 x, 6427 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 2073.060 seconds System time 1.500 seconds Average resident text size = 0K Average resident data+stack size = 0K Maximum resident size = 0K Virtual text size = 132044K Virtual data size = 32653K data size initialized = 234K data size uninitialized = 362K data size sbrk = 32057K Virtual memory limit = 4194304K (4194304K) Major page faults = 400 Minor page faults = 77462 Swaps = 0 Input blocks = 0 Output blocks = 0 Context switch (voluntary) = 0 Context switch (involuntary) = 0 ###################################################################### BDD statistics -------------------- BDD nodes allocated: 1431711 -------------------- BDD nodes representing init set of states: 32 BDD nodes representing state constraints: 21219 BDD nodes representing input constraints: 1 Forward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 3250 cluster 2 : 1052 cluster 3 : 3587 Backward Partitioning Schedule BDD cluster size (#nodes): cluster 1 : 3250 cluster 2 : 1052 cluster 3 : 3587