| Overview |  |
Copyright © Quviq AB, 2012-2023
Version: 1.46.3
This module defines a parse transformation to enable the precondition, postcondition, and so on, of each command in a QuickCheck state machine to be specified together.
This parse transformation is used with QuickCheck state machines to enable specifications to be written in a different style, the "grouped" style. This may result in shorter, more readable specifications in certain cases. However, one should be warned that the parse transformation may cause some difficulty in debugging such specifications, because the compiled code no longer corresponds exactly to the source code.
What the parse transformation does is to offer a new set of call-back functions to define QuickCheck state machines with. This parse transformation is automatically invoked by eqc_statem.hrl, and recognizes a grouped specification by the absence of a command/1 function in the module, or by the optional user annotation -eqc_group_commands(true).
Note that you cannot mix the old call-back functions with the new call-back functions. Either you use the grouped style, or you use the call-backs as defined in the original QuickCheck state machine descriptions.
In the ungrouped style, an eqc_statem specification defines a number of callbacks, command, precondition, postcondition, etc, in which all generated commands are handled. In the default grouped style, each command is specified by a number of functions, which can be grouped together, that represent generation, precondition, postcondition, etc. These functions are named by appending a suffix to the name of the command itself. Apart from the COMMAND_args call-back, each of these call-backs is optional, and if not provided a default is used.
In addition to the suffixes defined for eqc_statem, a component command may
also use any of the additional suffixes _callouts and _callers.
COMMAND_callers() :: [atom()]
Returns a list of allowed callers for the COMMAND. This information is only used when the component is part of a cluster. If there are no restrictions for the command, [anyone] (the default) can be used. If used in a cluster, during command generation, this command is excluded from generation unless there is at least one caller in the list of callers that is not in the cluster!
default: [anyone]
COMMAND_callouts(S::symbolic_state(), Args::[term()]) :: eqc_component:callout()
Returns a callout specification for the given symbolic state and the given command
arguments. See eqc_component for details.
In the ungrouped style, an eqc_fsm specification defines a number of callbacks, command, precondition, postcondition, etc, in which all generated commands are handled. In the grouped style, each command is specified by a number of functions, which can be grouped together, that represent generation, precondition, postcondition, etc. These functions are named by appending a suffix to the name of the command itself. Apart from the COMMAND_args callback, each of these callbacks is optional, and if not provided a default is used.
Note that the state transition function is specified differently for grouped style eqc_fsm specifications. The state names are still represented as atoms, or tuples for parameterized states, but the transitions no longer are a list with state names and call tuples, but with state names and transition function atoms instead. This also implies that one no longer provides the state data as argument of the transition function. As an example, in the ungrouped style we would write a state transition like:
unlocked(S) ->
[{unlocked,{call,locker,read,[]}},
{locked, {call,locker,lock,[]}}].
In grouped style, we would instead write:
unlocked() ->
[{unlocked,read},
{locked, lock}].From the name of the functions read and lock the grouped eqc_fsm can derive that the functions read_args and write_args whould be invoked to obtain the state data generators.
Generated by EDoc