uses NonDet

automaton Fibonacci
  signature
    input initialize(x:Int, y:Int)
    internal compute
  states
    initialized:Bool := false,
    a : Int, b : Int, c : Int
  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                           % The schedule block determines all the
    do                               % transitions the Simulator will execute.
      fire input initialize(randomInt(0,20), 16);  % first, initialize
      while true do  fire internal compute  od     % then continue with compute
    od