forked from apalache-mc/apalache
-
Notifications
You must be signed in to change notification settings - Fork 0
/
trex-arch.drawio
1 lines (1 loc) · 13.1 KB
/
trex-arch.drawio
1
<mxfile host="Electron" modified="2021-01-15T13:43:32.874Z" agent="5.0 (Macintosh; Intel Mac OS X 11_1_0) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/14.1.8 Chrome/87.0.4280.88 Electron/11.1.1 Safari/537.36" etag="vZ7e2WJS7BfoBkvPvljc" version="14.1.8" type="device" pages="4"><diagram id="C5RBs43oDa-KdzZeNtuy" name="Classes">7V1pd5s6E/41OSf9kBx244+xs7T3TZebpMt7v8lGtrnFQAE3cX/9lUBikcRiGwxp7fa0RggB0jPzzIxG8pk6Xb/cBcBfvfcs6JwpkvVypl6fKYosSwb6D5dskxJTV5KCZWBbpFJW8Gj/gqRQIqUb24JhoWLkeU5k+8XCuee6cB4VykAQeM/FagvPKd7VB0vIFTzOgcOXfrWtaEXeQhll5W+hvVzRO8vGODmzBrQyeZNwBSzvOVek3pyp08DzouTb+mUKHdx5tF++vtt+de6/G3d//R3+AJ8n/3v68OUiaex2l0vSVwigG+3d9K/vi9u3X7R/v/mfbv9+lu6uZn9dkEukn8DZkP56hD9iEExXcP4dBuTVoy3tz/DZXjvARUeThedGj+QM6o0JcOyli77P0WOiK9XJTxhENhqKK3Ii8nxUOl/ZjnUPtt4Gv0wYgfl3ejRZeYH9CzULHHRKRgXodBARVClGocYjvhIVS6g0gCGq84n2kJwW3YMwInXmnuMAP7Rn8QPjKmsQLG134kWRt6YNeRvXghY5Soc8PogC73sKInz9wnacqed4Qdw1qqVD09LSmrkzpjJTDfz0DUeSjDjuP/iSwzEZ2TvorWEUbFEVepaCdMscP2eYlw1Stsrh3SRlgIjZMm06vdsDEkvgLlGvpbdTVOZ2WsPbKUbxdsBBSHFBBCe438M8gNGX3JtmRTGsd4C4ykE82Ljnbzhgo56OciB24CIqhXDog7ntLu/jOtdaVvJAXhUXeejahRPDZ2VbFnRjeEUgAgkCMaZ8z3ajuC/0CfqLemwqXepnOnqgKTqWs2P0F1cPoqnnInwBOwYQRPB+hhjiVchdRWuHfG0DspWapB6y2yIUdoVMHqEFrOwKDI0DBocJx44VHek/WagEagCzRkOPm6MIecIAur6QORSpPIpUAWIcMIPOJy+0I9vD7QdJXQZJdWDpalCpcVCrdg4f06dPxuPDt4/B+wf185X/9k65/aoL+AxxwonPXh2fqSc+K4O4zEH8xGeHQbZSkwySz4RPrJz4rPVB7ZvPeOP1xGOvicd0o0gs5onGCLJ56/tEYx3QmNoYsUOhMf1EY60Pat80ZtSPKXStKxzuRUczx8MEMrFAuIolB48KOn9rO1Re0BEhH1kpIgH1XLD9hqtdGqZGC/4fF+j6mBZcv6Qt4aNt/ugTDGz03pgqk8IXO0pa1Edjckwb1Mhx1h4+2OYO2NZ2o5rQ2wRzWNG1ZMgQHS9hFWZIPWgVwuU8YkQQCaADIvtnMaJeQU2fMOgzWtJMhpbGDLslL0muyoewmYYMjWnIYBpKeoFrCAELbHPViFCWPrAuM/fRC6F19CVpsVVCHB1RRjJA5+FcDeW8XKlFuVIyQdtFrvaXhKpg1ZAlQZHF5uCugqCOqttpSQ4UqXibsVb9VGZV9W6kxuSkBvks2D2SEEavzhTDwbw6QwXGEn8rdZ9WwMdfN2vnNgBrbBk8r+wIPiLqx+XPAfCLQkThYcamHCVRTevQm2DUn8qbaiOhqSZpHfG6zPuntPuVuPulpwC4xChCIvcC55vI66739d3Vyv69r/LOlbD7da3CmTus+0W2coJ4+j+2MiMK/uz/3LjclA6KOKKQN66HFFFIit6Dl0LFXeMMwwkdyMq4iDdN5vCmmLpA3FmrqD28iez4SYwa6H/wEol/hykBVVTlRBgnqeDHnhGucuPOPeQT36SlJU5/eaeXDdOrDRPwKKqW+EP8eSFq1M44ooFhSxz66kie68WVfmfHfvfhNXgSEg5vV569zBtgRCW4SNeuvOj8DZF5KuyP5MQTpyUCOMdSdx6WXfGGu8R20bggRPyCcc8DNCTnuONi08MBNy/8JX4A8ThkBHju5jXXNFZXhRbi7xPPcyBwy5qzsvY+bNYzGJCXeESuiD7BLWOtwFwLwnCzLnkSwYPb8++5uuS5PgZgjmPATGUXaVBEmxE85xtCt0X4Ss7WdNYabKcr4C7hVXyNsLdA884KQXQeIR8QmQCPcJ7UvffcJX0XPxYyfUKvF/SZBYvcQfvhGrKcwl5oh74XwvIQ84ltWlBHZjN1JI+VrhTSuJ5uijF51E8rb+m5wLn3YrLAXPEvjKItsUYBMo/ZIGMaiCGsxIRe9giw7GZH1sYF6djVhkNoFKM2HnJoFJD1nyS92ERJ8KOtSIHCJ040cIJQw7YfNnBIsYt0C9a2g1/vLXR+QqwLqO+Ui8Ph45wykeIPr0w4bZRWZLTRIv4ILRIQ+klK9cJ+wXBPfKKcSolVTGLXSA0VmNKli60YxqVeQImiC6YwBU623JXPozRIE2xTn6yAs5jawdwRaJU0oGsIjeVM62gjOa93Lk1pKPMUnWsZCYejixBCRZJsSOmHsYWbBl0VJryZQrMm6tqaAmswMzo4JMoj409FoswjUcZI1Mfpx9gTicZ+SCyP/7eOVZHTn0Qk/QJijR8bvH6GhOISU17yX84IzUhJ+UXMRPicljuH7fYLQpv4HIlGpm3mwp7xne1cAVhjanP4oycSME2KitWLR+4s9HOto36y2TvOaAHnyyKOfkrcG3rxjL0Ylfls2QqH1kO6yIq+qFz+znv1dmKCpN1d1nY2qyJ+ZEY3ia0LxuzJOUKLWN8I7SehoZU3xhgTScd/REaVEX94qyz5dGjpaMaIsXRUUW7YWGDqaOOuTB1RLKcpjBLBlHL/JpDCob0L+vi4oownFfX0PO74iwTRydlKxLEF+GrhozVq9p07D+Aa4imGVECRy4z1SiqnGbKTe3GAb0tu932JXSU9/29em+42EG2KfjqL9KcIv85YkpoxpsqgVvg783NEcZNDhb+MoQcg+x8XC6yaTnLfn9z/YZTPSr0u9y/1Kp/A0b+dnkoWH597t/adnU3nwYCyx2wCNnvFaLo0oDvoiQJrfUNvCC5iFbDTAkJXr9uNjNmPmSd+qnru7h4jnXum/J88DHmojWtH4uc66RZsviqML2vQcFl+HlASaBejK19WHWIAKpXNCsfzlYryKzMPLQDNxVxoHs5NOFt0KC0Gk1RtygImPq4ReIjr17mslDhqJzn5w+RkJJoJPqqc0IaPsURnt16tnfOidFibDUKt8l7WiY2LI64rzEg2Xiem1zTU1joxszi/Z0pHWCdG08CPvZgyXtmSW/Q1zlaB7beYUlYKSQpnPU8LUxYctIgYzL44Opvr31RERmwwqqOllJwWV48hIsrrVdRqQxTSxOs+UKiywSQ2/6ApCnWppqGOU2o0PgaVBgCUWxITqIKO58epugw8CkDqECtaQ6zQbIxarJBhwbp5rBb1AznsAE06HYU0Lr6vTmPQxDVUgqasIVrRWyxC2A3i+CQuOtxVACtmaOWxFi+bo7UtG6w913paYRelsKJO1mgB0WpxUwgPdFlflit2k5XWZbjPyNK53rRgYy4mELmQLk2FsgFVOq2gWGGWZBujPVGsqTUNtcTMGmNKGJpR/VzV9YtMflSR4kN9ApFCALnHS7mKwkTxTVd1la4mYzOn+WRrXgSqFQDrCKdbYJO7nOV3mRZr6XG6OzdNBDwMyqSVC5lZC9jh2PEpR59DOFjGVZq60UpT6yzTS5qhFr3Ji3FnlMsZcPt62pwB15GnPWJCA1rR066vP65wO46qrPhYa6uATz329IDsVFTjq/cmKOOdBUXVdLkoKIIsipOgUEHRdxIUullF74JCPcGcoCDKDJONRJAVd8m79GQdp4DeS/ep2IHf8VoJMn9A13vR3Sq6XBKVmn95dFMTsbCAv6uwty4KOA5megi5M6giUoU7zgcN4NF/u/Sm/iaLdNY36Tu7ie64eIwQ5GGqqJbLqfwPOiTJeN/6vlsMslvocg11HJHU+YTMfuJDUqvxIVa7DB6iuXiRoRSTmy7kdiDLbgZo7ItZdjdArqGWbEtZGqhTpZfvg/YbpJKWp44GpabF43Y9izd4eYDPgZ0852tMl0lSM+NX+OxGtnPtuZDuD5S+4xvmuGmWTad5PkwCsMQWXV5eDt2c6y+j1EDuXVHpjkUbXRnqpWirq85suiHmlParZjwEpOA1Z+SdxLBCDLkNfQVCKJsCt6o7ETxkifJvKYJPWx/e2q71Sin+JH87pMAK5W/Xn485TP4GmSpeLh0PcO4Flu0u92SqwaBwgOtZ2V1oZEkUqhbRQ2cbFNOGjxx16ySk0TQdVW+a3HWEjG1Z2vunPfS6ljoOvBmDnOUo12z/qCeV1v40AvsDMwNQaf1MJHSh0oymUdo+VRr7y7Pmvhn27K8ecQ11rdBEWzswwOl8I9yuSbLpJreG3hBRh6KHHXT9uJvcGkParTRdO5QmHzXLRarbXZIFVbakSBqfZSuK5EtJ1c76XlXUNEf/WAhl03ibIvR4e0caDfY5Pf62zGkK0VE2Zu7KwNFoai8dfVGihMC86Wx7ZbPBasajs1SmUIzxKKdRel+jqDdNqzTVP4PvzAbW8W/Md4qc/30BRHi63DdEGxPesSDaPuGVZfgWZyxHVZm0reG/gZF/4sp9cwoZ4PTOlUc27nvx6Br/nrHxhzDc69n1v5ynNMPM89Tr4agjgWxfjmoNZE1+oP1EI/vRiD40GuHTmOiP9srC30x+ur+6wXMYSGso0uP7Jw4au/98LwsFbshp58jx1EnaL2qnzjEz2y7YmE38+8ptrCL48WU2vnM2smVOo28P/9z5b6cfL3jn+PfZLIDRqX1MnRo1yd/FZYbE1D7UntCLq3xlmf09h8ZTpsxSBTnNzz54hgFvfuLhGcmsOhLh1XvPwgvob/4D</diagram><diagram id="4G2OQQ1zny9nMmV_kp8x" name="Initialization">7Vxbc5s4FP41ns0+NMPd9mOcpG2m7SSzaWd3H2WQbW0wcoWc2P31K4m7hG05AXxJXxI4gIBzPn06N9yzr+erTwQsZt9wAMOeZQSrnn3Ts6yh47G/XLBOBF7fSgRTgoJEZBaCR/QLpkIjlS5RAOPKiRTjkKJFVejjKII+rcgAIfiletoEh9W7LsAUKoJHH4Sq9G8U0FkiHVj9Qv4Zouksu7PpDZMjc5CdnL5JPAMBfimJ7NuefU0wpsnWfHUNQ667TC/W9y/o3iL3yPeij//9+MvyP8EPyWAf97kkfwUCI9rs0Kktn0G4TPX1CH/2LC9k9xmNCdua8i2BiusZ9J8gSZVB15mGmV4WfHM5D7+iCQxRxPZGC0jQHFJ2vn0TpuKHQjZ6mSEKHxfA55e+MOgx2YzOQ7Znsk0GBwrYJSTfD0OwiNFY3NVgEgL9JYnRM/wLxgnquBQvKb/TdY4mLpywwVJkmsxsIxCiacR2fKZP8TCpFiChcCXBZofOzRwIbAJBzN6OrNl16Sj9FDrp3Bmkuy8FEE0jlc1KIBxmkAMp+Kf5yIWB2UZq4z3s3VfsrZizZIQFRhEVj+COeu6NZFVM6AxPcQTCsl1b1LW1VdeOW9G1U6drVdVOW5rOTPgOVG2aerq2W9O1+W50bRmH1rW6ZJyrrm3r0Lp23o2uHU2+NptYGn8i//rh+dPL55X1wwi+jb5EcPqhW752SroO4YR2p2lPE9VeW4oevhNFDzQV3YQLUqtoU4W0z334u+gZEAQievGnonkYsOgp3S2Ue1tIy066pNeYefMomn4VezecTWAUXPEYju2OQ+w/cbcdL6MABqlnztRN1v+kw4mdf2t8dic3Gn+8iskoIFNId6PttaYlMASUBRmVm9ZZKr30gcO1gIQrBwCSrWO8JD5MLyrMzZQG1qXT0kmw8TZ9t/Y2BXiSAQso5W/4BnR163Qdbh73NZemJgiz9mltRdHfCYhiRBGO1Fj9dsUCY4rJ3XwRKgb5HatvtHrOw0cTrJ+092dvVbbCi1ozrDVHe3C+mpZj9UOTWcfLxiF1ffD40TxjBpHzIvahcX3SqdX9cK1J161FkCfsee6laK9DRdc+rasoGkXM7WTa+MXdtpiyIDK+8PnWHTughpMlM3BtIR+EV6kqx5hSPK8PEvOwMI8R68JCSy8s3OZb6fmM7JVEnLZ/RPHG8DGvPWart2zpDfHjK2K82rfyFPsTSJckequd8QKyQ6MAxDORCkii/6x6POB7K0RzALBtYf/LoasPgZ0m2xMCOyHVDQQs26sOkTxXaxBQs3ULArnOihj0gj0hG9zgFGA0zwFbU0Nv4YDBSXCA7UqejhxvtswBNVnEjAQMSpioMy4w2+OCPaFwIC5QoNDvd8oFpqVAAcTxcl7hghMiAHOvzJEOA3Rjd9vsmALUDGTXfkCLc39fFBzJ5Le9jie/GgzEEVjEM1xXRzreOX8anr9C9cOOp/xm19+Iz2Pan4b/r0x7p+Npr+bGY3BaM76/n6GPZMY7Hcf6phrpnZ+fvy8WjmTSu2a3k95S1/qs0MwtUcGB93OJswMfkuruFTvBNhar4mBWnL7L0oegXLxmz5gMm5ykII3CFe3Vdp7kqW8ZgXMUBKJdhfCKMyhK0Wo2GCwpTqvS5kaoNV9v9qS8Tk2qt99lschS5791yfZFbMfQDPl0mIm/pe4DkfTpidq5QTH78/jtO/s7XnKQBFwQYSoel8eJYgjA9/lFxoy9hGVMEGGEINs861Rgl8PdLQhj4D9NRWvRfdJUkMoDQJ7ueVsSXQsyMWQyqUnuT1AYXuMQE/Eg9mQysXyfyWNK8BMsHQm8sed6/Eg62LBFuNgSXsya2kAOokrHpNxz1FxfikbLZGkBiLBoNqksACUTalJ8Y6v4QJfhh/V2KendrVF7JnvrSmBLNNHX8wrUgQbSQHIaseUlxVaLdg6nlyuJGGoo5sxowjI6pAnb1aSJQWssoSYNT4glTF1H0N5gl25owjGrZndfSxOOhB+3a5pQU40up4m7OOEGAoVL0RMfjDKWCJAvWML+yF2V1LeIk3oUSq5J/pUJBfh0CcKQmwdG3DcMxPWnTy2deiCOLrXIqavmqEWjv+mIqaWvSy0bmkY68kCkj1g9zfqjSi3WDo5qm1rUlKaClmNtG9rRuiz5dt6hmzxttRlugfynctt6l9lDze9HtqLm6LOHGyDQUfbQVtPER1Yi3AKCnTbbFwQHSxtKIBh2mza01RSSx523Bzb32T++/Eqe2IQwe2dBX9pYFEgnyR+4XLxAERQ+QzGmcOOSoVFUOHxwBeaLEKp1it9u3Xa3zh24em5de4klR6PB93V+nVPmi0urwhgu87OS/ZtVr+g8vFmXdkqL/Y2xmVAaWywy4tm9TB1VlmooZ6lfm6UayGmJlhnMUZMVtkiCgydOMIDbLG16+E0sexJLHgfuIha3NV5RkwsN8krrXKBJBc4G5+Iw4aKtWcbeGS4qTW9tU4GaXDDlelj+5UOvXP06A14YdFnJqil91vJCa7/V5NSVu0+GFxxdXnAOygvDqtUdzR5WlRecHQTTHC/UfnymeggRXNFHyhih666ot/wuRuOtz/Xgemtdw6gau99eG2Stlo6+8Vkzq9EEBA6U1JAhMGivAbJWS+ra0M/dgCyNIdb+JInByYArfz0f4xD5AiWMGtJSN0dEdmYyomXgCX/ZP7JhVvzVIp4EmWChcH7w8iy8ii6jjb6uV9FIGqMWORpfhB+FV7GNHHauI+4hnQpTSngqv8Wi61RYMsk0Vptiu8VPBCenF7+zbN/+Dw==</diagram><diagram name="Step" id="kx84utV55QcZ6GF4Z7hi">7V3bkuI4Ev0aYnsfusN38GPdZqc6umcqhp7b04awBTjKWIwtGtivX0mWjS2JQlBYQMNLhS1s2c5Mncw8Sql67sNs9Z8czKdfUQzTnmPFq5772HOc0AvIX9qwLhuCvlM2TPIkLpvsTcMw+R/kjRZvXSQxLFoXYoRSnMzbjRHKMhjhVhvIc7RsXzZGafupczCBUsMwAqnc+mcS42nZOnD6m/afYTKZVk+2g7D8ZQaqi/mXFFMQo2WjyX3quQ85Qrg8mq0eYEplV8nl8wsYRVPv0R0+vQ6fv8L/xujLx7Kzn/a5pf6EHGb4uF1zXX4H6YLLawj/6TlBSp5zP8rJ0YQeMat4mMLoFeZcGHhdSZjIZU4PF7P0SzKGaZKRs/s5zJMZxOR69zHlzS+btvvlNMFwOAcRvXVJTI+0TfEsJWc2OSTmgAG5Ja/P0xTMi2TEnmqRlhxGi7xIvsPfYFFaHW1FC0yf9FBbE20ck864ZdpEbfcgTSYZOYmIPNnLcCnAHMOVYDY7ZG7XhkAGEETk6/I1uY/30uemw8fOgJ8uN4ZoW7xt2jRCK+StgFv/pO56o2FywJW8h8JdSeGSPhtamKMkw+wV/Pue/yioFeV4iiYoA2lTsR0K23lT2J7fEranErYsa68rSftXI2lbU9R+V6IOrkbUtTPaIWq3K1H3r0fUSrQ2KOqBUVF7DVGncIzNCXrg6wk66ErQ4ZUI2rY0Jd2ZT6we1hB1RKPK5+w7yBOQ4Q//lkQPYxLP89ONdJ82rc2wURBsQeLLJJt8YWePFE1gFt/RrIKcjlIUvdJAEi2yGMY8ViTyztd/8e7Yyd+KKNKrtUZf7wCdkSwI5BP41nWhWrc5TAEmYW/roSpN8VtfqL1ubMK3BJsQ8atAizyC/K6NvonUwLpxGR8GW5/TF23PtQTzKXvcGFP9je+wL/tKhnLYPzFm2nLm+C0HWZHgBGVyAvm0ItkaRvnzbJ5KGrklkFvVXkPx+WSQxOovOAS09/OY4YljQPuis8j9hO1oRifdCfui88j9hK2Z3HTnPy46kdxP1q59amGbTSVPKmzPOrWwLzid3E/U4ant2pPTyR9U1H3NQOQYov79bpn8+fH++fPyc2C/3H3+I1s5H81K+qQI4mvS2Z2ZdSXbhrDnOaRfuUmxPpCHk96tX+AKWzJp0tAFFVgSgfSOy3OEMEYzNRWiR3447yA/+HUlyfCWDHp6JEmZjRydJXH9Lbz7DpbkWESGI8/T5RAv8ozKJCdN71Q4mkPy030Miiljvkp9V9P3A3q2SnBtCeSYGcKn0D+BLVQZ505j2DLMj20L/X67i/K9urMFOeEGRbGYtdDgB4SAQBcCfENqNwwBcupfQcA1jX3/pGPftsNPQjI3GFQtpsa/TEsUGZgXU6SaLrn4Ya/t+QMzw14kUrse9jIxUnv+4rqGvq4DMOP2Xc+w25dJmwJc94jvG8J4z3S0L1NG9Zgfg7S4snC/f2Yu3zMc8LsqsqWcUaW6aFlC8M8CVT98LKcx78gFrjVfbX6sZmGHSTYh99H74bzqkrxi2Wt5jWRqGK6wusiiZmZEE5wlccwqM3I6swo2U64yLwQWGPHZV3urrR1/XjUQnLyC8QlMTj25cuFCDiNEPvxDcXmIvxvJB6aG7sAskrsydXeNSZsp9fquYWSWaTnnEzlnTAz5NoqteMr+NophGEnbY6UcFkbkz/DrN/J3tKDfFtOGDGH2EZTVYV0Aep7QP1PyaSQKSHIY0yc907YZKKXZDhEoHZyM6zcoMJF1RA5YhR3thGSMy03vivdM6FVxUlDEpk8TTLaq0yFvS8F9RwHOCESvE1Zb92tZUsPbY5C//krr8vCaWaglWqhimmWcpOkDSlHOXsQdj8dOFJH2AufoFTZ+iYNR4Af0F95Z2KETcSsXUXkRxXxY7TJa1TlifHk8P6JRnNNAlQyxUqsWqjRUeLZEbzkOZcU0BO8r5F61vTczdAW9azKDckcDoSPRLrqGM5lidCnI3AlApICKBiz9CDjhWAZxwlVMMNaqb9qrGLwcDyY0Kp3OGCZ0OWF3y8yAGZjw7Lba/UNhwhPsxzcNEzIl6bFYpCixIYcshOmxRbwEJeIkYijh/kQvymoASTKCHiDlsQmPWKr7aezxUH4T/XA6IMmDLNu6xSH74ovnauJLd6tMNQrOzhhfdAkodwshaSgMEVYXB5qspYwvzg6g6hpfZPrTp/jyW8mA0DgjJ/lwndjwyS/6gllcJTjsDFE0aYUqN/TYFz38k6OHJ5Nh8yR6ba4vMUmIvWetly4h5llqHR2dMRkYrmLwzp4QO4J6d3oUY+oNHbOEmCcTYiGF7peEITL160Li2IJyXtYYCxeJq8c+LCFLOb9D1me6rrtOyuiSEVdwBWbzFMp0+Q3x30b8UFEyr0T8eqnZ8SG/M97KxPCu1lfsDhi3rOk1FDAKCWmgufRX7kgMGUSiomvU0VgVd7i11H7jk9PyHL7r8vPHFQ8T2Mm6cdIoaH+0jDkWnQDjrBjT8GDLExjTgWnLk4kzm00AgVfqjkArPbm5ob3ckGobIaUb6mwfIU9jUeIZeyFHFwu2VE6ehrZwxXU0h9IWtXszhAWVPBrWksEVHlJu03SZnokc1e5mQxJFEmO45NZXFd9cXY5qTL22ZbiS1pc5CDatYDUZpbIyo0xLM1avYRXr2QilrIaCTVjwqVGq7+rKskuSjdK6i9W/qm7o/EXJTY4RG1X0xxsVuXdEYKkqKsxmpv5lZ6ahJriXY+RUMYEt7EoVHjqV4VhCftDdVIZymbSCuZZW7tqblbv2+dR2Ni3krRXghw7xo7sR3emuY6lWdiIXtyK3CReXoePuKu+V3y+z2YF+eaddef+zLe+kAcmtvPPQaCRQTYwOFE7xGGVbSvM8RXGnLmbs9B/u+5RyGqIy0ExFdxKVgbinasdIdtn7xr05Lp2BsDeO5jZEx1i8o5S1zAlL+zNcUqDnnzYIcLZo11CYt3359Q8Q351YtVJ813c73ExBKQG5MLF/q3jvPHTqKxZYdlbxrtS7xqZ85kMnRR37W0Z73qGTWO4eitN0h5a7hyK31zWHY3YT8dPGTgb3EVcLW6ZVzmuXi52D036nZo7vVLsr8VQL4I296i5m94qdWH12ah50V+qpFoDMPgyOtgqI3rdt9Y/1bctKZZjdmKyDwrGB7rRaZ+GYzr725uMxWxvzvUuIyMRKG9sSI6lDS22k2O5g7CGnm/+gWV6++Tek7tP/AQ==</diagram><diagram name="Invariant checking" id="oWy5k7QknTCxPfUU-SjU">7Vtbc5s4FP41nuk+JMPd8WPipruZ2W3aut2mfdmRQQZtZESF8KW/vkcgY262cQpOMkkfOuiAhPyd70jfOSIDczxf/clRFPzDPEwHhuatBubbgWGMLAf+l4Z1ZnCGRmbwOfEyk741TMhPrIyasibEw3HpQcEYFSQqG10WhtgVJRvinC3Lj80YLb81Qj6uGSYuonXrV+KJILNeGMOt/S9M/GDzZt0ZZXfmaPOw+iVxgDy2LJjM64E55oyJ7Gq+GmMqsdvgwi9+Bmff9eju7npy+316H7gf/zvLBnt3TJf8J3Acim6HVr5cIJoovCb4x8BwKLznasrhypdXKSvGAXbvMVdgiPUGYcAlkpfJnP5NZpiSEFpXEeZkjgU8b76lyvxha7taBkTgSYRc2XUJ1ANbIOYUWjpcAh0Egi48b1OKophM07dqYOHYTXhMFvgTjjPWSStLhHzTOGeTNM5gMMVMHdx2hSjxQ2i4gGc6GYUC5gKvKrQ5gLmeEwECCDP4dXwN/dQoQ0UdFTsXqrncElHXlC0okNDeUA4p8vv5yFsHw4Xy8RH+Nmv+rrmz4ISIkVCkU7CvBvbbilcZFwHzWYho0a89Ym3sxdqyS1hbTVjXobb6Qnr4cpAetoPa7gDqj7dD/Qu9WZvvtU9ffPZ5fYaHZ/aLgVpvyereoHZeDNQ5hgegdvqC+uUsIGbLBaS3tVqvy6DPHIUxEYSFdTV0vQLpIRi/mUf0VQ21V0O5A5+MHNKfdZDpx0WZfroFrXG61uikYFsFsCmeiRNC3UjsEyJtWy8FaX30yLu09nIWEOuEC0gj1noNa9j1GPzwN/Ef+1CX0BAX0UuF3JQJweZwA4fepSwxSRtl7n1qgpneqY5p49uObTN7I/Yq5SeBuI/FYcY82DkcUyRgoy+9tQlr1fWD5NzWqTCudr7DsZtRYpZwF6uOFaflM3m4H+tqi2OR8PB3fcgiDLeuPBQH2MtduKlJXsjWiojcuXCd+vZ8ZLd3bwbN83KvMyyPklG0C/c2a/+6qIqRePN0QrSdjC2H8h752LkPdX1UcaE56i1Cm114sTNEtRmiMX4OodrWzcWQflw3W9aJI7VJkWfZrsS45GHnR8I2N86yFPMSHjC1aLW9ucmQ06MCEvoyiAIspxEuECdIjpmND/PNXpF1qPEJtIwo58A13VPl2Zx4nuwOuTDMD21z47rqQpC+qzRZ30mo7hNgp5z/GnU9ZTYJKrO304B6nmCeQ/smlj2l/yMWqyrDO2kPCw4lgiCaOg0JsIw3XYjsHLJS711FEngMH65+TJF773OWhN5tVs9Qdg/x+1voRcQ6XRy06uLQkJjMCKVjRhlPJ2LOZjPDdcEeC87uceGO50wd25F31GCjHolhVphhNmSQOV2K1KjuC91Ro0VRvbCehywtc5XW84IHH2fFbrGDZxFQ90sBd7upIqVsv7kDmJXzQbtat9+xzdcGsozKQFploJ43ErueBschiuKAnVz3We1Ss70Vqs542I/GN+1KEaSacfesDu2mRFypw/jJKMM9RDjot2OJcJBZpyGCoZ9WP9r1TF6X+mGCFjhXCpuFAC7ZLLe6CU+hhfvr+ZRR4m6lxKtYOEos6A0nlacVC3aLz0o6FwsHY27Dzs5W82xVeCyxkLsvL32b3YiF/CulU60adWmJ4hjCZCLD/w2E+U24eEaqYXPa8sxUQ83tfauG+rcjT6zs+zuK4VgSPBHFYBq9KYavd/77Bf56e+0vKLH//bbwfkZtjst63SgaJ9V19mk/alJpjKrn/vr5yCr8c7rZNmo16Z6pU086DKk1L+M4mWdqE4lcXobYR9nHO0XRWahCagGjnqxUCZ68Ss5jJafR8MVWb5Kz8ZitrjgtyYbPe/0sn/iUHRlv05Ms59BmHPaVas6SFkMlf9LK5hLJgRaEQXzCepSWPJfy8SVLKLS1/5NYpAEcMS4vkEx0gBcCc7xC84jKGbxS7SiqWQ1feJyWai0+pul1z9rH/4fsWbuPrZ/KlmWb5S2ro0THqX7n8OAdC5rbv/vJHt/+8ZR5/Qs=</diagram></mxfile>