## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / ticket3i_6.lus @ b745c1a8

History | View | Annotate | Download (3.58 KB)

1 | |
---|---|

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

3 |
let |

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

5 |
tel |

6 | |

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

8 |
let |

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

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

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

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

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

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

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

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

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

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

19 |
tel |

20 | |

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

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

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

24 |
var |

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

26 |
let |

27 | |

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

29 | |

30 |
g1 = pre p1 = 0; |

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

32 |
g3 = pre p1 = 2; |

33 |
g4 = pre p2 = 0; |

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

35 |
g6 = pre p2 = 2; |

36 |
g7 = pre p3 = 0; |

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

38 |
g9 = pre p3 = 2; |

39 | |

40 |
p1 = 0 -> |

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

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

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

44 |
pre p1; |

45 | |

46 |
p2 = 0 -> |

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

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

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

50 |
pre p2; |

51 | |

52 |
p3 = 0 -> |

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

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

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

56 |
pre p3; |

57 | |

58 |
t = init_t -> |

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

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

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

62 |
pre t; |

63 | |

64 |
s = t -> |

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

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

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

68 |
pre s; |

69 | |

70 |
a1 = init_a1 -> |

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

72 |
pre a1; |

73 | |

74 |
a2 = init_a2 -> |

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

76 |
pre a2; |

77 | |

78 |
a3 = init_a3 -> |

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

80 |
pre a3; |

81 | |

82 |
tel |

83 | |

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

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

86 |
returns ( OK : bool ); |

87 |
--@ contract guarantee OK; |

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

89 |
erreur_ticket3i : bool; |

90 |
env : bool; |

91 |
let |

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

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

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

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

96 |
init_a1 >= 0 and |

97 |
init_a2 >= 0 and |

98 |
init_a3 >= 0 and |

99 |
init_t >= 0 ); |

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

101 |
--%PROPERTY OK=true; |

102 |
--%MAIN; |

103 |
tel |