// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// An island is connected via a tunnel with the mainland. Inside the tunnel is//
// a single lane so that cars can either travel from the mainland to the      //
// island or vice versa, which is signaled by traffic lights on both ends of  //
// the tunnel. The number of cars that may be on the island is limited.       //
// You may view the problem also as the control to a parking lot where the    //
// entrance does only have one lane.                                          //
// ************************************************************************** //

import IslandTrafficControl.*;

macro MaxCars = 5;

module IslandTrafficControl(
   event
      ?il_want_enter, ?il_leave,  // detected by sensors when cars enter/leave the island
      ?ml_want_enter, ?ml_leave,  // detected by sensors when cars enter/leave the mainland
      !il_red_light, !il_green_light, // signals controlling traffic lights on island
      !ml_red_light, !ml_green_light, // signals controlling traffic lights on mainland
      il_grant,il_release,il_use,il_req,        // interface for island controller
      ml_grant,ml_release,ml_use,ml_req,        // interface for mainland controller
      // counting cars in the tunnel and on the island
      tc_inc,tc_dec,ic_inc,ic_dec,
      nat{MaxCars+1} tc,ic) {
 
     
     il_TLC: TrafficLightController
        (il_grant, il_release, (il_want_enter&ic!=0), (il_leave&tc!=0),
         false,
         il_green_light, il_red_light, il_use, il_req,
         tc_inc, tc_dec, ic_dec);
  ||
     tac: TunnelAccessControl
        (il_use, il_req, ml_use, ml_req,
         il_grant, il_release, ml_grant, ml_release,
         tc, ic);
  || ml_TLC: TrafficLightController
        (ml_grant, ml_release, ml_want_enter, (ml_leave&tc!=0),
         (ic==MaxCars),
         ml_green_light, ml_red_light, ml_use, ml_req,
         tc_inc, tc_dec, ic_inc);
  || tcounter: Counter(tc_inc,tc_dec,tc);
  || icounter: Counter(ic_inc,ic_dec,ic);
  //|| always {
  //      assume (ic==0 -> !il_want_enter);
  //      assume (tc==0 -> !il_leave & !ml_leave);
  //Make a workaround since behavior of environment matters (Added to the above parameters)
  //}
} satisfies {
  // -----------------------------------------------------------
  // It is never the case that both sides of the tunnel
  // have green traffic lights.
  // -----------------------------------------------------------
  TrafficLightsSafe : assert
    A G ((il_green_light -> !ml_green_light) &
         (ml_green_light -> !il_green_light) );
  // -----------------------------------------------------------
  // On each side of the tunnel, the traffic light
  // always either shows a green or a red light.
  // -----------------------------------------------------------
  TrafficLightsMutex : assert
    A G ((il_green_light <-> !il_red_light) &
         (ml_green_light <-> !ml_red_light) );
  // -----------------------------------------------------------
  // Summarizing the above two properties shows that there
  // three states of the traffic lights.
  // -----------------------------------------------------------
  TrafficLightsStates : assert
    A G (  il_green_light & !il_red_light & !ml_green_light & ml_red_light
            | !il_green_light &  il_red_light &  ml_green_light & !ml_red_light
            | !il_green_light &  il_red_light & !ml_green_light &  ml_red_light);
  // -----------------------------------------------------------
  // The number of cars on the island is always less or equal
  // to the constant MaxCars. However, this only holds if we
  // assume that no car wants to enter the tunnel from the island
  // when thera are no cars on the island. Otherwise, the ic
  // counter is decremented which may yield a number larger than
  // MaxCars (depending on that constant and the bitwidths).
  // -----------------------------------------------------------
  IslandNotOvercrowded : assert
    A (G ((ic==0) -> !il_want_enter)
       ->
       G (ic <= MaxCars));
  StopOvercrowding : assert
    A G (ic==MaxCars -> X ml_red_light);
  // -----------------------------------------------------------
  // When a traffic light changes from red to green, then
  // it is always the case that the tunnel is empty. Note
  // that changes from green to red can happen while there
  // are still cars in the tunnel (which is no problem).
  // -----------------------------------------------------------
  StartGreenLightOnlyWhenTunnelIsEmpty : assert
        A (G ((il_red_light & X il_green_light |
           ml_red_light & X ml_green_light )
          ->(tc==0)) );
  // -----------------------------------------------------------
  // The counters for counting the number of cars in the tunnel
  // and on the island are always less than or equal to the
  // constant MaxCars. Moreover, there is never an underflow
  // i.e., there is no decrement signal when the counter is zero.
  // -----------------------------------------------------------
  NoTunnelCounterUnderflow : assert
    A (G (tc==0 -> !il_leave & !ml_leave)
       ->
       G (tc_dec -> tc!=0)
      );
  NoTunnelCounterOverflow : assert
    A (G ((ic==0 -> !il_want_enter) &
          (tc==0 -> !il_leave & !ml_leave)
             )
       ->
       G (tc==MaxCars -> !tc_inc)
      );
  NoIslandCounterUnderflow : assert
    A (G (ic==0 -> !il_want_enter)
       ->
       G (ic_dec -> ic!=0)
      );
  NoIslandCounterOverflow : assert
    A (G ((ic==0 -> !il_want_enter) &
          (tc==0 -> !il_leave & !ml_leave))
       ->
       G (ic==MaxCars -> !ic_inc)
      );
  // -----------------------------------------------------------
  // If the mainland has green light, the number of cars on the
  // island may not decrease and each time the tunnel counter is
  // incremented, we also increase the island counter. In this
  // case, the cars in the tunnel are already counted as being
  // already on the island. If, on the other hand, the island
  // has green light, then the number of cars on the island may
  // not decrease and each time the tunnel counter is incremented,
  // we decrease the island counter (since a car left the island).
  // In this case, the cars in the tunnel are already counted as
  // being already on the mainland. Hence, depending on the
  // lights, the tunnel is either seen to belong to the mainland
  // or to the island.
  // -----------------------------------------------------------
  TunnelCarsBelongToMainlandOrIsland : assert
    A G ((ml_green_light -> !ic_dec & (tc_inc<->ic_inc)) &
         (il_green_light -> !ic_inc & (tc_inc<->ic_dec)) 
        );
  // -----------------------------------------------------------
  // Finally, we have to check the operability of the controllers,
  // i.e. the cars will eventually have green lights. However,
  // this depends on many assumptions as can be seen below.
  // The first assumption prevents that cars are produced in the
  // tunnel. The second assumption demands that cars do not stay
  // in the tunnel forever. The third assumption demands that there 
  // will be eventually cars wanting to the island. Finally, the 
  // fourth assumption demands that the cars do not stop on the 
  // sensors. For the fairness of the mainland controller, we 
  // furthermore have to demand that the number of cars on the 
  // island is not always MaxCars (otherwise the maximal number 
  // of cars could drive to the island and could stay there forever, 
  // which would forever produce a red light on the mainland). 
  // Moreover, we have to forbid that cars are produced on the 
  // island, i.e., that there are requests from the island without 
  // cars being there.
  // -----------------------------------------------------------
  IL_Fairness : assert
    A (G (((tc==0) -> !il_leave & !ml_leave) &
          ((tc!=0) & il_red_light & ml_red_light -> F (tc==0)) &
          (!ml_want_enter -> F ml_want_enter) &
          (il_leave -> F !il_leave)
         )
       ->
       !F G (il_want_enter & il_red_light)
      );
  ML_Fairness : assert
    A (G ((tc==0 -> !il_leave & !ml_leave) &
          (ic==0 -> !il_want_enter) &
          (tc!=0 & il_red_light & ml_red_light -> F (tc==0)) &
          (ml_leave -> F !ml_leave) &
          (ic==MaxCars -> F(ic!=MaxCars))
         )
       ->
       !F G (ml_want_enter & ml_red_light)
      );
}