automaton Adder
  signature
    input  add(i, j: Int)
    output result(k: Int)
  states
    value: Int := 0,
    ready: Bool := false
  transitions
    input add(i, j)
      eff value := i + j;
          ready := true
    output result(k)
      pre k = value /\ ready
      eff value := 0;
          ready := false

invariant of Adder:
  ~ready => value = 0