--| Variable declarations
const
    NODE_NUM : 2;
    DATA_NUM : 2;
    BUF_SIZE : 4; --3
    TRANS_SIZE : 2; -- 1
type
    NODE : scalarset(NODE_NUM);
    absNODE : union { NODE, enum { Other } };
    DATA : scalarset(DATA_NUM);
    NODE_IND : 0..NODE_NUM - 1;
    BUF_IND : 0..BUF_SIZE - 1;
    BUF_INDP : 0..BUF_SIZE;
    TRANS_IND : 0..TRANS_SIZE - 1;
    TRANS_INDP : 0..TRANS_SIZE;
    CACHE_STATE : enum { I, S, E };
    CACHE : record
        State : CACHE_STATE;
        Data : DATA;
    end;
    MSG_CMD : enum { Empty, ReqS, ReqE, Inv, InvAck, GntS, GntE };
    MSG : record
        Cmd : MSG_CMD;
        Data : DATA;
    end;
    RNAME : enum { Norule, SendReqS, RecvReqS, SendReqE, RecvReqE, SendInv,
                   RecvInv, SendInvAck, RecvInvAck, SendGntS, RecvGntS,
                   SendGntE, RecvGntE, Store };
    TNAME : enum { Notrans, ReqSTr, ReqETr, SendInvTr };
    BUF_ENT : record
        Rname : RNAME;
        Tname : TNAME;
        multiple : boolean;
    end;
    DIR_REC : record
        Rname : RNAME;
        Tname : TNAME;
        agent : absNODE;
    end;
var
    Cache : array[NODE] of CACHE;
    Chan1 : array[NODE] of MSG;
    Chan2 : array[NODE] of MSG;
    Chan3 : array[NODE] of MSG;
    InvSet : array[NODE] of boolean;
    ShrSet : array[NODE] of boolean;
    ExGntd : boolean;
    CurCmd : MSG_CMD;
    CurPtr : absNODE;
    MemData : DATA;
    AuxData : DATA;
    otherbuffer : array[BUF_IND] of BUF_ENT;
    dirrec : DIR_REC;
    concbuffer : array[NODE] of array[TRANS_IND] of BUF_ENT;
    system_nondet : boolean;
    nondet0 : boolean;
--| Function and procedure declarations
function findindex1 ( t : TNAME) : BUF_INDP;
    begin
        for i : BUF_IND do
            if otherbuffer[i].Tname = t then
                return i;
            endif;
        endfor;
        return BUF_SIZE;
    end;
function findindex2 ( m : RNAME;  t : TNAME) : BUF_INDP;
    begin
        for i : BUF_IND do
            if (otherbuffer[i].Rname = m) & (otherbuffer[i].Tname = t) then
                return i;
            endif;
        endfor;
        return BUF_SIZE;
    end;
function find ( r : RNAME;  t : TNAME;  a : NODE) : TRANS_INDP;
    begin
        for i : TRANS_IND do
            if (concbuffer[a][i].Rname = r) & (concbuffer[a][i].Tname = t) then
                return i;
            endif;
        endfor;
        return TRANS_SIZE;
    end;
function findtrans ( t : TNAME;  a : NODE) : TRANS_INDP;
    begin
        for i : TRANS_IND do
            if concbuffer[a][i].Tname = t then
                return i;
            endif;
        endfor;
        return TRANS_SIZE;
    end;
function existsconctrans(t: TNAME; a: NODE): boolean;
var i: TRANS_INDP;

   begin
i := findtrans(t,a);
if i < TRANS_SIZE then return true; else return false;
endif;   
   end;

procedure entername ( rn : RNAME;  tn : TNAME;
                      a :NODE);
    var
        i : TRANS_INDP;
    begin
    --assert (rn != SendInv);
        i := find(Norule, Notrans, a);
        if i < TRANS_SIZE then
            concbuffer[a][i].Rname := rn;
            concbuffer[a][i].Tname := tn;
        else
            assert false;
        endif;
        --if (dirrec.Tname = tn) & (dirrec.agent = a) then
          --  dirrec.Rname := rn;
        --endif;
    end;
