Difference between revisions of "CirqBuff and MBox QuickCheck Models"

From CERES
Jump to: navigation, search
 
(3 intermediate revisions by one user not shown)
Line 1: Line 1:
−
This page contains the complete CirqBuff and MBox [http://www.quviq.com/quickcheck-2/ QuickCheck] models described in the paper entitled ''Modelling of Autosar Libraries for Large Scale Testing'' by [[Wojciech Mostowski]], Thomas Arts, and John Hughes. The complete model archive can be downloaded here, below the complete model quote.
+
This page contains the complete CirqBuff and MBox [http://www.quviq.com/quickcheck-2/ QuickCheck] models described in the paper entitled ''Modelling of Autosar Libraries for Large Scale Testing'' by [[Wojciech Mostowski]], Thomas Arts, and John Hughes. The complete model archive can be  
 +
[[media:cirqbuff_mbox_qc_model.zip|downloaded here]], below the complete model quote. The C source files referenced by the model are available on request, please contact [mailto:wojciech.mostowski@hh.se Wojciech Mostowski].
  
  
Line 5: Line 6:
  
 
<pre>
 
<pre>
 +
-define(AUTOSAR_SRC, ".").
 
</pre>
 
</pre>
  
Line 10: Line 12:
  
 
<pre>
 
<pre>
 +
-record(cb_state, {ptr, size, elements, data_size}).
 
</pre>
 
</pre>
  
Line 15: Line 18:
  
 
<pre>
 
<pre>
 +
-module(qc_cb_setup).
 +
-export([ setup/0 ]).
 +
 +
-include_lib("eqc/include/eqc_c.hrl").
 +
-include_lib("source_path.hrl").
 +
 +
setup() -> eqc_c:start(cb,
 +
  [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"},
 +
    {c_src, ?AUTOSAR_SRC ++ "/src/cirq_buffer.c"} ]).
 
</pre>
 
</pre>
  
Line 20: Line 32:
  
 
<pre>
 
<pre>
 +
-module(qc_cb).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_component.hrl").
 +
-include_lib("cb.hrl"). % Auto-generated
 +
-include_lib("qc_cb.hrl").
 +
 +
initial_state() -> #cb_state{ elements=[] }.
 +
 +
invariant(S) -> length(S#cb_state.elements) =< S#cb_state.size.
 +
 +
postcondition_common(_S, {call, _, create, _, _ }, _Res) -> true;
 +
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).
 +
 +
create(Size, DataSize) -> cb:'CirqBuffDynCreate'(Size, DataSize).
 +
create_args(_S) -> [nat(), nat()].
 +
create_pre(S, [Size, _DataSize]) -> S#cb_state.ptr == undefined andalso Size > 0.
 +
create_next(S, R, [Size, DataSize]) ->
 +
  S#cb_state{ptr=R, size=Size, data_size = DataSize }.
 +
create_callers() -> [qc_mbox].
 +
create_return(_S, [Size, DataSize]) ->
 +
  #'CirqBufferType' { maxCnt = Size, currCnt = 0, dataSize = DataSize,
 +
    head = 'NULL', tail = 'NULL', bufStart = 'NULL', bufEnd = 'NULL' }.
 +
 +
push(Ptr, Val) ->  DataPtr = eqc_c:create_array(unsigned_char, Val),
 +
  CallRes = cb:'CirqBuffPush'(Ptr, DataPtr), eqc_c:free(DataPtr), CallRes.
 +
push_args(S) -> [S#cb_state.ptr, vector(S#cb_state.data_size, char())].
 +
push_pre(S) ->
 +
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) < S#cb_state.size.
 +
push_next(S, _R, [_Ptr, Value]) ->
 +
  S#cb_state{elements = S#cb_state.elements ++ [Value]}.
 +
push_return(S, _Args) -> % 0.
 +
  if length(S#cb_state.elements) < 128 -> 0; true -> 1 end.
 +
push_callers() -> [qc_mbox].
 +
 +
pop(Ptr, DataSize) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, DataSize)]),
 +
  CallRes = cb:'CirqBuffPop'(Ptr, DataPtr),
 +
  DataRes = eqc_c:read_array(DataPtr, DataSize),
 +
  eqc_c:free(DataPtr), {DataRes, CallRes}.
 +
pop_args(S) -> [S#cb_state.ptr, S#cb_state.data_size].
 +
pop_pre(S) ->
 +
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) > 0.
 +
