#define N 3

mtype = { red , green }
mtype sem1 = red , sem2 = red , sem3 = red ; // three semaphores
bool s0 , s1 , s2 , s3 ; // four presence sensors
//bool sensors[4];
byte countZ0 , countZ1 , countZ2 , countZ3 ; // count the vehicles in each zone
//mtype sem[3];
int number;
byte countZ[4];
byte ghost1, ghost2,ghost3;

ltl mutual_exclusion { []((ghost1+ghost2+ghost3)<2) }
//ltl ficar_verde {<>(sem1==green || sem2==green || sem3==green )}
proctype Sensors () {
    do
    :: s0 = ( countZ[0] > 0)
    :: s1 = ( countZ[1] > 0)
    :: s2 = ( countZ[2] > 0)
    :: s3 = ( countZ[3] > 0)
    od
}


proctype RoadsideUnit () {
    do
    ::if
    :: (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 0) -> sem3 = red; sem2 = red; sem1 = green
    :: (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 0) -> sem1 = red; sem3 = red; sem2 = green
    :: (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 1) -> sem2 = red; sem1 = red; sem3 = green

    :: (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 0) -> sem3 = red; sem2 = red; sem1 = green
    :: (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 1) ->  sem1 = red; sem3 = red; sem2 = green
    :: (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 1) ->  sem2 = red; sem1 = red; sem3 = green
    :: (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 1) ->  sem3 = red; sem2 = red; sem1 = green
    fi
    od
}

proctype Vehicles () {
    do
        ::if
        :: (countZ[0]+countZ[1]+countZ[2]+countZ[3])<N -> select(number: 1 .. 3); countZ[number]++
        :: (sem1 == green && countZ[1] > 0 )  -> countZ[1] = countZ[1] - 1; ghost1 = 1; countZ[0] = countZ[0] + 1
        :: (sem2 == green && countZ[2] > 0 )  -> countZ[2] = countZ[2] - 1; ghost2 = 1; countZ[0] = countZ[0] + 1
        :: (sem3 == green && countZ[3] > 0 )  -> countZ[3] = countZ[3] - 1; ghost3 = 1; countZ[0] = countZ[0] + 1
        :: (countZ[0] > 0) -> countZ[0] = countZ[0] - 1;if
                                                        ::(countZ[0] == 0) -> ghost1=0; ghost2=0; ghost3=0//; sem1=red; sem2=red; sem3=red
                                                        :: else -> skip
                                                        fi
        fi
    od
}
init {


    run Sensors ();
    run RoadsideUnit ();
    run Vehicles ();
}