// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following implements the controller for a pump used in a mine. The     //
// example is due to Burns&Wellings' book "Hrt-Hood: A Structured Design      //
// Method for Hard Real-Time Ada Systems: Structured Design Method of Hard    //
// Real-Time Ada Systems" (Real-Time Safety Critical Systems , Vol 3)         //
// For some explanations, see also the pdf-file in this directory, which      //
// is an excerpt of [ScKr97a]: K. Schneider and T. Kropf, "The C@S System:    //
// Combining Proof Strategies for System Verification", Springer.             //
// ************************************************************************** //


import MinePump.*;

module MinePumpController(event
      ?COCritical,                      // CO level is critical
      ?MethaneLVLow,?MethaneLVHigh,     // Methane level is high or low
      ?AirFlowCritical,                 // air flow is critical
      ?LW,?HW,                          // water level is low or high
      ?SVStopPump,?SVStartPump,         // supervisor switches pump on or off
      ?OPStopPump,?OPStartPump,         // operator switches pump on or off
      !Alarm,
      !SwitchOffPump,!SwitchOnPump,
      StartPump,StopPump,
      !WaterLVLow,WaterLVMid,WaterLVHigh,
      MethaneCritical,!MethaneUnCritical,
      !PumpOff,!PumpOn,
      AlertOP) {
     PumpController(StopPump, StartPump,SwitchOffPump,SwitchOnPump,PumpOff,PumpOn);
  || Operator(SVStartPump,SVStopPump,OPStartPump,OPStopPump,
              MethaneCritical,WaterLVMid,AlertOP,StartPump,StopPump,Alarm);
  || COAirFlowMonitor(COCritical,AirFlowCritical,AlertOP);
  || WaterMonitor(LW,HW,MethaneCritical,AlertOP,
                  StopPump,StartPump,WaterLVMid,WaterLVLow,WaterLVHigh);
  || MethaneMonitor(MethaneLVHigh,MethaneLVLow,WaterLVHigh,AlertOP,
                    StartPump,StopPump,MethaneCritical,MethaneUnCritical);
} satisfies {
  s1  : assert A G (MethaneCritical -> PumpOff);
  s2  : assert A G (SwitchOnPump & MethaneCritical -> MethaneLVLow);
  s31 : assert A G (WaterLVHigh & !MethaneCritical -> StartPump);
  s32 : assert A G (WaterLVHigh & !MethaneCritical & !SVStopPump &
                    (MethaneUnCritical -> !MethaneLVHigh) & PumpOff -> SwitchOnPump);
  s4  : assert A G (WaterLVHigh & MethaneCritical -> Alarm);
  s5  : assert A G X (COCritical | AirFlowCritical -> Alarm);
  s6  : assert A G (MethaneUnCritical & MethaneLVHigh & PumpOn -> SwitchOffPump);
}