procedure removename ( tn : TNAME;  rp : RNAME;
                       a :NODE);
    var
        i : TRANS_INDP;
    begin
        i := find(rp, tn, a);
        if i < TRANS_SIZE then
            concbuffer[a][i].Rname := Norule;
            concbuffer[a][i].Tname := Notrans;
        else
            assert false;
        endif;
    end;
procedure enternameother ( rn : RNAME;  t : TNAME);
    var
        i : BUF_INDP;
    var
        j : BUF_INDP;
    begin
        i := findindex2(rn, t);
        if i < BUF_SIZE then
            otherbuffer[i].multiple := true;
        else
            j := findindex2(Norule, Notrans);
            if j < BUF_SIZE then
                otherbuffer[j].Rname := rn;
                otherbuffer[j].Tname := t;
                otherbuffer[j].multiple := false;
            else
                assert false;
            endif;
        endif;
        if (dirrec.Tname = t) & (dirrec.agent = Other) then
            dirrec.Rname := rn;
        endif;
    end;
procedure shiftup ( i : BUF_IND);
    begin
        for j : BUF_IND do
            if (j < (BUF_SIZE - 1)) & (j >= i) then
                otherbuffer[j].Rname := otherbuffer[j + 1].Rname;
                otherbuffer[j].Tname := otherbuffer[j + 1].Tname;
                otherbuffer[j].multiple := otherbuffer[j + 1].multiple;
            endif;
        endfor;
        otherbuffer[BUF_SIZE - 1].Rname := Norule;
        otherbuffer[BUF_SIZE - 1].Tname := Notrans;
        otherbuffer[BUF_SIZE - 1].multiple := false;
    end;
procedure removenameother ( t : TNAME;  r : RNAME);
    var
        i : BUF_INDP;
    begin
        i := findindex2(r, t);
        if i = BUF_SIZE then
            assert false;
        endif;
        if otherbuffer[i].multiple = true then
            otherbuffer[i].multiple := system_nondet;
        else
            shiftup(i);
        endif;
    end;
procedure removenamedir ( rn : RNAME;  tn : TNAME;  agent : absNODE);
    begin
        if ((dirrec.Rname = rn) & (dirrec.Tname = tn)) & (dirrec.agent = agent) then
            dirrec.Rname := Norule;
            dirrec.Tname := Notrans;
            dirrec.agent := Other;
        endif;
    end;
function existsbuf ( t : TNAME;  r : RNAME) : boolean;
    var
        i : BUF_INDP;
    begin
        i := findindex2(r, t);
        if i < BUF_SIZE then
            return true;
        else
            return false;
        endif;
    end;
function existsconc ( t : TNAME;  r : RNAME;
                      a : NODE) : boolean;
    var
        i : TRANS_INDP;
    begin
        i := find(r, t, a);
        if i < TRANS_SIZE then
            return true;
        else
            return false;
        endif;
    end;
function nosubtrans ( t : TNAME) : boolean;
    var
        i : BUF_INDP;
    var
        k : TRANS_INDP;
    begin
        i := findindex1(t);
        if i < BUF_SIZE then
            return false;
        else
            if t = SendInvTr then
                i := 2;
            else
                if t = ReqSTr then
                    i := 1;
                else
                    i := 0;
                endif;
            endif;
            for j : NODE do
                k := findtrans(t, j);
                if k < TRANS_SIZE then
                    return false;
                endif;
            endfor;
        endif;
        return true;
    end;
--| Rules
ruleset
    d : DATA
