library CoCASL/Examples

%display  __union__          %LATEX __\cup__
%display  __setMinus__       %LATEX __\setminus__
%display  __disjointUnion__  %LATEX __\cup__
%display  __member__         %LATEX __\epsilon__
%display  __inCap__          %LATEX __in__

%left_assoc __||__, __+__, __-__

logic CoCASL

spec FinSet[sort Elem] =
free {
    type FinSet[Elem] ::= {} | {__}(Elem) | __union__(FinSet[Elem]; FinSet[Elem])
    op __union__ : FinSet[Elem] * FinSet[Elem] -> FinSet[Elem], 
                assoc, comm, idem, unit {} }
    then
    pred __member__: Elem * FinSet[Elem]
    forall x,y: Elem; M,N: FinSet[Elem]
    . not x member {}                                
    . x member {y} <=> x=y 
    . x member M union N <=> x member M \/ x member N
    then
    op __setMinus__, __disjointUnion__ : FinSet[Elem] * FinSet[Elem] -> FinSet[Elem]
    ops __-__,__+__ : FinSet[Elem] * Elem -> FinSet[Elem]
end

spec CntSet[sort Elem] =
   cofree cotype Seq[Elem] ::= nil | (head : Elem; tail : Seq[Elem])
   pred __elem__ : Elem * Seq[Elem]
   var x:Elem; s:Seq[Elem]
   . x elem s <=> (x=head(s) \/ x elem tail(s))
then free {
   generated type CntSet[Elem] ::= mkSet(Seq[Elem])
   var s1,s2: Seq[Elem]
   . mkSet(s1)=mkSet(s2) <=> forall x:Elem . x elem s1 <=> x elem s2
  }
then
    op {} : CntSet[Elem] = mkSet(nil)
    op __union__ : CntSet[Elem] * CntSet[Elem] -> CntSet[Elem], 
                assoc, comm, idem, unit {}
    pred __member__: Elem * CntSet[Elem]
    forall x: Elem; s: Seq[Elem]
    . x member (mkSet (s)) <=> x elem s
    op {__} : Elem -> CntSet[Elem];
       __setMinus__, __disjointUnion__ : 
                   CntSet[Elem] * CntSet[Elem] -> CntSet[Elem]
    ops __-__,__+__ : CntSet[Elem] * Elem -> CntSet[Elem]
end


spec ACDomain[sort Name] = FinSet[sort Name] then
cofree {
    sort State
    free type Cap ::= inCap | out | open         
    free type HCap ::= enter | coenter | exit | coopen
    free type Action ::= tau | action(Cap; name :? Name)
    free type HAct ::= haction(HCap; name : Name)
    free type Concretion ::= conc(State; State; FinSet[Name])
    then FinSet[sort State] and CntSet[sort Concretion]
    then cotype State ::= (next : Action -> FinSet[State];
                           harden : HAct -> CntSet[Concretion]; 
                           names : FinSet[Name]) }
end

spec Rename = ACDomain[sort Name] 
then op subst : Name * Name * Name -> Name;
        subst : Name * Name * Action -> Action;
        subst : Name * Name * HAct -> HAct;
        rename : Name * Name * State -> State;
        rename : Name * Name * FinSet[State] -> FinSet[State];
        rename : Name * Name * Concretion -> Concretion;
        rename : Name * Name * CntSet[Concretion] -> CntSet[Concretion]
     vars a : Action; b : HAct; c : Cap; h : HCap; m,n,o : Name; P,Q: State;
          C : Concretion; s1,s2 : FinSet[State]; cs1,cs2 : CntSet[Concretion];
          p : FinSet[Name]
     . subst(m,n,o) = n when m=o else o
     . subst(m,n,tau) = tau
     . subst(m,n,action(c,o)) = action(c,subst(m,n,o))
     . subst(m,n,haction(h,o)) = haction(h,subst(m,n,o))
     . next(a, rename(m,n,P)) = rename(m,n,next(subst(m,n,a),P))
     . harden(b, rename(m,n,P)) = rename(m,n,harden(subst(m,n,b),P))
     . names(rename(m,n,P)) = (names(P) - m) + n
     . rename(m,n,{}:FinSet[State]) = {}
     . rename(m,n,{P}) = {rename(m,n,P)}
     . rename(m,n,s1 union s2) = 
       rename(m,n,s1) union rename(m,n,s2)
     . rename(m,n,conc(P,Q,p)) = conc(rename(m,n,P),rename(m,n,Q),p)
     . rename(m,n,{}:CntSet[Concretion]) = {}
     . rename(m,n,{C}) = {rename(m,n,C)}
     . rename(m,n,cs1 union cs2) = 
       rename(m,n,cs1) union rename(m,n,cs2)
end

spec Zero = ACDomain[sort Name]
then op zero : State
     vars a : Action; b : HAct
         . next(a, zero) = {}
         . harden(b, zero) = {}
         . names(zero) = {}
end

