anchor.diff:      #state{ets=?ETS, types=?LATTICES, store=dict:new()}.
   
   %% Generate commands
  -command(#state{ets=Ets, types=_Types, store=Store}) ->
  +command(#state{ets=Ets, types=Types, store=Store}) ->
       Variables = dict:fetch_keys(Store),
       oneof(
  -        [{call, ?MODULE, declare, [undefined, Ets]}] ++
  -        % [{call, ?MODULE, declare,
  -        %   [oneof([elements(Types), undefined]), Ets]}] ++
  +        [{call, ?MODULE, declare,
  +          [oneof([elements(Types), undefined]), Ets]}] ++
           [{call, ?MODULE, read,
             [elements(Variables), undefined, Ets]} || length(Variables) > 0] ++
           [?LET({Variable, GeneratedValue}, {elements(Variables), nat()},
  
positive.code: next_state(#state{store=Store0}=S, V, {call, ?MODULE, declare, [Type, _]}) ->
      Store = dict:store(V, #variable{type=Type}, Store0),
      S#state{store=Store};
  next_state(S, _V, {call, ?MODULE, bind, _}) ->
      S;
  
  %% Next state transformation
  next_state(S,_V,{call,_,_,_}) ->
      S.
  
  precondition(#state{store=Store},
               {call, ?MODULE, read, [Id, _Threshold, _Store]}) ->
      case dict:find(Id, Store) of
          error ->
              %% Not declared.
  
negative.code:         {ok, #variable{type=Type, value=Value}=Variable} ->
              case derflow_ets:is_inflation(Type, Value, NewValue) of
                  true ->
                      dict:store(Id, Variable#variable{value=NewValue}, Store0);
                  false ->
                      Store0
              end
  