do
    startstate "Init"
    begin
        for i : NODE do
            Chan1[i].Cmd := Empty;
            Chan2[i].Cmd := Empty;
            Chan3[i].Cmd := Empty;
            Cache[i].State := I;
            InvSet[i] := false;
            ShrSet[i] := false;
        endfor;
        for i : BUF_IND do
            otherbuffer[i].Rname := Norule;
            otherbuffer[i].Tname := Notrans;
            otherbuffer[i].multiple := false;
        endfor;
        for i : NODE do
            for j : TRANS_IND do
                concbuffer[i][j].Rname := Norule;
                concbuffer[i][j].Tname := Notrans;
                concbuffer[i][j].multiple := false;
            endfor;
        endfor;
        dirrec.Rname := Norule;
        dirrec.Tname := Notrans;
        dirrec.agent := Other;
        ExGntd := false;
        CurCmd := Empty;
        MemData := d;
        AuxData := d;
        system_nondet := false;
        nondet0 := false;
    end
;
end;
ruleset
    d : DATA
do
    rule "absStore"
ExGntd & forall i: NODE do Cache[i].State = I &  Chan2[i].Cmd != GntE & Chan3[i].Cmd != InvAck endforall
--ctc1
    ==>
    begin
        AuxData := d;
       -- removenamedir(RecvGntE, ReqETr, Other);
        nondet0 := false;
    end
;
end;
ruleset
    i : NODE;
    d : DATA
do
    rule "Store"
      Cache[i].State = E
    ==>
    begin
        Cache[i].Data := d;
        AuxData := d;
        --removenamedir(RecvGntE, ReqETr, i);
        nondet0 := false;
    end
;
end;
ruleset
    i : NODE
do
    rule "SendReqS"
      (Chan1[i].Cmd = Empty) & (Cache[i].State = I)
    ==>
    begin
        Chan1[i].Cmd := ReqS;
        nondet0 := false;
    end
;
end;
ruleset
    i : NODE
do
    rule "SendReqE"
      (Chan1[i].Cmd = Empty) & ((Cache[i].State = I) | (Cache[i].State = S))
    ==>
    begin
        Chan1[i].Cmd := ReqE;
        nondet0 := false;
    end
