## lustrec / bench / distrib / misc / durationThm_1_e3_389_e5_5 / durationThm_1_e3_389_e5_5.lus @ 43a2cae9

History | View | Annotate | Download (522 Bytes)

1 | |
---|---|

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

3 |
let |

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

5 |
tel |

6 |
node Age (p: bool) returns (age_of_p: int); |

7 |
let |

8 |
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1- 1 else 0; |

9 |
tel |

10 |
--@ ensures OK; |

11 |
node top (ik, im: int; p, q, r : bool) returns (OK: bool); |

12 |
var k,m : int; |

13 |
env : bool; |

14 |
let |

15 |
k = ik -> pre k; |

16 |
m = im -> pre m; |

17 |
env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)>=m => r)); |

18 |
OK = env => (true -> ( (Age(p)>=k+m) => r )); |

19 |
--%MAIN; |

20 |
--%PROPERTY OK=true; |

21 |
tel |