ttm {activity, internal_state, nt_action: TYPE; 
	        lower_bound:[nt_action -> timedef!time],
		upper_bound:[nt_action -> timedef!time],
		enabled_state:[states{activity, nt_action, 
		internal_state, timedef!time;}!states1 ->  bool], 
		graph:[states{activity, nt_action, 
		internal_state, timedef!time;}!states2 -> bool] }: CONTEXT = 
BEGIN
      %activ: TYPE;
      %internal_state: TYPE;
      %nt_action: TYPE; 
      t: CONTEXT = timedef;
      %states: TYPE = [# activ: activity, basic:internal_state, 
      %action_time: [nt_action  -> t!time] #];
      %enabled_state:[nt_action, internal_state -> bool];
      %states1: TYPE = [# nta:nt_action, is: internal_state #];
      %states2: TYPE = [# nta:nt_action, is: activity #];
      %enabled_state:[states1 -> bool];
      %graph:[states2 -> bool];
      %lower_bound:[nt_action -> t!time];
      %upper_bound:[nt_action -> t!time];
      cs: CONTEXT = states{activity, nt_action, 
		internal_state, timedef!time;};
      enabled_general(ac:nt_action,s:cs!states):bool =
               enabled_state((# nta := ac, is := s.basic, a := s.activ #))
               AND graph((# nta := ac, a := s.activ #));

% Only the tick can change the timers associated with the action.
% If enabled_general is not satisfied, It is reset to zero.
    
        update_clocks(s:cs!states): [nt_action->t!time] =
                (LAMBDA (q:nt_action):
                IF enabled_general(q,s) THEN
                   IF s.action_time(q) = lower_bound(q) AND
                         upper_bound(q) = t!infinity  THEN
                         s.action_time(q)
                   ELSE t!plus(s.action_time(q), t!one)
                   ENDIF
                ELSE t!zero
                ENDIF
                );

% After the normal action(except for Tick), Set the value of timers 
% according to the new enable conditions

        reset_clocks(ac:nt_action,s:cs!states): [nt_action->t!time] =
                (LAMBDA (q:nt_action):
                IF (enabled_general(q,s) AND q/=ac) THEN
                s.action_time(q)
                ELSE t!zero
                ENDIF
                );

        enabled_time(ac:nt_action, s:cs!states): bool =
                 t!geq(s.action_time(ac), lower_bound(ac)) AND  t!leq(s.action_time(ac), upper_bound(ac));

        enabled_tick(s:cs!states): bool =
                 FORALL (q:nt_action): enabled_general(q,s) =>(t!less(s.action_time(q),  upper_bound(q)));

END