anchor.diff:  %% utils
   %%-----------------------------------------------------------------------------
   
  +% Returns a symbolic call to one of the driver's functions
  +symb_call(Function, StreamName, MinTime) ->
  +    timer:sleep(50), % give time to CakeDB to flush
  +    case Function of
  +        append ->
  +            {call, ?DRIVER, append, [StreamName, list(integer(65,122))]};
  +        range_query ->
  +            Start = integer(MinTime, timestamp()),
  +            End = integer(MinTime, timestamp()),
  +            {call, ?DRIVER, range_query, [StreamName, Start, End]};
  +        _ -> % all_since and last_entry_at
  +            Now = {call, ?MODULE, timestamp, []},
  +            Diff = {call, ?MODULE, diff, [Now, MinTime]},
  +            Rand = {call, random, uniform, [Diff]},
  +            TS = {call, ?MODULE, sum, [MinTime, Rand]},
  +            {call, ?DRIVER, Function, [StreamName, TS]}
  +    end.
  +
  +diff(A,B) ->
  +    A-B.
  +
  +sum(A,B) ->
  +    A+B.
  +
  +% Check if list A is subset of list B
  +is_subset(A,B) ->
  +    lists:all(fun(X) -> lists:member(X,B) end, A).
  +
   % Returns the current timestamp
   timestamp() ->
       {Mega, Sec, Micro} = now(),
       Mega * 1000000 * 1000000 + Sec * 1000000 + Micro.
   
  -% Returns symbolic call to timestamp/0 function
  -timestamp_wrapper() ->
  -    {call,?MODULE,timestamp,[]}.
  -
  
positive.code: % define the commands to test
  command(S) ->
      oneof([
          {call,cakedb_driver,append,[elements(?STREAMNAMES),list(integer(32,255))]},
          {call,cakedb_driver,range_query,[
                  elements(?STREAMNAMES),
                  integer(S#state.starttime,timestamp_wrapper()),
                  integer(S#state.starttime,timestamp_wrapper())]},
          {call,cakedb_driver,all_since,[elements(?STREAMNAMES),integer(S#state.starttime,timestamp_wrapper())]},
          {call,cakedb_driver,last_entry_at,[elements(?STREAMNAMES),integer(S#state.starttime,timestamp_wrapper())]}
      ]).
  
  % define when a command is valid
  precondition(S,{call,cakedb_driver,last_entry_at,[StreamName,_Time]}) ->
      case lists:keysearch(StreamName,1,S#state.streams) of
          {value, {StreamName,Data}} ->
              Data =/= [];
          false ->
              false
      end;
  
negative.code:                     Result =:= []
              end
      end;
  postcondition(S, {call,?DRIVER,all_since,[StreamName,TS]}, Result) ->
      case lists:keysearch(StreamName,1,S#state.streams) of
          {value, {StreamName,Data}} ->
              Expected = [Y || {X,Y} <- Data, X>=TS];
          false ->
              Expected = []
      end,
      Observed = [Y || {_,Y} <- Result],
      is_subset(Expected, Observed);
  postcondition(S, {call,?DRIVER,last_entry_at,[StreamName,TS]}, Result) ->
      case lists:keysearch(StreamName,1,S#state.streams) of
          {value, {StreamName,Data}} ->
              io:format("~n[Y || {X,Y} <- Data]: ~p~n",[[Y || {X,Y} <- Data]]),%, X=<TS]]),
              io:format("Result: ~p~n~n",[Result]),
              true;
  %            lists:member(element(2,lists:nth(1,Result)), [Y || {X,Y} <- Data, X=<TS]);
          false ->
              io:format("~nResult (Should be empty): ~p~n",[Result]),
  %            Result =:= []
              true
      end;
  postcondition(_S, _V, _Result) ->
      true.
  