### Profile

Download (5.01 KB) Statistics
| Branch: | Tag: | Revision:
1 2 3 0cbf0839 ploc ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and X9; ``` ```tel ``` ```node readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool) ``` ```returns(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int); ``` ```var ``` ``` garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8, garde9 : bool; ``` ```let ``` ``` garde1 = pre x0>=1; ``` ``` garde2 = pre x1>=1 and pre x4>=1; ``` ``` garde3 = pre x2>=1 and pre x11>=1; ``` ``` garde4 = pre x1>=1; ``` ``` garde5 = pre x6>=1; ``` ``` garde6 = pre x3>=1 and pre x7>=1; ``` ``` garde7 = pre x8>=1 and pre x12>=1; ``` ``` garde8 = pre x4>=5 and pre x5>=1 and pre x7>=1; ``` ``` garde9 = pre x9>=1 and pre x10>=1; ``` ``` x0 = 0 -> ``` ``` if(etat1) then if(garde1) then pre x0-1 else pre x0 else ``` ``` if(etat2) then if(garde2) then pre x0+1 else pre x0 else ``` ``` pre x0; ``` ``` x1 = 0 -> ``` ``` if(etat1) then if(garde1) then pre x1+1 else pre x1 else ``` ``` if(etat2) then if(garde2) then pre x1-1 else pre x1 else ``` ``` if(etat3) then if(garde3) then pre x1+1 else pre x1 else ``` ``` if(etat4) then if(garde4) then pre x1-1 else pre x1 else ``` ``` pre x1; ``` ``` x2 = 1 -> ``` ``` if(etat3) then if(garde3) then pre x2-1 else pre x2 else ``` ``` if(etat4) then if(garde4) then pre x2+1 else pre x2 else ``` ``` pre x2; ``` ``` x3 = 0 -> ``` ``` if(etat2) then if(garde2) then pre x3+1 else pre x3 else ``` ``` if(etat6) then if(garde6) then pre x3-1 else pre x3 else ``` ``` pre x3; ``` ``` x4 = 0 -> ``` ``` if(etat2) then if(garde2) then pre x4-1 else pre x4 else ``` ``` if(etat6) then if(garde6) then pre x4+1 else pre x4 else ``` ``` if(etat7) then if(garde7) then pre x4+5 else pre x4 else ``` ``` if(etat8) then if(garde8) then pre x4-5 else pre x4 else ``` ``` pre x4; ``` ``` x5 = 0 -> ``` ``` if(etat4) then if(garde5) then pre x5+1 else pre x5 else ``` ``` if(etat8) then if(garde8) then pre x5-1 else pre x5 else ``` ``` pre x5; ``` ``` x6 = 0 -> ``` ``` if(etat5) then if(garde5) then pre x6-1 else pre x6 else ``` ``` if(etat6) then if(garde6) then pre x6+1 else pre x6 else ``` ``` pre x6; ``` ``` x7 = 0 -> ``` ``` if(etat5) then if(garde5) then pre x7+1 else pre x7 else ``` ``` if(etat6) then if(garde6) then pre x7-1 else pre x7 else ``` ``` if(etat7) then if(garde7) then pre x7+1 else pre x7 else ``` ``` if(etat8) then if(garde8) then pre x7-1 else pre x7 else ``` ``` pre x7; ``` ``` x8 = 1 -> ``` ``` if(etat7) then if(garde7) then pre x8-1 else pre x8 else ``` ``` if(etat8) then if(garde8) then pre x8+1 else pre x8 else ``` ``` pre x8; ``` ``` x9 = 0 -> ``` ``` if(etat4) then if(garde4) then pre x9+1 else pre x9 else ``` ``` if(etat9) then if(garde9) then pre x9-1 else pre x9 else ``` ``` pre x9; ``` ``` x10 = 0 -> ``` ``` if(etat8) then if(garde8) then pre x10+1 else pre x10 else ``` ``` if(etat9) then if(garde9) then pre x10-1 else pre x10 else ``` ``` pre x10; ``` ``` x11 = 1 -> ``` ``` if(etat3) then if(garde3) then pre x11-1 else pre x11 else ``` ``` if(etat9) then if(garde9) then pre x11+1 else pre x11 else ``` ``` pre x11; ``` ``` x12 = 1 -> ``` ``` if(etat7) then if(garde7) then pre x12-1 else pre x12 else ``` ``` if(etat9) then if(garde9) then pre x12+1 else pre x12 else ``` ``` pre x12; ``` ```tel ``` 3e36d4e0 ploc ```--@ ensures OK; ``` 0cbf0839 ploc ```node top(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool) ``` ```returns ( OK : bool ); ``` ``` var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int; ``` ``` env : bool; ``` ```let ``` ``` (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = ``` ``` readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9); ``` ``` env = Sofar( excludes9(etat1, etat2, etat3, etat4, etat5, ``` ``` etat6, etat7, etat8, etat9) and ``` ``` x0 > -32768 and x1 > -32768 and x2 > -32768 and ``` ``` x3 > -32768 and x4 > -32768 and x5 > -32768 and ``` ``` x6 > -32768 and x7 > -32768 and x8 > -32768 and ``` ``` x0 < 32767 and x1 < 32767 and x3 < 32767 and x4 < 32767 and ``` ``` x5 < 32767 and x6 < 32767 and x7 < 32767 and x8 < 32767 and ``` ``` x9 < 32767 and x10 < 32767 and x11 < 32767 and x12 < 32767); ``` ``` OK = x0 >= 0; ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```