Composition combines two or more separate model programs 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 mpv, otg, and ct, 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 this page, 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 SpeedControl.txt:

FSM(Low(), AcceptingStates(Low()), 
  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.