pop_next(S, _R, _Args) -> S#cb_state{elements = tl(S#cb_state.elements)}.
 +
pop_return(S, _Args) -> {hd(S#cb_state.elements), 0}.
 +
pop_callers() -> [qc_mbox].
 +
 +
prop_cb_length() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
  begin {H, S, Res} = run_commands(Cmds),
 +
    aggregate(command_names(Cmds),
 +
      measure(num_commands,
 +
        commands_length(Cmds),
 +
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok))) end)).
 +
 +
prop_cb() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
  begin {_, _, Res} = run_commands(Cmds), Res == ok end)).
 
</pre>
 
</pre>
  
Line 25: Line 96:
  
 
<pre>
 
<pre>
 +
-record(mbox_state, {ptr, size, elements, cb_state}).
 
</pre>
 
</pre>
  
Line 30: Line 102:
  
 
<pre>
 
<pre>
 +
-include_lib("source_path.hrl").
 +
 +
api_spec() -> #api_spec {
 +
  language = c, mocking = eqc_mocking_c,
 +
  modules  = [ #api_module{ name = mbox, functions = [
 +
    #api_fun_c{ name = 'CirqBuffDynCreate', ret = 'CirqBufferType *',
 +
                args = [ #api_arg_c{type = size_t, name = size, dir = in},
 +
                        #api_arg_c{type = size_t, name = dataSize, dir = in} ],
 +
                classify = {qc_cb, create} },
 +
    #api_fun_c{ name = 'CirqBuffPush', ret = int,
 +
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
 +
                        #api_arg_c{ type = 'void *', name = dataPtr, dir = in,
 +
                          stored_type = 'unsigned char *',
 +
                          buffer = {true, "cPtr->dataSize"}} ],
 +
                classify = {qc_cb, push} },
 +
    #api_fun_c{ name = 'CirqBuffPop',  ret = int,
 +
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
 +
                        #api_arg_c{ type = 'void *', name = dataPtr, dir = out,
 +
                          stored_type = 'unsigned char *',
 +
                          buffer = {true, "cPtr->dataSize"}} ],
 +
                classify = {qc_cb, pop} }]}]}.
 +
 +
start_mocking() -> eqc_mocking_c:start_mocking(mbox, ?MODULE:api_spec(),
 +
  [ "Std_Types.h", "cirq_buffer.h", "mbox.h" ],
 +
  [ ?AUTOSAR_SRC ++ "/src/mbox.c" ],
 +
  [ {cppflags, "-std=c99 -I . -I " ++ ?AUTOSAR_SRC ++ "/include"} ]).
 
</pre>
 
</pre>
  
Line 35: Line 133:
  
 
<pre>
 
<pre>
 +
-module(qc_mbox_setup).
 +
 +
-compile(export_all).
 +
 +
-include_lib("eqc/include/eqc_c.hrl").
 +
-include_lib("eqc/include/eqc_mocking.hrl").
 +
 +
-include("qc_mbox_capi.erl").
 
</pre>
 
</pre>
  
Line 40: Line 146:
  
 
<pre>
 
<pre>
 +
-module(qc_mbox).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_component.hrl").
 +
-include_lib("qc_mbox.hrl").
 +
-include_lib("qc_cb.hrl").
 +
 +
-include("mbox.hrl"). % Auto-generated
 +
-include("qc_mbox_capi.erl").
 +
 +
-define(PTR_SIZE, 8). % Change resp. for test running platform (here 64 bit arch.)
 +
 +
initial_state() -> #mbox_state{ elements=[] }.
 +
 +
invariant(S) -> length(S#mbox_state.elements) =< S#mbox_state.size.
 +
 +
postcondition_common(_S, {call, _, create, _, _ }, _R) -> true;
 +
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).
 +
 +
create(Size) -> mbox:'Arc_MBoxCreate'(Size).
 +
create_args(_S) -> [choose(1, 256)].
 +
create_pre(S, [Size]) -> S#mbox_state.ptr == undefined andalso Size > 0.
 +
create_next(S, R, [Size]) -> S#mbox_state{ptr=R, size=Size }.
 +
create_callouts(_S, [Size]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffDynCreate', [Size, ?PTR_SIZE],
 +
  #'CirqBufferType' { maxCnt = Size, currCnt = 0,
 +
    dataSize = 8, head = 'NULL', tail = 'NULL',
 +
    bufStart = 'NULL', bufEnd = 'NULL'}).
 +
 +
