[[[[ Begin initialization [[[[
%%%% Modified state variables for impl automaton:
     a --> 1
     b --> 0
     c --> 1
%%%% Modified state variables for spec automaton:
     a --> 1
     b --> 0
     c --> 1
]]]] End initialization ]]]]
[[[[ Begin step 1 [[[[
     Executed impl transition: internal compute in automaton FiboImpl
%%%% Modified state variables for impl automaton:
     a --> 0
     b --> 1
     c --> 1
     Executed spec transition: internal compute in automaton FiboSpec using 1 for sum
%%%% Modified state variables for spec automaton:
     a --> 0
     b --> 1
     c --> 1
]]]] End step 1 ]]]]
[[[[ Begin step 2 [[[[
     Executed impl transition: internal compute in automaton FiboImpl
%%%% Modified state variables for impl automaton:
     a --> 1
     b --> 1
     c --> 2
     Executed spec transition: internal compute in automaton FiboSpec using 2 for sum
%%%% Modified state variables for spec automaton:
     a --> 1
     b --> 1
     c --> 2
]]]] End step 2 ]]]]
[[[[ Begin step 3 [[[[
     Executed impl transition: internal compute in automaton FiboImpl
%%%% Modified state variables for impl automaton:
     a --> 1
     b --> 2
     c --> 3
     Executed spec transition: internal compute in automaton FiboSpec using 3 for sum
%%%% Modified state variables for spec automaton:
     a --> 1
     b --> 2
     c --> 3
]]]] End step 3 ]]]]
[[[[ Begin step 4 [[[[
     Executed impl transition: internal compute in automaton FiboImpl
%%%% Modified state variables for impl automaton:
     a --> 2
     b --> 3
     c --> 5
     Executed spec transition: internal compute in automaton FiboSpec using 5 for sum
%%%% Modified state variables for spec automaton:
     a --> 2
     b --> 3
     c --> 5
]]]] End step 4 ]]]]