uses NonDet

automaton Fibonacci
  signature
    input initialize(x:Int, y:Int)
    internal compute
  states
    initialized:Bool := false,
    a : Int, b : Int, c : Int
    so that a + b = c
  transitions
    input initialize(x, y)
      eff if (initialized = false) then
            a := y - x;
            b := x;
            c := y;
            initialized := true
          fi
    internal compute
      pre initialized = true
      eff a := b; b := c; c := a + b
  schedule
    do
      fire input initialize(randomInt(0,30), randomInt(-20, 20));
      while true do  fire internal compute  od
    od