SHARE
TWEET

Untitled

a guest Mar 26th, 2019 64 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #define N 3
  2.  
  3. mtype = { red , green }
  4. mtype sem1 = red , sem2 = red , sem3 = red ; // three semaphores
  5. bool s0 , s1 , s2 , s3 ; // four presence sensors
  6. //bool sensors[4];
  7. byte countZ0 , countZ1 , countZ2 , countZ3 ; // count the vehicles in each zone
  8. //mtype sem[3];
  9. int number;
  10. byte countZ[4];
  11. byte ghost1, ghost2,ghost3;
  12.  
  13. ltl mutual_exclusion { []((ghost1+ghost2+ghost3)<2) }
  14. //ltl ficar_verde {<>(sem1==green || sem2==green || sem3==green )}
  15. proctype Sensors () {
  16.     do
  17.     :: s0 = ( countZ[0] > 0)
  18.     :: s1 = ( countZ[1] > 0)
  19.     :: s2 = ( countZ[2] > 0)
  20.     :: s3 = ( countZ[3] > 0)
  21.     od
  22. }
  23.  
  24.  
  25. proctype RoadsideUnit () {
  26.     do
  27.     ::if
  28.     :: (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 0) -> sem3 = red; sem2 = red; sem1 = green
  29.     :: (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 0) -> sem1 = red; sem3 = red; sem2 = green
  30.     :: (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 1) -> sem2 = red; sem1 = red; sem3 = green
  31.  
  32.     :: (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 0) -> sem3 = red; sem2 = red; sem1 = green
  33.     :: (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 1) ->  sem1 = red; sem3 = red; sem2 = green
  34.     :: (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 1) ->  sem2 = red; sem1 = red; sem3 = green
  35.     :: (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 1) ->  sem3 = red; sem2 = red; sem1 = green
  36.     fi
  37.     od
  38. }
  39.  
  40. proctype Vehicles () {
  41.     do
  42.         ::if
  43.         :: (countZ[0]+countZ[1]+countZ[2]+countZ[3])<N -> select(number: 1 .. 3); countZ[number]++
  44.         :: (sem1 == green && countZ[1] > 0 )  -> countZ[1] = countZ[1] - 1; ghost1 = 1; countZ[0] = countZ[0] + 1
  45.         :: (sem2 == green && countZ[2] > 0 )  -> countZ[2] = countZ[2] - 1; ghost2 = 1; countZ[0] = countZ[0] + 1  
  46.         :: (sem3 == green && countZ[3] > 0 )  -> countZ[3] = countZ[3] - 1; ghost3 = 1; countZ[0] = countZ[0] + 1
  47.         :: (countZ[0] > 0) -> countZ[0] = countZ[0] - 1;if
  48.                                                         ::(countZ[0] == 0) -> ghost1=0; ghost2=0; ghost3=0//; sem1=red; sem2=red; sem3=red
  49.                                                         :: else -> skip
  50.                                                         fi
  51.         fi
  52.     od
  53. }
  54. init {
  55.  
  56.  
  57.     run Sensors ();
  58.     run RoadsideUnit ();
  59.     run Vehicles ();
  60. }
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top