post(Ptr, Val) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, Val),
 +
  CallRes = mbox:'Arc_MBoxPost'(Ptr, DataPtr),
 +
  eqc_c:free(DataPtr), CallRes.
 +
post_args(S) -> [S#mbox_state.ptr, vector(?PTR_SIZE, char())].
 +
post_pre(S) -> S#mbox_state.ptr /= undefined
 +
  andalso length(S#mbox_state.elements) < S#mbox_state.size.
 +
post_next(S, _R, [_Ptr, Value]) ->
 +
  S#mbox_state{elements = S#mbox_state.elements ++ [Value]}.
 +
post_return(_S, _Args) -> 0.
 +
post_callouts(S, [_Ptr, Value]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffPush', [?WILDCARD, Value],
 +
  if length(S#mbox_state.elements) < 128 -> 0; true -> 1 end).
 +
 +
fetch(Ptr) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, ?PTR_SIZE)]),
 +
  CallRes = mbox:'Arc_MBoxFetch'(Ptr, DataPtr),
 +
  DataRes = eqc_c:read_array(DataPtr, ?PTR_SIZE),
 +
  eqc_c:free(DataPtr), {DataRes, CallRes}.
 +
fetch_args(S) -> [S#mbox_state.ptr].
 +
fetch_pre(S) ->
 +
  S#mbox_state.ptr /= undefined andalso length(S#mbox_state.elements) > 0.
 +
fetch_next(S, _R, [_Ptr]) -> S#mbox_state{elements = tl(S#mbox_state.elements)}.
 +
fetch_return(S, [_Ptr]) -> {hd(S#mbox_state.elements), 0}.
 +
fetch_callouts(S, [_Ptr]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffPop', [?WILDCARD], { hd(S#mbox_state.elements), 0}).
 +
 +
weight(#mbox_state{ptr = undefined}, Op) -> case Op of create -> 1; _ -> 0 end;
 +
weight(_S, create) -> 0; weight(_S, post) -> 5; weight(_S, fetch) -> 1.
 +
 +
prop_mbox() ->
 +
  ?SETUP(fun() -> qc_mbox:start_mocking(), fun() -> ok end end,
 +
  ?FORALL(Cmds, more_commands(50, commands(?MODULE)),
 +
  begin {H, S, Res} = run_commands(Cmds),
 +
    aggregate(command_names(Cmds),
 +
      pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end)).
 
</pre>
 
</pre>
  
Line 45: Line 217:
  
 
<pre>
 
<pre>
 +
-module(qc_cluster).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_cluster.hrl").
 +
-include_lib("source_path.hrl").
 +
 +
components() -> [qc_cb, qc_mbox].
 +
 +
api_spec() -> eqc_cluster:api_spec(?MODULE).
 +
 +
setup_mocking() ->
 +
  eqc_mocking_c:start_mocking(mbox, api_spec(),
 +
    [ "cirq_buffer.h", "mbox.h" ],
 +
    [ ?AUTOSAR_SRC ++ "/src/mbox.c", ?AUTOSAR_SRC ++ "/src/cirq_buffer.c" ],
 +
    [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"} ],
 +
    components()).
 +
 +
property_mbox_cluster() ->
 +
  ?SETUP(fun() -> setup_mocking(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
    begin {H, S, Res} = run_commands(Cmds),
 +
      aggregate(command_names(Cmds),
 +
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end )).
 
</pre>
 
</pre>

Latest revision as of 18:14, 27 December 2016

This page contains the complete CirqBuff and MBox QuickCheck models described in the paper entitled Modelling of Autosar Libraries for Large Scale Testing by Wojciech Mostowski, Thomas Arts, and John Hughes. The complete model archive can be downloaded here, below the complete model quote. The C source files referenced by the model are available on request, please contact Wojciech Mostowski.


source_path.hrl

-define(AUTOSAR_SRC, ".").

qc_cb.hrl

-record(cb_state, {ptr, size, elements, data_size}).

qc_cb_setup.erl

-module(qc_cb_setup).
-export([ setup/0 ]).

-include_lib("eqc/include/eqc_c.hrl").
-include_lib("source_path.hrl").

setup() -> eqc_c:start(cb,
  [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"},
    {c_src, ?AUTOSAR_SRC ++ "/src/cirq_buffer.c"} ]).

qc_cb.erl

-module(qc_cb).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").
-include_lib("cb.hrl"). % Auto-generated
-include_lib("qc_cb.hrl").

initial_state() -> #cb_state{ elements=[] }.

invariant(S) -> length(S#cb_state.elements) =< S#cb_state.size.

postcondition_common(_S, {call, _, create, _, _ }, _Res) -> true;
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).

create(Size, DataSize) -> cb:'CirqBuffDynCreate'(Size, DataSize).
create_args(_S) -> [nat(), nat()].
create_pre(S, [Size, _DataSize]) -> S#cb_state.ptr == undefined andalso Size > 0.
create_next(S, R, [Size, DataSize]) ->
  S#cb_state{ptr=R, size=Size, data_size = DataSize }.
create_callers() -> [qc_mbox].
create_return(_S, [Size, DataSize]) ->
  #'CirqBufferType' { maxCnt = Size, currCnt = 0, dataSize = DataSize,
    head = 'NULL', tail = 'NULL', bufStart = 'NULL', bufEnd = 'NULL' }.

push(Ptr, Val) ->  DataPtr = eqc_c:create_array(unsigned_char, Val),
  CallRes = cb:'CirqBuffPush'(Ptr, DataPtr), eqc_c:free(DataPtr), CallRes.
push_args(S) -> [S#cb_state.ptr, vector(S#cb_state.data_size, char())].
push_pre(S) ->
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) < S#cb_state.size.
push_next(S, _R, [_Ptr, Value]) ->
  S#cb_state{elements = S#cb_state.elements ++ [Value]}.
push_return(S, _Args) -> % 0.
  if length(S#cb_state.elements) < 128 -> 0; true -> 1 end.
push_callers() -> [qc_mbox].

pop(Ptr, DataSize) -> 
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, DataSize)]),
  CallRes = cb:'CirqBuffPop'(Ptr, DataPtr),
  DataRes = eqc_c:read_array(DataPtr, DataSize),
  eqc_c:free(DataPtr), {DataRes, CallRes}.
pop_args(S) -> [S#cb_state.ptr, S#cb_state.data_size].
pop_pre(S) ->
   S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) > 0.
pop_next(S, _R, _Args) -> S#cb_state{elements = tl(S#cb_state.elements)}.
pop_return(S, _Args) -> {hd(S#cb_state.elements), 0}. 
pop_callers() -> [qc_mbox].

prop_cb_length() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
  begin {H, S, Res} = run_commands(Cmds),
    aggregate(command_names(Cmds),
      measure(num_commands,
        commands_length(Cmds), 
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok))) end)).

prop_cb() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
  begin {_, _, Res} = run_commands(Cmds), Res == ok end)).

qc_mbox.hrl

-record(mbox_state, {ptr, size, elements, cb_state}).

qc_mbox_capi.erl

-include_lib("source_path.hrl").

api_spec() -> #api_spec {
  language = c, mocking = eqc_mocking_c,
  modules  = [ #api_module{ name = mbox, functions = [
    #api_fun_c{ name = 'CirqBuffDynCreate', ret = 'CirqBufferType *',
                args = [ #api_arg_c{type = size_t, name = size, dir = in},
                         #api_arg_c{type = size_t, name = dataSize, dir = in} ],
                classify = {qc_cb, create} },
    #api_fun_c{ name = 'CirqBuffPush', ret = int,
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
                         #api_arg_c{ type = 'void *', name = dataPtr, dir = in,
                           stored_type = 'unsigned char *',
                           buffer = {true, "cPtr->dataSize"}} ],
                classify = {qc_cb, push} },
    #api_fun_c{ name = 'CirqBuffPop',  ret = int,
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
                         #api_arg_c{ type = 'void *', name = dataPtr, dir = out,
                           stored_type = 'unsigned char *',
                           buffer = {true, "cPtr->dataSize"}} ],
                classify = {qc_cb, pop} }]}]}.

