Modeling with PyModel

Models
Model program
Model program configuration
Finite State Machine (FSM)
Test suite


Models

To describe models and control their execution, you can write three
kinds of modules: model programs, finite state machines (FSMs), and
test suites (yes, a test suite can also serve as a model).  You can
name any number of these modules as arguments on the command line for
any of the commands.  The command imports them all, composes their
contents into a product, and then uses the product to generate or run
tests, or perform analyses.


Model Program

Purpose: Describe the behavior of "infinite" systems (whose action
arguments belong to types that can take on an "infinite" number of
values, such as numbers, strings, or collections.)

Examples: Marquee/Marquee.py, PowerSwitch/PowerSwitch.py, Stack/Stack.py,
WebApplication/WebModel.py, Socket/Socket.py, populations/populations.py

Summary: Describes a collection state variables, action functions that
may update the state variables, and enabling conditions that describe
when each action is allowed to occur.  Enabling conditions are Boolean
functions on state variables and action arguments; they cannot update
the state.  An action without enabling conditions is always enabled.

The state variables, actions, and enabling conditions are the core of
a model program.  A model program also requires additional information
(metadata) that describes how the model program should be processed
by the analyzer and tester.  Provide this information by assigning
particular required and optional attributes in the model program (see
below).

Restrictions: Action function arguments must be hashable.  Therefore,
if these arguments are collections, they must be tuples but not lists
or dictionaries.  State variables should have values that are
meaningful to test for equality with ==.  Therefore, state variables
can be collections (including lists and dictionaries) but (usually)
should not be instances.

Model program, required attributes:

state: sequence (tuple or list) of strings, the names of the state
variables

actions: the action vocabulary, a sequence of action functions
(identifiers not strings)

Model program, optional attributes:

enablers: dictionary, associates each action function with a sequence of
enabling condition functions.  All of these enabling conditions must
be true to enable the action.  At this time there can be only one
enabling conditon in the sequence.  An action which is not in the
dictionary is always enabled.  Some samples use the naming convention
where action Foo has enabling condition FooEnabled but this is not
required.  The default is the empty dictionary, all actions are
enabled in all states

cleanup: sequence (list or tuple) of cleanup actions that make
progress to an accepting state.  The default is the empty tuple, no
cleanup actions

domains: dictionary, associates each action function with a dictionary
that associates each action argument name (string) with a list of
argument values.  The default is the empty dictionary with empty
domains.  This is an error if actions have arguments.

The list of action argument values may appear explicitly the in
domain, or the argument name may be associated with a callable (for
example a lambda expression or a function) that is evaluated at run
time (each time the action is used) to return a collection of argument
values.  This function can use the model state, so the arguments can
depend on the state.  See populations/populations.py and
populations/test/domains9.py for examples of state-dependent domains.
State-dependent domains *must* be callables (as in populations.py or 
domains9.py) to force them be re-evaluated each time they are used.
Just naming the collection variable (as in populations/test/domainsx.py)
does *not* work.

combinations: dictionary, associates each action function with 'all'
(to form argument lists from the Cartesian product of all the domains)
or 'cases' (to form the i'th argument list from the i'th item in each
domain).  If an action is missing from the dictionary, use 'all'.  The
default is the empty dictionary, all argument lists use 'all',
Cartesian product

accepting (or Accepting): Boolean function of state variables that
returns True when the state is an accepting state where a run is
allowed to stop.  The default always returns True, so all states are
accepting states.

statefilter (or state_filter or StateFilter): Boolean function of
state variables that returns True when the state should be added to
the FSM generated by exploration (in the pma program).  The default
always returns True, so all states are added to the FSM.

stateinvariant (or state_invariant or StateInvariant): Boolean
function of state variables that expresses safety requirements.  It is
usually intended that stateinvariant should return True in every
state.  States where stateinvariant returns False are unsafe states,
and usually indicate design errors that permit unintended behaviors.

reset (or Reset): function with no arguments that restores initial
state, so the model can execute multiple runs in a single pmt session.
There is no default; if the model program does not define a Reset
function and the pmt command line calls for multiple runs, it is an
error.