;
end;
    rule "absRecvReqS"
      CurCmd = Empty
    ==>
    begin
        CurCmd := ReqS;
        CurPtr := Other;
        for j : NODE do
            InvSet[j] := ShrSet[j];
        endfor;
        enternameother(RecvReqS, ReqSTr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "RecvReqS"
      (CurCmd = Empty) & (Chan1[i].Cmd = ReqS)
    ==>
    begin
        CurCmd := ReqS;
        CurPtr := i;
        Chan1[i].Cmd := Empty;
        for j : NODE do
            InvSet[j] := ShrSet[j];
        endfor;
        entername(RecvReqS, ReqSTr, i);
        nondet0 := false;
    end
;
end;
    rule "absRecvReqE"
      CurCmd = Empty
    ==>
    begin
        CurCmd := ReqE;
        CurPtr := Other;
        for j : NODE do
            InvSet[j] := ShrSet[j];
        endfor;
        enternameother(RecvReqE, ReqETr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "RecvReqE"
      (CurCmd = Empty) & (Chan1[i].Cmd = ReqE)
    ==>
    begin
        CurCmd := ReqE;
        CurPtr := i;
        Chan1[i].Cmd := Empty;
        for j : NODE do
            InvSet[j] := ShrSet[j];
        endfor;
        entername(RecvReqE, ReqETr, i);
        nondet0 := false;
    end
;
end;
    rule "absSendInv"
(CurCmd = ReqE) | ((CurCmd = ReqS) & (ExGntd = true))

-- & (forall i : NODE do Cache[i].State != E & Chan2[i].Cmd != GntE endforall)
    ==>
    begin
        --*enternameother(SendInv, SendInvTr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "SendInv"
      ((Chan2[i].Cmd = Empty) & (InvSet[i] = true)) & ((CurCmd = ReqE) | (
                                                       (CurCmd = ReqS) & (
                                                       ExGntd = true)))
    ==>
    begin
        Chan2[i].Cmd := Inv;
        InvSet[i] := false;
        --*entername(SendInv, SendInvTr, i);
        nondet0 := false;
    end
;
end;
    rule "absSendInvAck"
      existsbuf(SendInvTr, SendInv)
    ==>
    begin
        --*removenameother(SendInvTr, SendInv);
        --*enternameother(SendInvAck, SendInvTr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "SendInvAck"
      ((Chan2[i].Cmd = Inv) & (Chan3[i].Cmd = Empty)) --& (existsconc(SendInvTr,SendInv,i))
    ==>
    begin
        Chan2[i].Cmd := Empty;
        Chan3[i].Cmd := InvAck;
        if Cache[i].State = E then
            Chan3[i].Data := Cache[i].Data;
        endif;
        Cache[i].State := I;
        undefine Cache[i].Data;
        --*removename(SendInvTr, SendInv, i);
        --*entername(SendInvAck, SendInvTr, i);
        nondet0 := false;
    end
;
end;
    rule "absRecvInvAck"
(CurCmd != Empty) & (forall j: NODE do Cache[j].State != E & Chan2[j].Cmd != GntE & Chan3[j].Cmd != InvAck endforall)

--& (existsbuf(SendInvTr, SendInvAck))
--ctc1 
    ==>
    begin
        if ExGntd = true then
            ExGntd := false;
--modified with data prop
            MemData := AuxData;
        endif;
        --*removenameother(SendInvTr, SendInvAck);
        --removenamedir(SendInvAck, SendInvTr, Other);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "RecvInvAck"
      ((Chan3[i].Cmd = InvAck) & (CurCmd != Empty)) --& (existsconc(SendInvTr, SendInvAck, i))
    ==>
    begin
        Chan3[i].Cmd := Empty;
        ShrSet[i] := false;
        if ExGntd = true then
            ExGntd := false;
            MemData := Chan3[i].Data;
            undefine Chan3[i].Data;
        endif;
        --*removename(SendInvTr, SendInvAck, i);
        --removenamedir(SendInvAck, SendInvTr, i);
        nondet0 := false;
    end
;
end;
    rule "absSendGntS"
      ((((CurCmd = ReqS) & (CurPtr = Other)) & (ExGntd = false)) & (existsbuf(
                                                                              ReqSTr, RecvReqS))) --(nosubtrans(SendInvTr )
    ==>
    begin
        CurCmd := Empty;
        undefine CurPtr;
        removenameother(ReqSTr, RecvReqS);
        --removenamedir(RecvReqS, ReqSTr, Other);
--enternameother(SendGntS,ReqSTr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "SendGntS"
      (((((CurCmd = ReqS) & (CurPtr = i)) & (Chan2[i].Cmd = Empty)) & (
                                                                       ExGntd = false)) & (existsconc(ReqSTr, RecvReqS, i)) ) --&  (nosubtrans(SendInvTr ))
    ==>
    begin
        Chan2[i].Cmd := GntS;
        Chan2[i].Data := MemData;
        ShrSet[i] := true;
        CurCmd := Empty;
        undefine CurPtr;
        removename(ReqSTr, RecvReqS, i);
        --removenamedir(RecvReqS, ReqSTr, i);
--entername(SendGntS,ReqSTr,i);
        nondet0 := false;
--assert (nosubtrans(SendInvTr));
    end
;
end;
    rule "absSendGntE"
      (((((CurCmd = ReqE) & (CurPtr = Other)) & (ExGntd = false)) & forall 
                                                                    j : NODE do 
                                                                    ShrSet[j] = false end) & (existsbuf(
       ReqETr, RecvReqE))) -- & (nosubtrans(SendInvTr 
    ==>
    begin
        ExGntd := true;
        CurCmd := Empty;
        undefine CurPtr;
        removenameother(ReqETr, RecvReqE);
        --removenamedir(RecvReqE, ReqETr, Other);
--enternameother(SendGntE,ReqETr);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "SendGntE"
      ((((((CurCmd = ReqE) & (CurPtr = i)) & (Chan2[i].Cmd = Empty)) & ( ExGntd = false)) & forall j : NODE do ShrSet[j] = false end))


-- & (existsconc(ReqETr, RecvReqE, i) & (nosubtrans(SendInvTr ))))
    ==>
    begin
        Chan2[i].Cmd := GntE;
        Chan2[i].Data := MemData;
        ShrSet[i] := true;
        ExGntd := true;
        CurCmd := Empty;
        undefine CurPtr;
        removename(ReqETr, RecvReqE, i);
        --removenamedir(RecvReqE, ReqETr, i);
        nondet0 := false;
--entername(SendGntE, ReqETr, i);
--assert (nosubtrans(SendInvTr));         
    end
;
end;
    rule "absRecvGntS"
      existsbuf(ReqSTr, SendGntS)
    ==>
    begin
        --removenameother(ReqSTr, SendGntS);
        --removenamedir(SendGntS, ReqSTr, Other);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "RecvGntS"
      (Chan2[i].Cmd = GntS) --& (existsconc(ReqSTr, SendGntS, i))
    ==>
    begin
        Cache[i].State := S;
        Cache[i].Data := Chan2[i].Data;
        Chan2[i].Cmd := Empty;
        undefine Chan2[i].Data;
        --removename(ReqSTr, SendGntS, i);
        --removenamedir(SendGntS, ReqSTr, i);
        nondet0 := false;
    end
;
end;
    rule "absRecvGntE"
      existsbuf(ReqETr, SendGntE)
    ==>
    begin
        --removenameother(ReqETr, SendGntE);
        --removenamedir(SendGntE, ReqETr, Other);
        nondet0 := false;
    end
;
ruleset
    i : NODE
do
    rule "RecvGntE"
      (Chan2[i].Cmd = GntE) --& (existsconc(ReqETr, SendGntE, i))
    ==>
    begin
        Cache[i].State := E;
        Cache[i].Data := Chan2[i].Data;
        Chan2[i].Cmd := Empty;
        undefine Chan2[i].Data;
        --removename(ReqETr, SendGntE, i);
        --removenamedir(SendGntE, ReqETr, i);
        nondet0 := false;
    end
;
end;

rule "setnondet"
  TRUE
==>
begin
    system_nondet := TRUE;
end;
rule "resetnondet"
  TRUE
==>
begin
    system_nondet := FALSE;
end;
invariant "CntrlProp"
    forall i : NODE do forall j : NODE do (i != j) -> (((Cache[i].State = E) -> (
                                                        Cache[j].State = I)) & (
                                                       (Cache[i].State = S) -> (
                                                       (Cache[j].State = I) | (
                                                       Cache[j].State = S)))) end end;

invariant "DataProp"
  ( ExGntd = false -> MemData = AuxData ) &
  forall i : NODE do Cache[i].State != I -> Cache[i].Data = AuxData end;

--| End of model

---non-interference lemmas-----


invariant "CTC2"
  forall i : NODE do
    Cache[i].State = E ->
    ExGntd = true &   -- 4
    forall j : NODE do
      j != i -> Cache[j].State = I  &   -- & 6
                --Chan2[j].Cmd != GntS &   -- 6
                Chan2[j].Cmd != GntE &  -- &  6
                Chan3[j].Cmd != InvAck   -- 7
    end
  end;

invariant "CTC1"
                                 forall i: NODE do forall j: NODE do (i != j) -> (Chan3[i].Cmd = InvAck & ExGntd = true & CurCmd != Empty -> (Cache[j].State != E & Chan2[j].Cmd != GntE & Chan3[j].Cmd != InvAck)) end end;