start_mocking() -> eqc_mocking_c:start_mocking(mbox, ?MODULE:api_spec(),
  [ "Std_Types.h", "cirq_buffer.h", "mbox.h" ],
  [ ?AUTOSAR_SRC ++ "/src/mbox.c" ],
  [ {cppflags, "-std=c99 -I . -I " ++ ?AUTOSAR_SRC ++ "/include"} ]).

qc_mbox_setup.erl

-module(qc_mbox_setup).

-compile(export_all).

-include_lib("eqc/include/eqc_c.hrl").
-include_lib("eqc/include/eqc_mocking.hrl").

-include("qc_mbox_capi.erl").

qc_mbox.erl

-module(qc_mbox).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").
-include_lib("qc_mbox.hrl").
-include_lib("qc_cb.hrl").

-include("mbox.hrl"). % Auto-generated
-include("qc_mbox_capi.erl").

-define(PTR_SIZE, 8). % Change resp. for test running platform (here 64 bit arch.)

initial_state() -> #mbox_state{ elements=[] }.

invariant(S) -> length(S#mbox_state.elements) =< S#mbox_state.size.

postcondition_common(_S, {call, _, create, _, _ }, _R) -> true;
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).

create(Size) -> mbox:'Arc_MBoxCreate'(Size).
create_args(_S) -> [choose(1, 256)].
create_pre(S, [Size]) -> S#mbox_state.ptr == undefined andalso Size > 0.
create_next(S, R, [Size]) -> S#mbox_state{ptr=R, size=Size }.
create_callouts(_S, [Size]) -> 
  ?CALLOUT(mbox, 'CirqBuffDynCreate', [Size, ?PTR_SIZE], 
  #'CirqBufferType' { maxCnt = Size, currCnt = 0,
    dataSize = 8, head = 'NULL', tail = 'NULL',
    bufStart = 'NULL', bufEnd = 'NULL'}).

