automaton FibonacciNDChoose                     % does not run in the Simulator
  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 where 0 <= x /\ x <= 50;  % Simulator doesn't know
          c := choose y:Int where 0 <= x /\ x <= 50;  % how to resolve a choose
          a := c - b;
          initialized := true
    internal compute
      pre initialized
      eff a := b;
          b := c;
          c := a + b