combines two or more separate
into a new model program called the product
. Compose a contract model program with a scenario to achieve scenario control for testing, or to check a temporal property during analysis. Compose two or more contract model programs to
build up complex models in a well-structured way.
The NModel tools
, compose all of the model programs entered as options on the command line. Any combination of C# model programs and finite state machines (FSMs) can be composed.
Composition synchronizes on shared actions and interleaves unshared actions. Here is an example. Consider the C# model program on
, compiled in PowerSwitch.dll
. This program can be visualized alone by
mpv /r:PowerSwitch.dll PowerSwitch.Contract.Create
Let us compose this program with the following finite state machine (FSM), in a file called
Transitions(t(Low(), IncrementSpeed(), Medium()),
t(Medium(), IncrementSpeed(), High()),
t(High(), IncrementSpeed(), Low())))
You can view this FSM alone, by mpv /fsm:SpeedControl.txt
To compose these two programs, use
mpv /r:PowerSwitch.dll /fsm:SpeedControl.txt PowerSwitch.Contract.Create
Here there are no shared actions, so all the unshared actions interleave, and the product is larger (has more states and transitions) than the programs that were composed. When actions are shared, the product is smaller; the set of traces of the product is
the intersection of the sets of traces of the composed programs. In that case, composition has the effect of selecting some runs of interest, so it is useful for scenario control and property checking.
Composition of model programs is a generalization of the construction of finite automata for the intersection of regular languages. For example, see the discussion following Theorem 3.3 on pp. 59 -- 60 of Hopcroft and Ullman, 1979 edition.