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.

(:svg width="350" height="170" style="margin-top: 2ex;":) <defs>

  <marker id="arrow" markerWidth="11" markerHeight="15" refx="4" refy="10" orient="auto">
    <path d="M 4 10 l -4 4 l 10 -4 l -10 -4 l 4 4" stroke="black" fill="black"/>
  </marker>

</defs> <style type="text/css">

  text {
    font-family: sans-serif;
    font-size: 12pt;
  }
  circle.state {
    fill: white;
    stroke: black;
    stroke-width: 2;
  }
  text.state {
    text-anchor: middle;
    alignment-baseline: middle;
  }
  text.trans {
    text-anchor: middle;
    alignment-baseline: middle;
  }
  path.trans {
    stroke: black;
    fill: none;
    marker-end: url(#arrow);
  }

</style> <circle class="state" cx="50" cy="85" r="40"/> <text class="state" x="50" y="85">Ready</text> <circle class="state" cx="300" cy="85" r="40"/> <text class="state" x="300" y="85">Waiting</text> <path d="M 75 45 q 100 -50 195 0" stroke="black" fill="none" marker-end="url(#arrow)"/> <text class="trans" x="175" y="10">request/reply</text> <path class="trans" d="M 255 85 l -150 0"/> <text class="trans" x="175" y="77">ack</text> <path class="trans" d="M 275 125 q -100 50 -195 0"/> <text class="trans" x="175" y="165">after 10.0/reset</text> (:endsvg:)

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: