automaton Fibonacci
  signature
    internal compute
  states
    a:Int := 1,
    b:Int := 0,
    c:Int := 1
  transitions
    internal compute
      eff a := b;
          b := c;
          c := a + b

invariant A of Fibonacci:
  a + b = c