Graded-CTL NuSMV

Source Code for "SyncArb5"

--syncarb.smv:

MODULE arbiter-element(above,below,init-token)

VAR
Persistent : boolean;
Token : boolean;
Request : boolean;

ASSIGN
init(Token) := init-token;
next(Token) := token-in;
init(Persistent) := 0;
next(Persistent) := Request & (Persistent | Token);

DEFINE
above.token-in := Token;
override-out := above.override-out | (Persistent & Token);
grant-out := !Request & below.grant-out;
ack-out := Request & (Persistent & Token | below.grant-out);

MODULE main

VAR
e5 : arbiter-element(self,e4,0);
e4 : arbiter-element(e5,e3,0);
e3 : arbiter-element(e4,e2,0);
e2 : arbiter-element(e3,e1,0);
e1 : arbiter-element(e2,self,1);

DEFINE
grant-in := 1;
e1.token-in := token-in;
override-out := 0;
grant-out := grant-in & !e1.override-out;