%%%%%%%%%%%%%%%%%%%%
% The ALARM module %
%%%%%%%%%%%%%%%%%%%%

module ALARM :

% To handle the alarm time:

type ALARM_TIME_TYPE;
constant INITIAL_ALARM_TIME : ALARM_TIME_TYPE;
function TOGGLE_24H_MODE_IN_ALARM_TIME (ALARM_TIME_TYPE) : ALARM_TIME_TYPE;

% To set the alarm time:

type ALARM_TIME_POSITION;
constant INITIAL_ALARM_TIME_POSITION : ALARM_TIME_POSITION;
function NEXT_ALARM_TIME_POSITION (ALARM_TIME_POSITION) : ALARM_TIME_POSITION;
         % say from hours to 10-minutes to minutes and circularly
         % (not relevant for ESTEREL)
function SET_ALARM_TIME (ALARM_TIME_TYPE, ALARM_TIME_POSITION)
                       : ALARM_TIME_TYPE;
         % applies a setting command

% To communicate with a watch:

type WATCH_TIME_TYPE;
function COMPARE_ALARM_TIME_TO_WATCH_TIME
                          (ALARM_TIME_TYPE, WATCH_TIME_TYPE) : boolean;

% To beep:

type BEEP_TYPE;
constant ALARM_BEEP_VALUE : BEEP_TYPE;
constant ALARM_DURATION : integer;

% Interface

input TOGGLE_24H_MODE_COMMAND;

output ALARM_TIME : ALARM_TIME_TYPE;

input ENTER_SET_ALARM_MODE_COMMAND,
      SET_ALARM_COMMAND,
      NEXT_ALARM_TIME_POSITION_COMMAND,
      EXIT_SET_ALARM_MODE_COMMAND;

output START_ENHANCING : ALARM_TIME_POSITION,
       STOP_ENHANCING : ALARM_TIME_POSITION;

input WATCH_TIME : WATCH_TIME_TYPE;
input WATCH_BEING_SET;

input S;
input TOGGLE_ALARM_COMMAND,
      STOP_ALARM_BEEP_COMMAND;

output ALARM_STATUS : boolean;
output BEEP : BEEP_TYPE;

relation WATCH_BEING_SET => WATCH_TIME;

         % all the other signals are pairwise incompatible,
         % except STOP_ALARM_BEEP_COMMAND that may appear anytime
relation   S
         # TOGGLE_24H_MODE_COMMAND
         # TOGGLE_ALARM_COMMAND
         # ENTER_SET_ALARM_MODE_COMMAND
         # SET_ALARM_COMMAND
         # NEXT_ALARM_TIME_POSITION_COMMAND
         # EXIT_SET_ALARM_MODE_COMMAND;

% Body

signal START_BEEPING in

   % initializations

   emit ALARM_TIME (INITIAL_ALARM_TIME);
   emit ALARM_STATUS (false);

   % main loop

   loop
      % normal mode
      abort % when ENTER_SET_ALARM_MODE_COMMAND
         loop
            await
               case TOGGLE_24H_MODE_COMMAND do
                  emit ALARM_TIME
                         (TOGGLE_24H_MODE_IN_ALARM_TIME(pre(?ALARM_TIME)))
               case TOGGLE_ALARM_COMMAND do
                  emit ALARM_STATUS (not(pre(?ALARM_STATUS)))
               case WATCH_TIME do
                  present WATCH_BEING_SET else
                     if COMPARE_ALARM_TIME_TO_WATCH_TIME
                                         (?ALARM_TIME, ? WATCH_TIME)
                        and ?ALARM_STATUS
                     then 
                        emit START_BEEPING 
                     end if
                  end present
            end await
         end loop
      when ENTER_SET_ALARM_MODE_COMMAND;

      % set-alarm mode
      % the currently set position is the value of START_ENHANCING
      % (one might also accept TOGGLE_24H_MODE_COMMAND
      % and TOGGLE_ALARM_COMMAND; for this one just has to
      % copy the corresponding cases above into the next await).
      % Notice that the alarm does not ring in set mode

      abort % when EXIT_SET_ALARM_MODE_COMMAND
         emit START_ENHANCING (INITIAL_ALARM_TIME_POSITION);
         loop
            await
               case SET_ALARM_COMMAND do
                   emit ALARM_TIME (SET_ALARM_TIME (pre(?ALARM_TIME),
                                                    ?START_ENHANCING))
               case NEXT_ALARM_TIME_POSITION_COMMAND do
                   emit STOP_ENHANCING (pre(?START_ENHANCING));
                   emit START_ENHANCING 
                         (NEXT_ALARM_TIME_POSITION(pre(?START_ENHANCING)))
            end await
         end loop
      when EXIT_SET_ALARM_MODE_COMMAND;
      emit STOP_ENHANCING (?START_ENHANCING);
      emit ALARM_STATUS (true)
   end loop
||
   % beeping sequence
   every START_BEEPING do
      abort
         loop emit BEEP (ALARM_BEEP_VALUE) each S
      when 
         case STOP_ALARM_BEEP_COMMAND 
         case ALARM_DURATION S
      end abort
   end every
end signal
end module

