Error: incomplete structure ref 'S' saw '')' = 41'

25 views Asked by At

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'

0

There are 0 answers