edges([1,2,3,4,5,6,7,8]).

snodes([idle,busy,busyEx,busySH,loop,loopSH]).
cnodes([inv,waitEx,waitSh,sh,ex]).

init([inv],[idle],_).

reqEx(1).
reqInv(2).
reqDg(3).
reqSh(4).
markedEx(5).
markedSh(6).
pending(7).
markedEx1(8).

% Server

ccrule(a,inv,waitEx, RE,req-ex):-reqEx(RE).
ccrule(a,inv,waitSh, RS,req-sh):-reqSh(RS).

dcrule(a,ex,C,inv,ex-inv):-reqInv(C);markedEx(C).
dcrule(a,sh,C,inv,sh-inv):-reqInv(C);markedSh(C).

crule(a,waitEx,E,ex,E,wait-ex):-markedEx(E).
crule(a,ex,Dg,sh,S,   downgrade) :-reqDg(Dg),markedSh(S).
crule(a,waitSh,S,sh,S,wait-sh):-markedSh(S).

srule(a,idle,R,loop,P,idle-loopEx) :-reqEx(R),pending(P).
srule(a,loop,E,loop,I,inv-ex) :-markedEx(E),reqInv(I).
srule(a,loop,S,loop,I,inv-sh) :-markedSh(S),reqInv(I).
srule(a,busy,P,busyEx,E,busy-ex1) :-pending(P),markedEx1(E).
srule(a,busyEx,E,idle,E1,busy-ex) :-markedEx1(E),markedEx(E1).

srule(a,idle,R,loopSH,P,idle-loopSh)  :-reqSh(R),pending(P).
srule(a,loopSH,E,loopSH,R,dg-ex):-markedEx(E),reqDg(R).
srule(a,busySH,P,idle,S,busy-sh)  :-pending(P),markedSh(S).

trule(a,loop,busy,    [P,RE,RS],test-all-ex) :-pending(P),reqEx(RE),reqSh(RS).
trule(a,loopSH,busySH,[P,RE,RS,S],test-all-sh) :-pending(P),reqEx(RE),reqSh(RS),markedSh(S).

trule(a,busyEx,bad,[P,RE,RS,I,D,S,E],test-consistency) :-
   pending(P),reqEx(RE),reqSh(RS),reqInv(I),reqDg(D),markedSh(S),markedEx(Ex).

unsafe([G2]):-
 edges(Q),
 SS= idle,
 S=  [node(1,SS,Q)],
 S1= [node(1,SS,Q),node(2,SS,Q)],
 C=  [node(1,ex), node(2,ex)],
 E=  [edge(a,1,1,Ex),edge(a,1,2,Ex)],
 E3= [edge(a,1,1,Ex),edge(1,2,1,Ex)],
 C1= [node(1,ex), node(2,sh)],
 E2= [edge(a,1,1,Ex),edge(a,1,2,Sh)],
 S2= [node(1,bad,Q)],
 C4= [node(1,waitEx)],
 E4= [edge(a,1,1,Rex),edge(a,2,1,Rex)],
 S4= [node(1,SS,Q),node(2,SS,Q)],
 G1= unsafe(graph(1,2,[S,C,E])),
 G2= unsafe(graph(1,2,[S,C1,E2])),
 G3= unsafe(graph(1,0,[S2,[],[]])),
 G4= unsafe(graph(2,1,[S4,C4,E4])),
 markedEx(Ex),
 markedSh(Sh),
 reqEx(Rex).

invariants([]).
