Last change
on this file since 3257 was
2949,
checked in by sacerdot, 7 years ago

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a prefixpoint.

File size:
924 bytes

Line  

1  include "common/Graphs.ma". 

2  

3  record property_lattice : Type[1] ≝ 

4  { l_property :> Type[0] 

5  ; l_bottom : l_property 

6  ; l_equal : l_property → l_property → bool 

7  ; l_included : l_property → l_property → bool 

8  ; l_is_maximal : l_property → bool 

9  }. 

10  

11  definition valuation ≝ λlatt : property_lattice.label → latt. 

12  definition rhs ≝ λlatt : property_lattice.valuation latt → latt. 

13  definition equations ≝ λlatt : property_lattice.label → rhs latt. 

14  

15  record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝ 

16  { fix_lfp :> valuation latt 

17  ; fix_correct : 

18  ∀l : label. 

19  (* inclusion suffices for correctness *) 

20  l_included latt (eqs l fix_lfp) (fix_lfp l) 

21  }. 

22  

23  definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs. 

24  

25  coercion apply_fixpoint: 

26  ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝ 

27  λlatt,eqs,f,l. fix_lfp … f l 

28  on _f: fixpoint ? ? to label → ?. 

Note: See
TracBrowser
for help on using the repository browser.