% DRT example from Lawford, Pantelic, and Zhang paper
% Fundamenta Informaticae, 70, pages 75-110, 2006.
%
% Dense time model based on timeout automata
%
drt_real_time: CONTEXT =
BEGIN

  TIME: TYPE = REAL;
  CTRL_STATE: TYPE = { a, c, e };
  READING: TYPE = { high, low };
  RELAY: TYPE = { close, open };


  %--------------------------------------------------------
  % Event buffer: for signaling open/close relay events
  % - event is open/close
  % - delivery is time when the event is scheduled to be
  %   received by the reactor
  % - active: true if there's actually an event
  %--------------------------------------------------------
  event_buffer: TYPE = [# event: RELAY, delivery: TIME, active: BOOLEAN #];

  open_event?(e: event_buffer): BOOLEAN = e.active AND e.event = open;

  close_event?(e: event_buffer): BOOLEAN = e.active AND e.event = close;

  consume_event(e: event_buffer): event_buffer = e WITH .active := FALSE;

  % null event: only active flag matters
  null_event: event_buffer = (# event := open, delivery :=  0, active := false #);

  open_relay(t: TIME): event_buffer = (# event := open, delivery := t, active := true #);

  close_relay(t: TIME): event_buffer = (# event := close, delivery := t, active := true #);


  %
  % Controller:
  % Loop:
  %   wait until pressure = high and power = high
  %        (sample every 0.1 seconds)
  %   wait 3 seconds
  %   if power = high then
  %     open relay
  %     wait 2 seconds
  %     if power = low then close relay
  %   end
  % endloop
  %
  SAMPLING_PERIOD: TIME = 1;

  controller: MODULE =
    BEGIN
      INPUT time: TIME
      OUTPUT timeout: TIME

      INPUT pressure, power: READING
      LOCAL ctrl_state: CTRL_STATE

      GLOBAL ev: event_buffer
      

    INITIALIZATION
      timeout = time + SAMPLING_PERIOD;
      ctrl_state = a;
      ev = null_event

    TRANSITION    
      [ ctrl_state = a AND time = timeout AND power = high AND pressure = high -->
          ctrl_state' = c;
          timeout' = time + 30

     [] ctrl_state = a AND time = timeout AND (power = low OR pressure = low) -->
          timeout' = time + SAMPLING_PERIOD

     [] ctrl_state = c AND time = timeout AND power = low -->
          ctrl_state' = a;
          timeout' = time + SAMPLING_PERIOD

     [] ctrl_state = c AND time = timeout AND power = high -->
          ctrl_state' = e;
          ev' = open_relay(time);
          timeout' = time + 20

     [] ctrl_state = e AND time = timeout -->
          ctrl_state' = a;
          ev' = close_relay(time);
          timeout' = time + SAMPLING_PERIOD
     ]
    END;


  %
  % A simple model of the controlled reactor
  % - cool is the normal state.
  % - from cool, the system can start a short "temporary overheating" 
  %   (modeled as state warm, returns to cool within at most 2.5 s)
  % - from cool, the system can also transition to "severe overheating"
  %   (modeled as state hot)
  % - from hot, if nothing is done, the system goes into "meltdown" after
  %   4.5 to 6.0 s
  % - if the relay opens before that, the system starts cooling 
  % - if the relay stays open for long enough (1.5 s), the system returns to cool
  %   in 4 s otherwise if goes to meltdown
  %
  REACTOR_STATE: TYPE = { cool, warm, hot, cooling, meltdown };
  
  reactor: MODULE =
    BEGIN
      INPUT time: TIME
      OUTPUT timeout: TIME
      OUTPUT pressure, power: READING
      LOCAL state: REACTOR_STATE
      GLOBAL ev: event_buffer

    DEFINITION
      pressure = IF state = cool THEN low ELSE high ENDIF;
      power = IF state = cool THEN low ELSE high ENDIF

    INITIALIZATION
      state = cool;
      timeout IN { t: TIME | time < t }

    TRANSITION
      [ state = cool AND time = timeout -->
          state' = warm;
          timeout' IN { t: TIME | time + 10 <= t AND t <= time + 25 }

     [] state = cool AND time = timeout -->
          state' = hot;
          timeout' IN { t: TIME | time + 45 <= t AND t <= time + 60 }

     [] state = warm AND time = timeout -->
          state' = cool;
          timeout' IN { t: TIME | time + 20 <= t }

     [] state = hot AND time = timeout -->
          state' = meltdown

     [] state = hot AND open_event?(ev) AND ev.delivery = time -->
          state' = cooling;
          timeout' = time + 40;
          ev' = null_event

     [] state /= hot AND open_event?(ev) AND ev.delivery = time -->
          ev' =  null_event

     [] state = cooling AND close_event?(ev) AND ev.delivery = time -->
          state' = IF timeout - time >= 25 THEN meltdown ELSE cooling ENDIF;
          ev' = null_event

     [] state /= cooling AND close_event?(ev) AND ev.delivery = time -->
          ev' = null_event

     [] state = cooling AND time = timeout -->
          state' = cool;
          timeout' IN { t: TIME | time + 20 <= t };
 
     [] state = meltdown -->

      ]
    END;


  %
  % Clock: advances time to the next discrete transition
  % - if there is no event in the event buffer, then 
  %   time can advance if time < controller timeout 
  %                    and time < reactor timeout
  %   in this case, time advances to
  %      min(controller timeout, reactor timeout)
  % 
  % - if there is an event in the buffer, then time advance
  %   if time < min(controller timeout, reactor timeout, event delivery)
  %   and it must be updated to this min.
  %
  % Specification trick: to avoid nested if-then-else that 
  % can be expensive for ICS (less so for yices), we use a pseudo
  % non-deterministic definition (is_min ...). 
  %

  min(t1: TIME, t2: TIME): TIME = IF t1 < t2 THEN t1 ELSE t2 ENDIF;

  is_min(t: TIME, t1: TIME, t2: TIME, t3: TIME): BOOLEAN = 
     t <= t1 AND t <= t2 AND t <= t3 AND (t = t1 OR t = t2 OR t = t3);

  clock: MODULE =
    BEGIN
      INPUT ctrl_timeout, reactor_timeout: TIME
      INPUT ev: event_buffer
      OUTPUT time: TIME
    INITIALIZATION
      time = 0
    TRANSITION
     [ time < ctrl_timeout AND time < reactor_timeout AND NOT ev.active -->
         time' = min(ctrl_timeout, reactor_timeout)

    [] time < ctrl_timeout AND time < reactor_timeout AND ev.active AND time < ev.delivery -->
         time' IN { t: TIME | is_min(t, ctrl_timeout, reactor_timeout, ev.delivery) }
     ]
    END;  


   %
   % Full system: asynchronous composition of the two modules + the clock
   %
   system: MODULE = 
        (RENAME timeout TO ctrl_timeout IN controller)
     [] (RENAME timeout TO reactor_timeout IN reactor)
     [] clock;


   %
   % Lemmas: sal-inf-bmc -v 3 -d 1 -i drt_real_time <lemma>
   %
   time_aux0: LEMMA system |- G(time >= 0);

   time_aux1: LEMMA system |- G(time <= ctrl_timeout AND time <= reactor_timeout);

   time_aux2: LEMMA system |- G(ev.active => time = ev.delivery);


   ctrl_aux0: LEMMA system |- G(ctrl_state = a => ctrl_timeout <= time + SAMPLING_PERIOD);

   ctrl_aux1: LEMMA system |- G(ctrl_state = c => ctrl_timeout <= time + 30);

   ctrl_aux2: LEMMA system |- G(ctrl_state = e => ctrl_timeout <= time + 20);


   %
   % provable at depth 12 with lemmas time_aux0 to time_aux2 + ctrl_aux0 to ctrl_aux2
   % sal-inf-bmc -v 3 -d 12 -i -l time_aux0 -l time_aux1 -l time_aux2 -l ctrl_aux0 
   %    -l ctrl_aux1 -l ctrl_aux2 drt_real_time safety

   safety: THEOREM system |- G(state /= meltdown);

END