[erlang-questions] {precondition, false} in PropEr_statem

[Motiejus Jakštys]

On Wed, Jan 16, 2013 at 12:01:58AM +0100, Eirini Arvaniti wrote:
> On 15 January 2013 21:39, Motiejus Jakštys <desired.mta@REDACTED> wrote:
> 
> > Hi,
> > I introduced some preconditions to my stateful properties. Depending
> > on external state it returns true or false (if application somewhere
> > is turned on or not). After many (1000+ usually) tests I get this
> > error:
> >
> > History: <command history>
> > State: <last state>
> > Result: {precondition,false}
> >
> > It is natural that precondition sometimes returns false; that's the
> > reason to have them. But I couldn't figure what is wrong in this case.
> >
> > Snippet:
> >
> >     ?FORALL(Cmds, commands(?MODULE, initial_state(Nodes)),
> >         begin
> >                 % Every test should be run in a separate bucket
> >                 {History,State,Result} = run_commands(?MODULE, Cmds),
> >                 % ... clean up
> >                 ?WHENFAIL(
> >                     io:format("No: ~p~nHistory: ~p\nState: ~p\nResult:
> > ~p\n",
> >                         [Id, History, State,Result]),
> >                     Result =:= ok)
> >         end).
> >
> > What does it mean when PropEr returns {precondition, false}?
> >
> > Thanks,
> > Motiejus Jakštys
> >
> 
> 
> Hello Motiejus,
> 
> {precondition, false} means that a precondition is not satisfied during
> command execution.
> 
> When a command sequence is executed, preconditions are checked and are
> expected to be true,
> since they have been already checked (and were true) during command
> generation.
> A precondition may be expected to be false at runtime only when a
> counterexample is re-checked.
> During normal testing it should not happen.
> In your case, could it be that the external state on which preconditions
> depend changes during command execution?

Hello Eirini,

External state is indeed changed during runtime of the algorithm. I.e.
changing the external state is one of the of the commands that can be
generated. But it is the expected way proper_statem works, isn't it?

If I understand correctly, you are asking whether the state is changed
between command generation and actual execution, but somewhat from
remote. Then no. Or you are talking about different external state
change?

I will briefly illustrate what the system does, maybe I missed
something. Demobucket is just an OTP application.

These are the commands that change external state:

command(S) ->
    frequency([
            ...
            {1, {call, ?MODULE, stop_bucket, [rand_node(S)]}},
            {9, {call, ?MODULE, start_bucket, [rand_node(S)]}}
        ]).

start_bucket(Node) ->
    rpc:call(Node, application, start, [demobucket]).

stop_bucket(Node) ->
    rpc:call(Node, application, stop, [demobucket]).

%% some code to check if bucket runs anywhere but on Node
precondition(#state{nodes=AllNodes}, {call, ?MODULE, stop_bucket, [Node]}) ->
    Nodes = AllNodes -- [N],
    Cond = fun(Apps) -> lists:keyfind(demobucket, 1, Apps) /= false end,
    {[A|B], []} = rpc:multicall([N|Nodes], application, which_applications, []),
    Cond(A) andalso lists:any(Cond, B);

%% some code to check whether bucket doesn't run on Node
precondition(_, {call, ?MODULE, start_bucket, [Node]}) ->
    Apps = rpc:call(Node, application, which_applications, []),
    lists:keyfind(demobucket, 1, Apps) =:= false;

precondition(_, {call, ?MODULE, _, _}) ->
    true.

To sum up, unless I am looking at wrong direction, nothing except
stop_bucket/1 and start_bucket/1 change external system state.

Regards,
Motiejus