## lustrec / test / src / kind_fmcad08 / misc / durationThm_3.lus @ 0cbf0839

History | View | Annotate | Download (690 Bytes)

1 |
-- |
---|---|

2 |
-- Source: Bertrand Jeannet |

3 |
-- |

4 | |

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

6 |
let |

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

8 |
tel |

9 | |

10 | |

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

12 |
-- how long has p been maintained true in the strict past |

13 |
let |

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

15 |
tel |

16 | |

17 |
-- Theorem 5: |

18 |
-- ((p -k-> q and ([[q]] => length <= m)) => ([[p]] => length <= k+m) |

19 | |

20 |
-- Not provable in luke-* |

21 |
node top (k0, m0: int; p, q : bool) returns (OK: bool); |

22 |
var k,m: int; |

23 |
env : bool; |

24 |
let |

25 |
k = k0-> pre(k); |

26 |
m = m0-> pre(m); |

27 |
env = Sofar( (k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)<= m) ); |

28 |
OK = env => (Age(p) <= k+m); |

29 |
--%PROPERTY OK=true; |

30 |
--%MAIN; |

31 |
tel |