//  Declare lookups
Boolean Lookup MergingTraffic;
Boolean Lookup LetBehind;
Boolean Lookup RollStop;

cruisecontrol:
{
  // ---------
  // Constants
  // ---------

  // Positions and thresholds
  Integer INIT_DISTANCE     = 55;
  Integer BEGIN_RAMP        = 33;
  Integer END_RAMP          = 25;
  Integer NEAR_INTERSECTION =  5;
  Integer AT_INTERSECTION   =  0;

  // time units
  Integer timestep        =  1;
  Integer SEMAPHORE_CYCLE = 28;

  // timestamps when semaphore changes color
  Integer GREEN_LIGHT     = 28;
  Integer YELLOW_LIGHT    = 12;
  Integer RED_LIGHT       =  8;

  // Discretized speed values
  Integer STOPPED         =  0;
  Integer SLOW            =  1;
  Integer MODERATE        =  2;
  Integer FAST            =  3;
  Integer DESIRED         =  2;

  // ---------
  // Variables (proper)
  // ---------
  Integer distance	  = 55;
  Integer speed	          =  1;
  Integer acceleration    =  0;
  Integer semaphore       = 28;
  Boolean cruise_enabled  = false;
  Integer cruise_speed	  =  0;

  // Should be lookups
  Boolean merging_traffic = false;
  Boolean let_behind      = false;
  Boolean roll_stop       = false;

  /*
   ********************************************************************
   *  First, setup the global variables, then execute the main program
   ********************************************************************
  */

  Sequence
    
  SetUp : 
  { 
      Concurrence

      SetMT: {
        Assignment: merging_traffic = LookupNow(cruisecontrol.MergingTraffic);
      }

      SetLB: {
        Assignment: let_behind = LookupNow(cruisecontrol.LetBehind);
      }

      SetRS: {
        Assignment: roll_stop = LookupNow(cruisecontrol.RollStop);
      }
  }

  /* 
   ********************************************************************
   *  Three concurrently executing components: car, driver, semaphore  
   ********************************************************************
  */
 
  Main : 
  {

     InvariantCondition: !(distance == AT_INTERSECTION AND 
                           speed > STOPPED);

     Concurrence

     // ==============================
     // Car movement
     // ==============================
     Car:
     {
         RepeatCondition: distance > AT_INTERSECTION AND speed > 0;
   
         Assignment: distance = distance - speed * timestep;
     } 
    
     // ==============================
     // Driver actions
     // ==============================
   
     Driver:
     {
       Sequence
   
       DriveToRamp:
       {
         StartCondition:  distance > BEGIN_RAMP;
         RepeatCondition: distance > BEGIN_RAMP;
   
         Concurrence
   
         SetDesiredCruise:
         {
           SkipCondition: !(speed == DESIRED AND cruise_enabled == false);
           Concurrence 
           EnableCruise:   { Assignment: cruise_enabled = true; }
           SetCruiseSpeed: { Assignment: cruise_speed = speed; }
           NoAcceleration: { Assignment: acceleration = 0; }
         }

         MaintainSpeed:
         {
           SkipCondition: !(speed == DESIRED AND cruise_enabled == true AND cruise_speed == DESIRED);
           Concurrence
           AtDesiredSpeed: { Assignment: speed = DESIRED; }
           ConstantSpeed:  { Assignment: acceleration = 0; }
         }

         IncreaseSpeed:
         {
           SkipCondition: !(speed < DESIRED);
           Concurrence
           IncSpeed2Cruise:   { Assignment: speed = speed + 1; }
           Accelerate2Cruise: { Assignment: acceleration = 1; }
         }

         DecreaseSpeed:
         {
           SkipCondition: !(speed > DESIRED);
           Concurrence
           DecSpeed2Cruise:   { Assignment: speed = speed - 1; }
           Decelerate2Cruise: { Assignment: acceleration = -1; }
         }
       }
   
       AvoidTraffic:
       {
         StartCondition: END_RAMP <= distance AND distance <= BEGIN_RAMP;
   
         Concurrence

         LetBehind:
         {
           SkipCondition: !(merging_traffic AND let_behind);
           Concurrence 
           IncSpeedAtRamp:   { Assignment: speed = speed + 1; }
           AccelerateAtRamp: { Assignment: acceleration = 1; }
         }

         LetAhead:
         {
           SkipCondition: !(merging_traffic AND !let_behind);
           Concurrence
           DecSpeedAtRamp:   { Assignment: speed = speed - 1; }
           DecelerateAtRamp: { Assignment: acceleration = -1; }
           DisableCruise:    { Assignment: cruise_enabled = false; }
         }

         NoTraffic:
         {
           SkipCondition: merging_traffic;
           Assignment: acceleration = 0;
         }
       }
   
       StopAtLight:
       {
         StartCondition: AT_INTERSECTION < distance AND distance < END_RAMP;
         RepeatCondition: distance > AT_INTERSECTION AND speed > 0;
   
         Concurrence

         Roll:
         { 
           SkipCondition: !(cruise_enabled AND speed > cruise_speed AND roll_stop);
           Concurrence
           RollDecSpeed:        { Assignment: speed = speed - 1; }
           RollDecelerate:      { Assignment: acceleration = -1; }
         }

         Break:
         {
           SkipCondition: !(cruise_enabled AND speed > cruise_speed AND !roll_stop);
           Concurrence
           PressBreakPedal: { Assignment: speed = speed - 1; }
           BreakDecelerate: { Assignment: acceleration = -1; }
           BreakDisengage:  { Assignment: cruise_enabled = false; }
         }

         CruiseOn:
         { 
           SkipCondition: !(cruise_enabled AND speed == cruise_speed AND acceleration < 0);
           Assignment: acceleration = 0;
         }

         BreakLate:
         {
           SkipCondition: !(cruise_enabled AND speed <= cruise_speed AND !(acceleration < 0));
           Concurrence
           PressPedalLate:  { Assignment: speed = speed - 1; }
           DecelerateLate:  { Assignment: acceleration = -1; }
           DisengageLate:   { Assignment: cruise_enabled = false; }
         }

         NoCruiseSlowdown:
         {
           SkipCondition: !(!cruise_enabled AND speed > SLOW);
           Concurrence
           NCDecSpeed:    { Assignment: speed = speed - 1; }
           NCDecelerate:  { Assignment: acceleration = -1; }
         }

         NoCruiseAdvance:
         {
           SkipCondition: !(!cruise_enabled AND speed == SLOW AND distance > NEAR_INTERSECTION);
           Assignment: acceleration = 0;
         }

         Stop:
         {
           SkipCondition: !(!cruise_enabled AND speed == SLOW AND distance <= NEAR_INTERSECTION);
           Concurrence
           SlowDecSpeed:    { Assignment: speed = speed - 1; }
           SlowDecelerate:  { Assignment: acceleration = -1; }
         }

       }
     }
   
     // ==============================
     // Semaphore actions
     // ==============================
   
     Semaphore:
     {
         RepeatCondition: semaphore > 0;
         Assignment: semaphore = semaphore - timestep;
     }
   }
}