PartialRefBasics.pvs

PartialRefBasics[Conf: TYPE,
                     FM: TYPE,
                     {||}: [FM -> set[Conf]],
                     Asset: TYPE,
                     AssetName: TYPE,
                     CK: TYPE,
                     (IMPORTING maps[AssetName,Asset]) [||]: [CK -> [mapping -> [Conf -> finite_sets[Asset].finite_set]]] ]: THEORY
BEGIN
     
   % --------------------------------------------------------------------------------------------------------
   % ------------------------------------------------VARIABLES-----------------------------------------------
   % -------------------------------------------------------------------------------------------------------- 
    c: VAR Conf
    s: VAR set[Conf]
    fm1,fm2: VAR FM
    an: VAR AssetName
    a1,a2: VAR Asset
    anSet: VAR finite_sets[AssetName].finite_set
    ck1,ck2: VAR CK

    IMPORTING SPLrefinement[Conf,FM, Asset,AssetName,CK,{||},[||]]  
    am,am1,am2: VAR AM  

   % --------------------------------------------------------------------------------------------------------
   % ------------------------------------------------FM PARTIAL REFINEMENT-----------------------------------
   % --------------------------------------------------------------------------------------------------------      
    fmPartialRefinement(fm1,fm2,s) : bool = 
          FORALL c: s(c) => {||}(fm1)(c) AND {||}(fm2)(c)

    fmPartRef: LEMMA FORALL fm1,fm2: (fm1 |= fm2) <=> fmPartialRefinement(fm1,fm2,{|fm1|})

   % --------------------------------------------------------------------------------------------------------
   % ------------------------------------------------AM PARTIAL REFINEMENT-----------------------------------
   % -------------------------------------------------------------------------------------------------------- 
    amPartialRef(am1,am2,anSet) : bool =
          |>(filter(anSet,am1),filter(anSet,am2))
            

   % --------------------------------------------------------------------------------------------------------
   % ------------------------------------------------CK WEAKER EQUIVALENCE-----------------------------------
   % -------------------------------------------------------------------------------------------------------- 
    ckWeakerEq(ck1,ck2,s) : bool = 
          FORALL am,c : s(c) => ([|ck1|](am))(c) = ([|ck2|](am))(c)   

END PartialRefBasics