% Variant of example from TIOA User Guide, 9/28/05, Figure 3.5, page 10

let legalTime(hour, minute: Nat) = minute < 60 /\ hour < 24

automaton Alarm
  signature
    input  showTime(hour, minute: Nat) where legalTime(hour, minute),
           setAlarm(hour, minute: Nat) where legalTime(hour, minute),
           toggleAlarm
    output ring
  states
    alarmTime: Nat := 0,
    turnedOn: Bool := false,
    ringNow: Bool := false
  transitions
    input setAlarm(hour, minute)
      eff alarmTime := (60*hour) + minute
    input showTime(hour, minute)
      eff ringNow := turnedOn /\ alarmTime = (60*hour) + minute
    input toggleAlarm
      eff turnedOn := ~turnedOn
    output ring
      pre ringNow
      eff ringNow := false
      
 automaton ClockA
  signature
    output show(hour, minute: Nat) where legalTime(hour, minute)
    input  set(hour, minute: Nat) where legalTime(hour, minute)
  states 
    now: Real := 0,
    nextHour: Nat := 12,
    nextMinute: Nat := 0,
    timeToShow: DiscreteReal := 0
  transitions 
    input set(hour, minute)
      eff nextHour := hour;
	      nextMinute := minute;
	      timeToShow := now
    output show(hour, minute)
      pre hour = nextHour /\ minute = nextMinute /\ now = timeToShow
      eff nextMinute := mod(minute + 1, 60);
	      if nextMinute = 0 then nextHour := mod(hour + 1, 12) fi;
	      timeToShow := now + 1
  trajectories
    trajdef timePassage
      stop when now = timeToShow
      evolve d(now) = 1
      

automaton AlarmClockA
  components ClockA; Alarm