spec CapabilityPrefixing = Zero
then op cap : Cap * Name * State -> State
     vars a : Action; b : HAct; c : Cap; n : Name; P: State
     . next(a, cap(c, n, P)) = { P } when a = action(c, n) else {}
     . harden(b, cap(c, n, P)) = {}
     . names(cap(c, n, P)) = { n } union names(P)
end

spec NameRestriction = ACDomain[sort Name] and Rename
then ops res : Name * State -> State;
         res : FinSet[Name] * State -> State; 
     vars a : Action; b : HAct; n : Name; P, Q : State; c : Concretion;
          p : FinSet[Name]; p,q : FinSet[Name] 
     . Q member next(a, res(n, P)) <=> 
        exists R : State . Q = res(n, R) /\ R member next(a, P) /\ not name(a)=n
     . c member harden(b, res(n, P)) <=>
        (exists R, S : State
         . c = conc(R, res(n, S), p)
           /\ conc(R, S, p) member harden(b, P) 
           /\ not n member names(R)) \/
        (exists R, S : State
         . c = conc(res(n, R), S, p) 
           /\ conc(R, S, p) member harden(b, P) 
           /\ not n member names(S)) \/
        (exists R, S : State; m : Name
         . c = conc(rename(n,m,R), rename(n,m,S), p union {m}) 
           /\ conc(R, S, p) member harden(b, P) 
           /\ not m member names(P) union p
           /\ not n member p
           /\ n member names(S)
           /\ n member names(R))
      . names(res(n, P)) = names(P) - n
      . res({},P) = P
      . res({n},P) = res(n,P)
      . res(p union q,P) = res(p,res(q,P))
end

spec AmbientAndParallel = Zero and NameRestriction
then ops amb : Name * State -> State;
         __||__ : State * State -> State, assoc  %implied
vars a : Action; b : HAct; cap : Cap;m, n : Name; P,Q : State; c : Concretion
  . Q member next(tau, amb(n, P)) <=>
     ( exists P', P'' : State; p: FinSet[Name]  .
                 Q = res(p, amb(n, P'') || P') /\
                 conc(P', P'', p) member  harden(haction(exit, n), P)) \/
     ( exists P' : State  . Q = amb(n, P') /\ P' member next(tau, P))
  . next(action(cap, n), amb(m, P)) = {}
  . c member harden(haction(enter, n), amb(m, P)) <=>
     ( exists P' : State . c = conc(amb(m, P'), zero, {}) /\
                          P' member next(action(inCap, n), P))
  . harden(haction(coenter, n), (amb(n, P))) = {conc(P, zero, {})}
  . c member harden(haction(exit, n), amb(m, P)) <=>
     ( exists P' : State  . c = conc(amb(m, P'), zero, {}) /\
                        P' member next(action(out, n), P))
  . harden(haction(coopen, n), (amb(n, P))) = {conc(P, zero, {})}
  . names(amb(n, P)) = {n} union names(P)

vars a : Action; b : HAct; n : Name; P, Q, R : State; c : Concretion
    . R member next(a, P || Q) <=>
      (a = tau /\ exists P',Q',Q'' : State; p : FinSet[Name]  .
        R = res(p, P' || Q' || Q'') /\ P' member next(action(open, n), P) /\
        conc(Q',Q'',p) member harden(haction(coopen, n),Q)) \/
      (a = tau /\  exists Q', P', P'' : State; p : FinSet[Name]  .
        R = res(p, P' || P'' || Q') /\ Q' member next(action(open, n),Q) /\
        conc(P', P'',p) member harden(haction(coopen, n), P)) \/
      (a = tau /\  exists P', P'',Q',Q'' : State; p,q : FinSet[Name]  .
        R = res(p union q,amb(n, P' || Q') || P'' || Q'') /\
        conc(P', P'',p) member harden(haction(enter, n), P) /\
        conc(Q',Q'',q) member harden(haction(coenter, n),Q)) \/
      (a = tau /\  exists P', P'',Q',Q'' : State; p,q : FinSet[Name]  .
         R = res(p union q,amb(n, P' || Q') || P'' || Q'') /\
         conc(P', P'',p) member harden(haction(coenter, n), P) /\
         conc(Q',Q'',q) member harden(haction(enter, n),Q)) \/
      ( exists P' : State  . R = P' || Q /\ P' member next(a, P)) \/
      ( exists Q' : State  . R = P || Q' /\ Q' member next(a,Q))
    . c member harden(b, (P || Q)) <=>
        ( exists P', P'' : State; p : FinSet[Name]  . 
           c = conc(P', P'' || Q, p) /\ conc(P', P'', p) member  harden(b, P)) \/
        ( exists Q',Q'' : State; p : FinSet[Name]  . 
           c = conc(Q', P || Q'', p) /\ conc(Q',Q'', p) member harden(b,Q))
    . names(P || Q) = names(P) union names(Q)
end

spec AmbientCalculus =
     CapabilityPrefixing and NameRestriction and AmbientAndParallel
end