Skip to content

{var, N} leaks into postcondition/3 in a statem #52

@fishcakez

Description

@fishcakez

The vars should be evaluated before passed to a postcondition. A minimal example:

-module(counter_statem).

-include_lib("triq/include/triq.hrl").
-include_lib("triq/include/triq_statem.hrl").

-export([statem_prop/0]).
-export([initial_state/0]).
-export([command/1]).
-export([precondition/2]).
-export([next_state/3]).
-export([postcondition/3]).

statem_prop() ->
    ?FORALL(Cmds, commands(?MODULE),
            begin
                {_, _, Result} = run_commands(?MODULE, Cmds),
                Result =:= ok
            end).

initial_state() ->
    0.

command(Counter) ->
    oneof([{call, erlang, '+', [Counter, choose(0, 1)]},
           {call, erlang, '-', [Counter, choose(0, 1)]}]).

precondition(_, _) -> true.

next_state(_, NCounter, _) -> NCounter.

postcondition(Counter, {call, _, '+', _}, Result) -> Result >= Counter;
postcondition(Counter, {call, _, '-', _}, Result) -> Result =< Counter.

This fails because Counter in postcondition/3 is the virtual {var, N}.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions