Search code examples
model-checkingspinpromela

Promela modeling with Spin

I am working on a promela model that is fairly simple. Using two different modules, it acts as a crosswalk/Traffic light. The first module is the traffic light that outputs the current signal (green, red, yellow, pending). This module also receives as an input a signal called "pedestrian" which acts as an indicator that there are pedestrians wanting to cross. The second module acts as the crosswalk. It receives output signals from the traffic light module (green, yellow, green). It outputs the pedestrian signal to the traffic light module. This module simply defines whether the pedestrian(s) is crossing, waiting or not present. My issue is that once the count value goes to 60, a timeout occurs. I believe the statement "SigG_out ! 1" is causing the error but I do not know why. I have attached the image of the trace I receive from the command line. I am completely new to Spin and Promela and so I am not sure how to use the information form the trace to find my issue in the code. Any help is greatly appreciated.

Here is the code for the complete model:

mtype = {red, green, yellow, pending, none, crossing, waiting};
mtype traffic_mode;
mtype crosswalk_mode;
int count;
chan pedestrian_chan = [0] of {byte};

chan sigR_chan = [0] of {byte};

chan sigG_chan = [0] of {byte};

chan sigY_chan = [0] of {byte};

ltl l1 {!<> (pedestrian_chan[0] == 1) && (traffic_mode == green || traffic_mode == yellow || traffic_mode == pending)}
ltl l2 {[]<> (pedestrian_chan[0] == 1) -> crosswalk_mode == crossing }

proctype traffic_controller(chan pedestrian_in, sigR_out, sigG_out, sigY_out)

{

do
    ::if
      ::(traffic_mode == red) -> 
        count = count + 1;
        if
        ::(count >= 60) ->
            sigG_out ! 1;
            count = 0;
            traffic_mode = green;
        :: else -> skip;
        fi
      ::(traffic_mode == green) -> 
        if
        ::(count < 60) ->
            count = count + 1;
        ::(pedestrian_in == 1 & count < 60) ->
            count = count + 1;
            traffic_mode = pending;
        ::(pedestrian_in == 1 & count >= 60)
            count = 0;
            traffic_mode = yellow;
        fi
      ::(traffic_mode == pending) ->
        count = count + 1;
        if
        ::(count >= 60) ->
            sigY_out ! 1;
            count = 0;
            traffic_mode = yellow;
        ::else -> skip;
        fi  
      ::(traffic_mode == yellow) ->
        count = count + 1;
        if
        ::(count >= 5) ->
            sigR_out ! 1;
            count = 0;
            traffic_mode = red;
        :: else -> skip;
        fi
      fi
od  

}



proctype crosswalk(chan sigR_in, sigG_in, sigY_in, pedestrian_out)

{
do
    ::if
      ::(crosswalk_mode == crossing) ->
        if
        ::(sigG_in == 1) -> crosswalk_mode = none;
        fi
      ::(crosswalk_mode == none) ->
        if  
        :: (1 == 1) -> crosswalk_mode = none
        :: (1 == 1) -> 
            pedestrian_out ! 1
            crosswalk_mode = waiting
        fi
      ::(crosswalk_mode == waiting) ->
        if
        ::(sigR_in == 1) -> crosswalk_mode = crossing;
        fi
      fi
od   
}


init

{

    count = 0;

    traffic_mode = red;

    crosswalk_mode = crossing;


    atomic
    {
        run traffic_controller(pedestrian_chan, sigR_chan, sigG_chan, sigY_chan);
        run crosswalk(sigR_chan, sigG_chan, sigY_chan, pedestrian_chan);
    }

}

enter image description here

Solution

  • You are using channels incorrectly, this line in particular I wouldn't even know how to interpret it:

    :: (sigG_in == 1) ->

    1. Your channels are synchronous, which means that whenever a process sends something on one side, another process must listen on the other end of the channel in order to deliver the message. Otherwise, the process blocks until when the situation changes. Your channels are synchronous because you declared them of size 0.

    2. To read from a channel, you need to use the proper syntax:

      int some_var;
...
some_channel?some_var;
// here some_var contains value received through some_channel

    It seems to be a bit pointless to use three different channels to send different signals. What about using three different values?

    mtype = { RED, GREEN, YELLOW };
chan c = [0] of { mtype };
...
c!RED
...
// (some other process)
...
mtype var;
c?var;
// here var contains RED
...