## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / traffic_e7_46.lus @ 0c9457a0

History | View | Annotate | Download (529 Bytes)

1 | |
---|---|

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

3 |
let |

4 |
Y = (true -> pre Y) or X; |

5 |
tel |

6 |
node Store( Delta : int ) returns ( Total : int ); |

7 |
var Prev : int; |

8 |
let |

9 |
Prev = 0 -> pre Total; |

10 |
Total = if Delta < 0 and Prev > 0 then Prev+Delta |

11 |
else if Delta > 0 and Prev < 10 then Prev+Delta |

12 |
else Prev; |

13 |
tel |

14 |
--@ ensures OK; |

15 |
node top( Delta : int ) returns ( OK : bool ); |

16 |
var Total : int; |

17 |
let |

18 |
Total = Store( Delta ); |

19 |
OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; |

20 |
--%MAIN; |

21 |
--%PROPERTY OK=true; |

22 |
tel |