cannot understand why this happens when creating variable of typedef Semaphore
mtype = {RED, GREEN};
show mtype NS_Light = RED,DN_Light = RED,SD_Light = RED,SW_Light = RED,SN_Light = RED,EW_Light = RED;
show bool NS_Req = false,DN_Req = false,SD_Req = false,SW_Req = false,SN_Req = false,EW_Req = false;
#define p 0
#define v 1
chan sema = [0] of { bit };
show chan chann[6] = [0] of {bool};
typedef Semaphore{
byte count = 1, i = 0;
chan ch = [6] of {pid};
}
Semaphore S;
inline wait(S){
atomic{
if :: S.count >= 1 ->
S.count --;
:: else ->
S.ch ! _pid;
!(S.ch ?? [eval(_pid)])
fi
}
}
inline signal(S){
atomic{
S.i = len(S.ch);
if :: S.i == 0 ->
S.count ++
:: else -> S.ch ? _ fi
}
}
#define NS_safe []!(NS_Light == GREEN && (DN_Light == GREEN || SD_Light == GREEN || SW_Light == GREEN || EW_Light == GREEN))
#define DN_safe []!(DN_Light == GREEN && (NS_Light == GREEN || SD_Light == GREEN || EW_Light == GREEN))
#define SD_safe []!(SD_Light == GREEN && (DN_Light == GREEN || NS_Light == GREEN || EW_Light == GREEN))
#define SN_safe []!(SN_Light == GREEN && (EW_Light == GREEN))
#define SW_safe []!(SW_Light == GREEN && (NS_Light == GREEN))
#define EW_safe []!(EW_Light == GREEN && (SN_Light == GREEN || DN_Light == GREEN || SD_Light == GREEN || NS_Light == GREEN))
#define safety NS_safe && DN_safe && SD_safe && SN_safe && SW_safe && EW_safe
//ltl {safety}
#define NS_life [](NS_Req && (NS_Light == RED) -> <>(NS_Light == GREEN))
#define DN_life [](DN_Req && (DN_Light == RED) -> <>(DN_Light == GREEN))
#define SD_life [](SD_Req && (SD_Light == RED) -> <>(SD_Light == GREEN))
#define SN_life [](SN_Req && (SN_Light == RED) -> <>(SN_Light == GREEN))
#define SW_life [](SW_Req && (SW_Light == RED) -> <>(SW_Light == GREEN))
#define EW_life [](EW_Req && (EW_Light == RED) -> <>(EW_Light == GREEN))
#define lifeness NS_life && DN_life && SD_life && SN_life && SW_life && EW_life
//ltl {lifeness}
#define NS_fair []<> !( NS_Light == GREEN && NS_Req)
#define DN_fair []<> !( DN_Light == GREEN && DN_Req)
#define SD_fair []<> !( SD_Light == GREEN && SD_Req)
#define SN_fair []<> !( SN_Light == GREEN && SN_Req)
#define SW_fair []<> !( SW_Light == GREEN && SW_Req)
#define EW_fair []<> !( EW_Light == GREEN && EW_Req)
#define fairness NS_fair && DN_fair && SD_fair && SN_fair && SW_fair && EW_fair
ltl {fairness}
/*proctype dijkstra(){
byte count = 1;
do :: (count == 1) ->
sema ! p; count = 0
:: (count == 0) ->
sema ? v; count = 1
od
}*/
proctype NS_Detection() {
do
:: !NS_Req -> NS_Req = true;
od
}
proctype DN_Detection() {
do
:: !DN_Req -> DN_Req = true;
od
}
proctype SD_Detection() {
do
:: !SD_Req -> SD_Req = true;
od
}
proctype SW_Detection() {
do
:: !SW_Req -> SW_Req = true;
od
}
proctype SN_Detection() {
do
:: !SN_Req -> SN_Req = true;
od
}
proctype EW_Detection() {
do
:: !EW_Req -> EW_Req = true;
od
}
proctype NS_CTL(chan NS_in, NS_out) {
do
:: wait(S);
if :: (NS_Req) -> NS_Light = GREEN;NS_Req = false;
:: else -> skip;
fi;
NS_Light = RED;
signal(S);
od
}
proctype DN_CTL(chan DN_in, DN_out) {
do
if :: (DN_Req) -> DN_Light = GREEN;DN_Req = false;
:: else -> skip;
fi;
DN_Light = RED;
signal(S);
od
}
proctype SD_CTL(chan SD_in, SD_out) {
do
:: wait(S);
if :: (SD_Req) -> SD_Light = GREEN;SD_Req = false;
:: else -> skip;
fi;
SD_Light = RED;
signal(S);
od
}
proctype SW_CTL(chan SW_in, SW_out) {
do
:: wait(S);
if :: (SW_Req) -> SW_Light = GREEN;SW_Req = false;
:: else -> skip;
fi;
SW_Light = RED;
signal(S);
od
}
proctype SN_CTL(chan SN_in, SN_out) {
do
:: wait(S);
if :: (SN_Req) -> SN_Light = GREEN;SN_Req = false;
:: else -> skip;
fi;
SN_Light = RED;
signal(S);
od
}
proctype EW_CTL(chan EW_in, EW_out) {
do
:: wait(S);
if :: (EW_Req) -> EW_Light = GREEN;EW_Req = false;
:: else -> skip;
fi;
EW_Light = RED;
signal(S);
od
}
init {
run NS_Detection();
run NS_CTL(chann[0], chann[1]);
run DN_Detection();
run DN_CTL(chann[1], chann[2]);
run SD_Detection();
run SD_CTL(chann[2], chann[3]);
run SW_Detection();
run SW_CTL(chann[3], chann[4]);
run SN_Detection();
run SN_CTL(chann[4], chann[5]);
run EW_Detection();
run EW_CTL(chann[5], chann[0]);
chann[0] ! true
}`
Syntax check get me Error: incomplete structure ref 'S' saw '')' = 41'