observables: sequence of action functions (identifiers not strings),
the observable actions in the model program.  An observable action
does not obtain its argument values from the model program's domains
(above).  Instead, it obtains its argument values (if any) from
actions with the same names in scenario machines (FSMs or TestSuites)
with which the model program is composed, even if a domain for that
action is provided in the model program.  If no scenario machines are
composed, or they do not provide argument values, then the observable
action is not enabled; it never executes.  Actions which are not
observables are controllable actions.  Controllable actions always
obtain their argument values from the model program's domains.

Observable actions support "passive testing": automatically checking
log files (or other traces collected from instrumented systems)
against a model.  To perform passive testing, designate all the
actions in the trace to be observable actions.  Express the trace (or
traces) as a PyModel TestSuite, then compose the model with that
TestSuite.  Runs in the product that do not reach an accepting state
are test failures.


Model Program configuration

Purpose: Bind or rebind attributes in a model program module.  This
makes it possible to run pma or pmt with different combinations of
domains (for example) without rewriting the model program module, just
by using different command line arguments (that name different
configuration modules).  Argument order doesn't matter; the
configuration module can precede or follow its model program module in
the argument list.

Examples: Marquee/DisplayFive.py (rebinds both actions and domains,
used in test_graphics script), Socket/SocketSendA.py and SendAll.py
(rebind domains and enabling conditions, respectively, both used in
test_graphics script), WebApplication/OneUserDomain.py and
OneUserFilter.py (mutates a list used in domains and rebinds
StateFilter, respectively, both used in test_graphics script),
Stack/Observables.py and AllObservables.py (binds observables,
used in the test_scenarios and test_scenario_graphics scripts),
populations/filter3 (binds statefilter, used in test_filter script).

Required attributes: A configuration module must contain a docstring
(the module's __doc__attribute, the first literal string in the
module) that begins with 'pymodel config'.  This 'pymodel config' is
case insensitive (it may be capitalzed or not) and may be preceded by
blanks in the docstring.  


Finite State Machine (FSM)

Purposes:

1. Describe the behavior of finite systems (whose action arguments
belong to types that can take on an only a finite number of values)

Example:  ABP/ABP.py

2. Restrict behavior of a model program by composition

Examples: Stack/StackOneScenario.py, Socket/NoBlockScenario.py,
WebApplication/ScenarioLoginRepeat.py, OneUserScenario.py,
OneUserNoIntScenario.py

3. Written by the pma program to save exploration results for graphics,
analysis etc.

Examples: *FSM.py modules in samples.

FSM required attributes:

initial: the initial state (integer)

accepting: sequence (list or tuple) of accepting states (integers)
where traces are allowed to stop.

graph: the graph of the finite state machine, a sequence of sequences,
where each sequence is a transition tuple: (current state, (action,
sequence of argument values, return value), next state).  States are
integers.  Actions are identifiers, usually imported from another
module (the model program whose behavior is to be restricted, for
example).  Each action must have a __name__ attribute.  The seqeuence
of arguments may be empty but it must be present.  Each argument value
must be hashable.  The return value may be None but it must be
present.

FSM optional attributes: 

actions: action vocabulary, sequence of action methods.  The default
is the sequence of actions that occur as current states and next
states in the graph.

cleanup: sequence (list or tuple) of cleanup actions that make
progress to an accepting state.


Test Suite

Purposes:

1. Offline test suite created by hand (sort of like a hand-written
unit test)

Examples: WebApplication/TestIntFailure.py, TestIntSuccess.py.

2. Allowed or forbidden trace(s) used to validate a model program

Examples: ABP/Scenarios.py, PowerSwitch/Scenarios.py,
Stack/Scenarios.py, WebApplication/TestIntSuccess.py, TestIntWrong.py

3. Written by the pmt program to save traces in an offline test suite,
or to record an on-the-fly test session to reproduce later.

Examples:  *Test.py modules in samples

Required attributes:

testsuite (or test_suite or testSuite): sequence of sequences, each
nested sequence is a single run that starts in the initial state.  pmt
attempts to execute all the runs in the test suite, but pmt exits when
a run experiences a conformance failure.  Each run is a sequence of
actions, consisting of a tuple of three items: action identifier,
sequence of action arguments (may be empty but must be present),
action return value (may be None but must be present).  The action
identifier must be a symbol with a __name__ attribute.  The sequence
of arguments is itself a tuple.  Each action must be a tuple (not a
list) because it must be hashable (so each action argument must also
be hashable).


Revised May 2012