// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This case study is due to Mario Trapp and is described in his PhD thesis.  //
// The program models the control of a light control in a building.           //
// ************************************************************************** //

import LightControl.*;

macro LAMPBRIGHTNESS_dimmable    = 2;
macro LAMPBRIGHTNESS_switchable  = 1;
macro LAMPBRIGHTNESS_unavailable = 0;

macro LAMP_Dimming   = 2;
macro LAMP_Switching = 1;
macro LAMP_Off       = 0;

macro LIGHTCONTROL_DimmerControl            = 3;
macro LIGHTCONTROL_IntelligentSwitchControl = 2;
macro LIGHTCONTROL_SwitchControl            = 1;
macro LIGHTCONTROL_Off                      = 0;

macro OCCUPANCY_OccupancyDetection   = 4;
macro OCCUPANCY_TransponderDetection = 3;
macro OCCUPANCY_MotionDetection      = 2;
macro OCCUPANCY_EntryExitDetection   = 1;
macro OCCUPANCY_Off                  = 0;

macro ALARMSYSTEM_AlarmLight = 2;
macro ALARMSYSTEM_Alarm      = 1;
macro ALARMSYSTEM_Off        = 0;

// ================================================================================
// Main Module
// ================================================================================

module LightControlSystem(
   bool ?hasDesiredIlluminance,
   bool ?hasTransponderID,
   bool ?hasEntryExit,
   bool ?hasCurrentIlluminance,
   bool ?hasMotionDetection,
   bool ?hasCameraImage,
   bool ?AlarmNotify,
   bool ?lightOnOff,
   bool ?hasDimmerValue,
   event nat{3} !AlarmCfg,
   event nat{4} !LightControlCfg,
   event nat{5} OccupancyMode,
   event nat{5} !OccupancyCfg,
   event nat{3} lampBrightness,
   event nat{3} !LampCfg) {
      AlarmSystem(AlarmNotify,OccupancyMode,lampBrightness,AlarmCfg);
   || LightControl(hasDesiredIlluminance,hasCurrentIlluminance,OccupancyMode,lampBrightness,LightControlCfg);
   || Occupancy(hasMotionDetection,hasCameraImage,hasTransponderID,hasEntryExit,OccupancyMode,OccupancyCfg);
   || Lamp(hasDimmerValue,lightOnOff,lampBrightness,LampCfg);
}

// ================================================================================
// Specifications
// ================================================================================

