daily pastebin goal
68%
SHARE
TWEET

Untitled

a guest Mar 25th, 2019 67 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 total_max = 100; //maximum number of vehicles that can pass through the system
  6. byte n = 10; //maximum number of vehicles simultaneously in the system
  7. byte total_counter_v = 0; //total counter of vehicles
  8.  
  9. proctype Sensors () {
  10. do
  11.     :: s0 = ( countZ0 > 0)
  12.     :: s1 = ( countZ1 > 0)
  13.     :: s2 = ( countZ2 > 0)
  14.     :: s3 = ( countZ3 > 0)
  15.     :: total_counter_v >= total_max -> break;
  16. od ;
  17. }
  18.  
  19. proctype RoadsideUnit () {
  20.     do // update sem1 , sem2 and sem3 according to s0 , s1 , s2 and s3
  21.     :: 1 == 1 ->
  22.         printf("TOTAL_MAX %d\n",total_counter_v);
  23.         printf("sem1 %e sem2 %e sem3 %e\n",sem1,sem2,sem3);
  24.         printf("s0 %d s1 %d s2 %d s3 %d\n",s0,s1,s2,s3);
  25.         printf("countZ0 %d countZ1 %d countZ2 %d countZ3 %d\n",countZ0,countZ1,countZ2,countZ3);
  26.     :: s0 -> skip;
  27.     :: !s0 && (sem1 == red && sem2 == red && sem3 == red) && (s1 || s2 || s3) -> //all sem are red
  28.         if
  29.         :: s1 && !s2 && !s3 -> sem1 = green;
  30.         :: !s1 && s2 && !s3 -> sem2 = green;
  31.         :: !s1 && !s2 && s3 -> sem3 = green;
  32.         :: s1 && s2 && !s3 -> sem1 = green;
  33.         :: s1 && !s2 && s3 -> sem1 = green;
  34.         :: !s1 && s2 && s3 -> sem2 = green;
  35.         :: else -> skip;
  36.         fi;
  37.     :: !s0 && sem1 == green && !s1  -> //sem1 is green with no cars:
  38.         sem1 = red;
  39.     :: !s0 && sem2 == green && !s2  -> //sem2 is green with no cars:
  40.         sem2 = red;
  41.     :: !s0 && sem3 == green && !s3  -> //sem3 is green with no cars:
  42.         sem3 = red;
  43.     :: total_counter_v >= total_max -> break;
  44.     od;
  45. }
  46.  
  47. proctype Vehicles () {
  48.     do // non - deterministically move vehicles through zones Z0 , Z1 , Z2 , and Z3
  49.     :: (countZ0 + countZ1 + countZ2 + countZ3) < n ->       // handle arrivals - can any car arrive?
  50.         printf("---1 soma: %d\n", (countZ0 + countZ1 + countZ2 + countZ3));
  51.         atomic{
  52.         printf("############ATOMIC#########\n");
  53.         if
  54.         :: countZ1++ ->
  55.             total_counter_v++;
  56.         :: countZ2++ ->
  57.             total_counter_v++;
  58.         :: countZ3++ ->
  59.             total_counter_v++;
  60.         fi;
  61.         }
  62.     :: (countZ0 + countZ1 + countZ2 + countZ3) > 0 ->
  63.         printf("---2 soma: %d\n", (countZ0 + countZ1 + countZ2 + countZ3));
  64.  
  65.         if //handle zone departures
  66.         :: s0 ->
  67.             printf("---teste s0 CountZ0 %d\n", countZ0);
  68.             atomic{countZ0--;}
  69.         :: s1 ->
  70.             printf("---teste s1 sem1 %e\n",sem1);
  71.             if
  72.             :: sem1 == green ->
  73.                 atomic{countZ1--; countZ0++;}
  74.             fi;
  75.         :: s2 ->
  76.             printf("---teste s2 sem2 %e\n",sem2);
  77.             if
  78.             :: sem2 == green ->
  79.                 atomic{countZ2--; countZ0++;}
  80.             fi;
  81.         :: s3 ->
  82.             printf("---teste s3 sem3 %e\n",sem3);
  83.             if
  84.             :: sem3 == green ->
  85.                 atomic{countZ3--; countZ0++;}
  86.             fi;
  87.         fi;
  88.     :: total_counter_v >= total_max -> break;
  89.     :: else -> printf("TESTE ELSE\n");
  90.     od ;
  91. }
  92.  
  93. init {
  94.     run Sensors();
  95.     run RoadsideUnit();
  96.     run Vehicles();
  97. }
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