daily pastebin goal
44%
SHARE
TWEET

badabadabada

a guest Mar 24th, 2019 52 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. mtype = { red , green }
  2. mtype sem1 = red , sem2 = red , sem3 = red ; // three semaphores
  3. bool s0 , s1 , s2 , s3 ; // four presence sensors
  4. byte countZ0 , countZ1 , countZ2 , countZ3 ; // count the vehicles in each zone
  5. byte n = 5; //maximum number of vehicles
  6. byte total_v = 0; //counter of vehicles
  7.  
  8. proctype Sensors () {
  9. do
  10.     :: s0 = ( countZ0 > 0)
  11.     :: s1 = ( countZ1 > 0)
  12.     :: s2 = ( countZ2 > 0)
  13.     :: s3 = ( countZ3 > 0)
  14. od ;
  15. }
  16.  
  17. proctype RoadsideUnit () {
  18.     do // update sem1 , sem2 and sem3 according to s0 , s1 , s2 and s3
  19.     :: s0 -> skip;
  20.     :: !s0 && (sem1 == red && sem2 == red && sem3 == red) && (s1 || s2 || s3) -> //all sem are red
  21.         if
  22.         :: s1 && !s2 && !s3 -> sem1 = green;
  23.         :: !s1 && s2 && !s3 -> sem2 = green;
  24.         :: !s1 && !s2 && s3 -> sem3 = green;
  25.         :: s1 && s2 && !s3 -> sem1 = green;
  26.         :: s1 && !s2 && s3 -> sem1 = green;
  27.         :: !s1 && s2 && s3 -> sem2 = green;
  28.         :: else -> skip;
  29.         fi;
  30.     :: !s0 && sem1 == green && !s1  -> //sem1 is green with no cars:
  31.         sem1 = red;
  32.     :: !s0 && sem2 == green && !s2  -> //sem2 is green with no cars:
  33.         sem2 = red;
  34.     :: !s0 && sem3 == green && !s3  -> //sem3 is green with no cars:
  35.         sem3 = red;
  36.     :: else -> skip;
  37.     od;
  38. }
  39.  
  40. proctype Vehicles () {
  41.     byte temp_v, temp_dif, temp_zone, do_counter;
  42.     byte max_v = 3; //maximum number of vehicles that can arrive/depart at a time
  43.     do // non - deterministically move vehicles through zones Z0 , Z1 , Z2 , and Z3
  44.     :: total_v < n ->       // handle arrivals
  45.         temp_zone = 0;
  46.         temp_dif = n - total_v;
  47.         if
  48.         :: max_v < temp_dif ->
  49.             select(temp_v : 0..max_v); // how many vehicles arrive
  50.         :: else ->
  51.             select(temp_v : 0..temp_dif); // how many vehicles arrive
  52.         fi;
  53.         total_v = total_v + temp_v;
  54.  
  55.         do_counter = 0;
  56.         do
  57.         :: temp_v > 0 ->
  58.             select(temp_zone : 0..temp_v);  // temp_zone saves the amount of cars that will arrive in a zone
  59.             if
  60.             :: do_counter == 0 ->
  61.                 countZ1 = countZ1+temp_zone;
  62.             :: do_counter == 1 ->
  63.                 countZ2 = countZ2+temp_zone;
  64.             :: do_counter == 2 ->
  65.                 countZ3 = countZ3+temp_zone;
  66.             :: else -> skip;
  67.             fi;
  68.  
  69.             temp_v = temp_v - temp_zone;
  70.             do_counter++;
  71.         :: else -> skip;
  72.         od;
  73.     //handle zone departures
  74.     :: s0 ->
  75.         countZ0 = countZ0 - max_v;
  76.         if
  77.         :: countZ0 < 0 ->
  78.             countZ0 = 0;
  79.         fi;
  80.     :: s1 ->
  81.         if
  82.         :: sem1 == green && countZ1 > max_v ->
  83.             countZ1 = countZ1 - max_v;
  84.             countZ0 = countZ0 + max_v;
  85.         :: sem1 == green && countZ1 <= max_v ->
  86.             countZ0 = countZ0 + countZ1;
  87.             countZ1 = 0;
  88.         :: else -> skip;
  89.         fi;
  90.     :: s2 ->
  91.         if
  92.         :: sem2 == green && countZ2 > max_v ->
  93.             countZ2 = countZ2 - max_v;
  94.             countZ0 = countZ0 + max_v;
  95.         :: sem2 == green && countZ2 <= max_v ->
  96.             countZ0 = countZ0 + countZ1;
  97.             countZ2 = 0;
  98.         :: else -> skip;
  99.         fi;
  100.     :: s3 ->
  101.         if
  102.         :: sem3 == green && countZ3 > max_v ->
  103.             countZ3 = countZ3 - max_v;
  104.             countZ0 = countZ0 + max_v;
  105.         :: sem3 == green && countZ3 <= max_v ->
  106.             countZ0 = countZ0 + countZ3;
  107.             countZ3 = 0;
  108.         :: else -> skip;
  109.         fi;
  110.     :: else ->
  111.         temp_v = 0;
  112.     od ;
  113. }
  114.  
  115. init {
  116.     run Sensors ();
  117.     run RoadsideUnit ();
  118.     run Vehicles ();
  119. }
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