#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
    :: sensors[0] = ( countZ[0] > 0)
    :: sensors[1] = ( countZ[1] > 0)
    :: sensors[2] = ( countZ[2] > 0)
    :: sensors[3] = ( countZ[3] > 0)
    od
}


proctype RoadsideUnit () {
    do
    ::if
    :: (sensors[0] == 0 && sensors[1] == 1 && sensors[2] == 0 && sensors[3] == 0) -> sem3 = red; sem2 = red;  sem1 = green
    :: (sensors[0] == 0 && sensors[1] == 0 && sensors[2] == 1 && sensors[3] == 0) -> sem1 = red; sem3 = red; sem2 = green
    :: (sensors[0] == 0 && sensors[1] == 0 && sensors[2] == 0 && sensors[3] == 1) ->  sem2 = red; sem1 = red; sem3 = green

    :: (sensors[0] == 0 && sensors[1] == 1 && sensors[2] == 1 && sensors[3] == 0) -> sem3 = red; sem2 = red; sem1 = green
    :: (sensors[0] == 0 && sensors[1] == 0 && sensors[2] == 1 && sensors[3] == 1) ->  sem1 = red; sem3 = red; sem2 = green
    :: (sensors[0] == 0 && sensors[1] == 1 && sensors[2] == 0 && sensors[3] == 1) ->  sem2 = red; sem1 = red; sem3 = green
    :: (sensors[0] == 0 && sensors[1] == 1 && sensors[2] == 1 && sensors[3] == 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 //Rever
    :: (countZ[0] == 0) -> ghost1=0; ghost2=0; ghost3=0 // ; sem1=red; sem2=red; sem3=red
    ;
    fi
    od
}
init {


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