This example shows how a timed finite state machine can be systematically modeled in TESL (however, a language for defining such a mapping from TFSM to TESL in a generic way is still future work). We model a two-state protocol finite state machine waiting for a request and then waiting for an acknowledgement for 10 units of time. If the acknowledgement does not occur before the delay, a reset event is produced.

unit-clock allEvents
decimal-clock chronometer

/**** States ****/
// State Ready
unit-clock in_Ready
unit-clock enter_Ready
unit-clock leave_Ready
allEvents sustained from enter_Ready to leave_Ready implies in_Ready

// State Waiting
unit-clock in_Waiting
unit-clock enter_Waiting
unit-clock leave_Waiting
allEvents sustained from enter_Waiting to leave_Waiting implies in_Waiting

/**** Transitions ****/
// Transition: Ready -> Waiting when request produces reply
event_request when in_Ready implies enter_Waiting
event_request when in_Ready implies leave_Ready
event_request when in_Ready implies action_reply

// Transition: Waiting -> Ready when ack produces None
event_ack when in_Waiting implies enter_Ready
event_ack when in_Waiting implies leave_Waiting

// Transition: Waiting -> Ready when 10.0 produces reset
timeout_Waiting_to_Ready when in_Waiting implies enter_Ready
timeout_Waiting_to_Ready when in_Waiting implies leave_Waiting
timeout_Waiting_to_Ready when in_Waiting implies action_reset

/**** Actions ****/
// Output action: reset
unit-clock action_reset

// Output action: reply
unit-clock action_reply

/**** Events ****/
// Input event: ack
unit-clock event_ack
event_ack implies allEvents

// Input event: request
unit-clock event_request
event_request implies allEvents

// Event: delay 10.0 after entering Waiting
// the "with reset" avoid the production of spurious events when
// the Waiting state is leaved before the expiration of the delay
unit-clock timeout_Waiting_to_Ready
enter_Waiting time delayed by 10.0 on chronometer
                           with reset on leave_Waiting
                           implies timeout_Waiting_to_Ready
timeout_Waiting_to_Ready implies allEvents

// Initial state
decimal-clock start sporadic 0
tag relation start = chronometer
start implies allEvents
start implies enter_Ready

/**** Scenario ****/
start time delayed by 5.0 on chronometer implies event_request
start time delayed by 13.0 on chronometer implies event_ack
start time delayed by 19.0 on chronometer implies event_request

@tagref chronometer
@output tikz select in_Ready, enter_Ready, leave_Ready, in_Waiting, enter_Waiting, 
                    leave_Waiting, action_reset, action_reply, event_request, event_ack, 
                    timeout_Waiting_to_Ready -> timeout_W_to_R, start, allEvents
             xscale 0.5
@output svg xscale 20 standalone

The following results shows that event_request is not produced when the acknowledgement comes in time, and is produced when it comes after the 10 time units delay: