### Profile

 1 ```-- ``` ```-- Source: David Merchat (node swimingpool) ``` ```-- ``` ```node First( X : int ) returns ( First : int ); ``` ```let ``` ``` First = X -> pre First; ``` ```tel ``` ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or ``` ``` X1 and not X2 and not X3 and not X4 and not X5 and not X6 or ``` ``` not X1 and X2 and not X3 and not X4 and not X5 and not X6 or ``` ``` not X1 and not X2 and X3 and not X4 and not X5 and not X6 or ``` ``` not X1 and not X2 and not X3 and X4 and not X5 and not X6 or ``` ``` not X1 and not X2 and not X3 and not X4 and X5 and not X6 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and X6; ``` ```tel ``` ```node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns ``` ```(x1, x2, x3, x4, x5, x6, x7, p1, p2 : int); ``` ```var ``` ``` g1, g2, g3, g4, g5, g6 : bool; ``` ```let ``` ``` g1 = false -> pre x6>=1; ``` ``` g2 = false -> pre x1>=1 and pre x7>=1; ``` ``` g3 = false -> pre x2>=1; ``` ``` g4 = false -> pre x3>=1 and pre x6>=1; ``` ``` g5 = false -> pre x4>=1; ``` ``` g6 = false -> pre x5>=1; ``` ``` x1 = 0 -> ``` ``` if(e1) then if(g1) then pre x1+1 else pre x1 else ``` ``` if(e2) then if(g2) then pre x1-1 else pre x1 else ``` ``` pre x1; ``` ``` x2 = 0 -> ``` ``` if(e2) then if(g2) then pre x2+1 else pre x2 else ``` ``` if(e3) then if(g3) then pre x2-1 else pre x2 else ``` ``` pre x2; ``` ``` x3 = 0 -> ``` ``` if(e3) then if(g3) then pre x3+1 else pre x3 else ``` ``` if(e4) then if(g4) then pre x3-1 else pre x3 else ``` ``` pre x3; ``` ``` x4 = 0 -> ``` ``` if(e4) then if(g4) then pre x4+1 else pre x4 else ``` ``` if(e5) then if(g4) then pre x4-1 else pre x4 else ``` ``` pre x4; ``` ``` x5 = 0 -> ``` ``` if(e5) then if(g5) then pre x5+1 else pre x5 else ``` ``` if(e6) then if(g6) then pre x5-1 else pre x5 else ``` ``` pre x5; ``` ``` x6 = p1 -> ``` ``` if(e1) then if(g1) then pre x6-1 else pre x6 else ``` ``` if(e3) then if(g3) then pre x6+1 else pre x6 else ``` ``` if(e4) then if(g4) then pre x6-1 else pre x6 else ``` ``` if(e6) then if(g6) then pre x6+1 else pre x6 else ``` ``` pre x6; ``` ``` x7 = p2 -> ``` ``` if(e2) then if(g2) then pre x7-1 else pre x7 else ``` ``` if(e5) then if(g5) then pre x7+1 else pre x7 else ``` ``` pre x7; ``` ``` p1 = init_p1 -> ``` ``` pre p1; ``` ``` p2 = init_p2 -> ``` ``` pre p2; ``` ```tel ``` ```node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int) ``` ```returns ( OK : bool ); ``` ```--@ contract guarantees OK; ``` ``` var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int; ``` ``` env : bool; ``` ```let ``` ``` (x1, x2, x3, x4, x5, x6, x7, p1, p2) = ``` ``` swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2); ``` ``` env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and ``` ``` 0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000; ``` ``` OK = env => x5 < 3; ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```