## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / ticket3i_6_e7_1096_e7_2688.lus @ 2d37a1e1

History | View | Annotate | Download (3.56 KB)

1 | |
---|---|

2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |

3 |
let |

4 |
Sofar = X -> X or pre Sofar; |

5 |
tel |

6 |
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); |

7 |
let |

8 |
excludes = not X1 or not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |

9 |
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 |

10 |
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 |

11 |
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 |

12 |
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 |

13 |
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 |

14 |
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 |

15 |
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 |

16 |
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 |

17 |
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; |

18 |
tel |

19 |
node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; |

20 |
init_a1, init_a2, init_a3, init_t : int) returns ( |

21 |
p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool); |

22 |
var |

23 |
g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; |

24 |
let |

25 |
erreur_ticket3i = if((p1>=3) or (p2>=3) or (p3>=3)) then true else false; |

26 |
g1 = pre p1 = 0; |

27 |
g2 = pre p1 = 1 and pre s >= a1; |

28 |
g3 = pre p1 = 2; |

29 |
g4 = pre p2 = 0; |

30 |
g5 = pre p2 = 1 and pre s >= a2; |

31 |
g6 = pre p2 = 2; |

32 |
g7 = pre p3 = 0; |

33 |
g8 = pre p3 = 1 and pre s >= a3; |

34 |
g9 = pre p3 = 2; |

35 |
p1 = 0 -> |

36 |
if(e1) then if(g1) then 1 else pre p1 else |

37 |
if(e2) then if(g2) then 2 else pre p1 else |

38 |
if(e3) then if(g3) then 0 else pre p1 else |

39 |
pre p1; |

40 |
p2 = 0 -> |

41 |
if(e4) then if(g4) then 1 else pre p2 else |

42 |
if(e5) then if(g5) then 2 else pre p2 else |

43 |
if(e6) then if(g6) then 0 else pre p2 else |

44 |
pre p2; |

45 |
p3 = 0 -> |

46 |
if(e7) then if(g7) then 1 else pre p3 else |

47 |
if(e8) then if(g8) then 2 else pre p3 else |

48 |
if(e9) then if(g9) then 0 else pre p3 else |

49 |
pre p3; |

50 |
t = init_t -> |

51 |
if(e1) then if(g1) then pre t+1 else pre t else |

52 |
if(e4) then if(g4) then pre t+1 else pre t else |

53 |
if(e7) then if(g7) then pre t+1 else pre t else |

54 |
pre t; |

55 |
s = t -> |

56 |
if(e3) then if(g3) then pre s+1 else pre s else |

57 |
if(e6) then if(g6) then pre s+1 else pre s else |

58 |
if(e9) then if(g9) then pre s+1 else pre s else |

59 |
pre s; |

60 |
a1 = init_a1 -> |

61 |
if(e1) then if(g1) then pre t else pre a1 else |

62 |
pre a1; |

63 |
a2 = init_a2 -> |

64 |
if(e4) then if(g4) then pre t else pre a2 else |

65 |
pre a2; |

66 |
a3 = init_a3 -> |

67 |
if(e7) then if(g7) then pre t else pre a3 else |

68 |
pre a3; |

69 |
tel |

70 |
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; |

71 |
init_a1, init_a2, init_a3, init_t : int ) |

72 |
returns ( OK : bool ); |

73 |
--@ contract guarantees OK; |

74 |
var p1, p2, p3, t, s, a1, a2, a3 : int; |

75 |
erreur_ticket3i : bool; |

76 |
env : bool; |

77 |
let |

78 |
( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) = |

79 |
ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9, |

80 |
init_a1, init_a2, init_a3, init_t ); |

81 |
env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |

82 |
init_a1 >= 0 and |

83 |
init_a2 >= 0 and |

84 |
init_a3 >= 0 and |

85 |
init_t >= 0 ); |

86 |
OK = env => 0 <= p3 and p3 <= 3; |

87 |
--%MAIN; |

88 |
--%PROPERTY OK=true; |

89 |
tel |