post(Ptr, Val) -> 
  DataPtr = eqc_c:create_array(unsigned_char, Val),
  CallRes = mbox:'Arc_MBoxPost'(Ptr, DataPtr),
  eqc_c:free(DataPtr), CallRes.
post_args(S) -> [S#mbox_state.ptr, vector(?PTR_SIZE, char())].
post_pre(S) -> S#mbox_state.ptr /= undefined
  andalso length(S#mbox_state.elements) < S#mbox_state.size.
post_next(S, _R, [_Ptr, Value]) ->
  S#mbox_state{elements = S#mbox_state.elements ++ [Value]}.
post_return(_S, _Args) -> 0.
post_callouts(S, [_Ptr, Value]) ->
  ?CALLOUT(mbox, 'CirqBuffPush', [?WILDCARD, Value],
  if length(S#mbox_state.elements) < 128 -> 0; true -> 1 end).

fetch(Ptr) -> 
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, ?PTR_SIZE)]),
  CallRes = mbox:'Arc_MBoxFetch'(Ptr, DataPtr),
  DataRes = eqc_c:read_array(DataPtr, ?PTR_SIZE),
  eqc_c:free(DataPtr), {DataRes, CallRes}.
fetch_args(S) -> [S#mbox_state.ptr].
fetch_pre(S) -> 
  S#mbox_state.ptr /= undefined andalso length(S#mbox_state.elements) > 0.
fetch_next(S, _R, [_Ptr]) -> S#mbox_state{elements = tl(S#mbox_state.elements)}.
fetch_return(S, [_Ptr]) -> {hd(S#mbox_state.elements), 0}.
fetch_callouts(S, [_Ptr]) -> 
  ?CALLOUT(mbox, 'CirqBuffPop', [?WILDCARD], { hd(S#mbox_state.elements), 0}).

weight(#mbox_state{ptr = undefined}, Op) -> case Op of create -> 1; _ -> 0 end;
weight(_S, create) -> 0; weight(_S, post) -> 5; weight(_S, fetch) -> 1.

prop_mbox() ->
  ?SETUP(fun() -> qc_mbox:start_mocking(), fun() -> ok end end,
  ?FORALL(Cmds, more_commands(50, commands(?MODULE)),
  begin {H, S, Res} = run_commands(Cmds),
    aggregate(command_names(Cmds),
      pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end)).

qc_cluster.erl

-module(qc_cluster).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_cluster.hrl").
-include_lib("source_path.hrl").

components() -> [qc_cb, qc_mbox].

api_spec() -> eqc_cluster:api_spec(?MODULE).

setup_mocking() ->
  eqc_mocking_c:start_mocking(mbox, api_spec(),
    [ "cirq_buffer.h", "mbox.h" ],
    [ ?AUTOSAR_SRC ++ "/src/mbox.c", ?AUTOSAR_SRC ++ "/src/cirq_buffer.c" ],
    [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"} ],
    components()).

property_mbox_cluster() ->
  ?SETUP(fun() -> setup_mocking(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
    begin {H, S, Res} = run_commands(Cmds),
      aggregate(command_names(Cmds),
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end )).
Retrieved from "https://wiki.hh.se/ceres/index.php?title=CirqBuff_and_MBox_QuickCheck_Models&oldid=6518"