satisfies {
   // -----------------------------------------------------------------------------
   // The following specifications state that the services do not get caught in a
   // state where they are switched off.
   // -----------------------------------------------------------------------------
   ALARMSYSTEM_alive : assert
       A G ((AlarmCfg==ALARMSYSTEM_Off)
            -> E F (AlarmCfg!=ALARMSYSTEM_Off));
   LIGHTCONTROL_alive : assert
       A G ((LightControlCfg==LIGHTCONTROL_Off)
            -> E F (LightControlCfg!=LIGHTCONTROL_Off));
   OCCUPANCY_alive : assert
       A G ((OccupancyCfg==OCCUPANCY_Off)
            -> E F (OccupancyCfg!=OCCUPANCY_Off));
   LAMP_alive : assert
       A G ((LampCfg==LAMP_Off)
            -> E F (LampCfg!=LAMP_Off));
   // -----------------------------------------------------------------------------
   // The next specifications are stronger and assert that every service can reach
   // all configurations all the time. Hence, there are no deadlocks and no
   // configuration is unreachable.
   // -----------------------------------------------------------------------------
   ALARMSYSTEM_alive2 : assert
       A G ((E F (AlarmCfg==ALARMSYSTEM_AlarmLight)) &
            (E F (AlarmCfg==ALARMSYSTEM_Alarm)) &
            (E F (AlarmCfg==ALARMSYSTEM_Off)) );
   LIGHTCONTROL_alive2 : assert
       A G ((E F (LightControlCfg==LIGHTCONTROL_DimmerControl)) &
            (E F (LightControlCfg==LIGHTCONTROL_IntelligentSwitchControl)) &
            (E F (LightControlCfg==LIGHTCONTROL_SwitchControl))  &
            (E F (LightControlCfg==LIGHTCONTROL_Off)) );
   OCCUPANCY_alive2 : assert
       A G ((E F (OccupancyCfg==OCCUPANCY_OccupancyDetection)) &
            (E F (OccupancyCfg==OCCUPANCY_TransponderDetection)) &
            (E F (OccupancyCfg==OCCUPANCY_MotionDetection))  &
            (E F (OccupancyCfg==OCCUPANCY_EntryExitDetection))   &
            (E F (OccupancyCfg==OCCUPANCY_Off)) );
   LAMP_alive2 : assert
       A G ((E F (LampCfg==LAMP_Dimming)) &
            (E F (LampCfg==LAMP_Switching)) &
            (E F (LampCfg==LAMP_Off)) );
   // -----------------------------------------------------------------------------
   // Conversely, each service is always in one of the defined configurations.
   // Note that unused values of the bitvectors could in principle occur, which
   // would indicate an erroneous behaviour of the system.
   // -----------------------------------------------------------------------------
   ALARMSYSTEM_reach : assert
       A G ((AlarmCfg==ALARMSYSTEM_AlarmLight) |
            (AlarmCfg==ALARMSYSTEM_Alarm) |
            (AlarmCfg==ALARMSYSTEM_Off) );
   LIGHTCONTROL_reach : assert
       A G ((LightControlCfg==LIGHTCONTROL_DimmerControl) |
            (LightControlCfg==LIGHTCONTROL_IntelligentSwitchControl) |
            (LightControlCfg==LIGHTCONTROL_SwitchControl)  |
            (LightControlCfg==LIGHTCONTROL_Off) );
   OCCUPANCY_reach : assert
       A G ((OccupancyCfg==OCCUPANCY_OccupancyDetection) |
            (OccupancyCfg==OCCUPANCY_TransponderDetection) |
            (OccupancyCfg==OCCUPANCY_MotionDetection)  |
            (OccupancyCfg==OCCUPANCY_EntryExitDetection)   |
            (OccupancyCfg==OCCUPANCY_Off) );
   LAMP_reach : assert
       A G ((LampCfg==LAMP_Dimming) |
            (LampCfg==LAMP_Switching) |
            (LampCfg==LAMP_Off) );
   OccupancyMode_reach : assert
       A G ((OccupancyMode==OCCUPANCY_OccupancyDetection) |
            (OccupancyMode==OCCUPANCY_TransponderDetection) |
            (OccupancyMode==OCCUPANCY_MotionDetection)  |
            (OccupancyMode==OCCUPANCY_EntryExitDetection)   |
            (OccupancyMode==OCCUPANCY_Off) );
   lampBrightness_reach : assert
       A G ((lampBrightness==LAMPBRIGHTNESS_dimmable) |
            (lampBrightness==LAMPBRIGHTNESS_switchable) |
            (lampBrightness==LAMPBRIGHTNESS_unavailable) );
   // -----------------------------------------------------------------------------
   // Initially, all configurations are in their "Off" mode.
   // -----------------------------------------------------------------------------
   InitialConfigurations : assert
        (AlarmCfg==ALARMSYSTEM_Off) &
        (LightControlCfg==LIGHTCONTROL_Off) &
        (OccupancyCfg==OCCUPANCY_Off) &
        (OccupancyMode==OCCUPANCY_Off) &
        (LampCfg==LAMP_Off) &
        (lampBrightness==LAMPBRIGHTNESS_unavailable);
   // -----------------------------------------------------------------------------
   // At time step 1, we can reach the following configurations.
   // These are 2*1*5*1*3*1=30 configurations.
   // -----------------------------------------------------------------------------
   Time1Configurations : assert
        A X (((AlarmCfg==ALARMSYSTEM_Off)
             |(AlarmCfg==ALARMSYSTEM_Alarm)) &
             (LightControlCfg==LIGHTCONTROL_Off) &
             ((OccupancyCfg==OCCUPANCY_OccupancyDetection)
             |(OccupancyCfg==OCCUPANCY_TransponderDetection)
             |(OccupancyCfg==OCCUPANCY_MotionDetection)
             |(OccupancyCfg==OCCUPANCY_EntryExitDetection)
             |(OccupancyCfg==OCCUPANCY_Off) ) &
             (OccupancyMode==OCCUPANCY_Off) &
             ((LampCfg==LAMP_Dimming)
             |(LampCfg==LAMP_Switching)
             |(LampCfg==LAMP_Off) ) &
             (lampBrightness==LAMPBRIGHTNESS_unavailable)
            );
   // -----------------------------------------------------------------------------
   // To reason about the reachable configurations, we verify the following
   // dependencies: "OccupancyCfg_OccupancyMode" states that "OccupancyMode" is
   // determined by the previous value of "OccupancyCfg".
   // -----------------------------------------------------------------------------
   OccupancyCfg_OccupancyMode : assert
        A G (((OccupancyCfg==OCCUPANCY_OccupancyDetection)
              -> A X (OccupancyMode==OCCUPANCY_OccupancyDetection))
            &((OccupancyCfg==OCCUPANCY_TransponderDetection)
              -> A X (OccupancyMode==OCCUPANCY_TransponderDetection))
            &((OccupancyCfg==OCCUPANCY_MotionDetection)
              -> A X (OccupancyMode==OCCUPANCY_MotionDetection))
            &((OccupancyCfg==OCCUPANCY_EntryExitDetection)
              -> A X (OccupancyMode==OCCUPANCY_EntryExitDetection))
            &((OccupancyCfg==OCCUPANCY_Off)
              -> A X (OccupancyMode==OCCUPANCY_Off)) );
   LampCfg_lampBrightness : assert
        A G (((LampCfg==LAMP_Dimming)
              -> A X (lampBrightness==LAMPBRIGHTNESS_dimmable))
            &((LampCfg==LAMP_Switching)
              -> A X (lampBrightness==LAMPBRIGHTNESS_switchable))
            &((LampCfg==LAMP_Off)
              -> A X (lampBrightness==LAMPBRIGHTNESS_unavailable)) );
   // -----------------------------------------------------------------------------
   // If the camera is not available, but the transponder works, the OCCUPANCY
   // service will be in mode "TransponderDetection".
   // -----------------------------------------------------------------------------
   Lemma : assert
       A X
         A G (!hasCameraImage & hasTransponderID
             -> (OccupancyCfg==OCCUPANCY_TransponderDetection));
}