## lustrec / test / src / kind_fmcad08 / misc / traffic_e7_46_e7_171.lus @ 22fe1c93

History | View | Annotate | Download (512 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 or Prev > 0 then Prev+Delta |

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

12 |
else Prev; |

13 |
tel |

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

15 |
var Total : int; |

16 |
let |

17 |
Total = Store( Delta ); |

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

19 |
--%MAIN; |

20 |
--%PROPERTY OK=true; |

21 |
tel |