automaton Clock
  signature 
    input  request
    output clock(t: Nat)
    internal tick
  states 
    counter: Nat := 0,
    flag: Bool := false
  transitions 
    internal tick
      pre true
      eff counter := counter + 1
    input request
      eff  flag := true
    output clock(t)
      pre flag /\ counter = t
      eff flag := false
  tasks
    {tick};
    {clock(t)}