uses NonDet

automaton Fibonacci
  signature
    internal initialize
    internal compute
  states
    initialized:Bool := false,
    a : Int, b : Int, c : Int
  transitions
    internal initialize
      pre initialized = false
      eff b := choose x:Int det do yield 5 od;         %% always use 5
          c := choose y:Int yield randomInt(0, 50);    %% choose a random Int
          a := c - b;
          initialized := true
    internal compute
      pre initialized
      eff a := b;
          b := c;
          c := a + b