automaton FiboSpec
  signature
    internal compute
  states
    a:Int, b:Int, c:Int             %% no initial values specified
    so that a + b = c
  transitions
    internal compute
      eff a := b;
          b := c;
          c := choose sum where sum = a + b                        %% NEW CODE

automaton FiboImpl                  %% identical to the Fibonacci automaton
 signature                          %% defined in Listing 2-1
   internal compute
 states
   a:Int := 1,
   b:Int := 0,
   c:Int := 1
 transitions
   internal compute
     eff a := b;
         b := c;
         c := a + b

forward simulation from FiboImpl to FiboSpec:
  (FiboImpl.a = FiboSpec.a /\
   FiboImpl.b = FiboSpec.b /\
   FiboImpl.c = FiboSpec.c)
  proof
    initially
      FiboSpec.a := FiboImpl.a;     %% specifies initial values for
      FiboSpec.b := FiboImpl.b;     %% the state variables of FiboSpec
      FiboSpec.c := FiboImpl.c
    for internal compute do
      fire internal compute using FiboImpl.a+FiboImpl.b for sum    %% NEW CODE
    od