PowerSwitch

This sample includes a very simple model program and FSM, for an

on-off power switch and a speed control.

This sample demonstrates several PyModel techniques (including

composition) on a minimal example.

- *PowerSwitch*: model program for on-off power switch

- *test*: execute *PowerSwitch*, demonstrate *pmt* options *-n* *-c* *-a* *-e* *-r*

- *Scenarios*: test suite with several traces of power switch

behavior, some allowed by the model program, others not allowed

- *SpeedControl*: FSM for speed control

- *test_scenarios*: execute *PowerSwitch*, *Scenarios*, and

*SpeedControl*, alone and composed. *PowerSwitch* composed with

*Scenarios* shows how forbidden traces end in non-accepting states.

*PowerSwitch* composed with *SpeedControl* shows how unshared actions

interleave.

- *test_graphics*: generate graphs of *PowerSwitch*, *SpeedControl*, and

their composition.

- *test_viewer*: Generate the same output as *test_graphics*, but this

script is shorter because it uses *pmv* instead of *pma* + *pmg* +

*dot*

- *fsmpy*, *svg*, *ps*, *pdf*: directories of output files from *test_graphics*

or *test_viewer*, and other graphics generated ad-lib at the command line

You can view the generated graphics files in a browser. Hover the

pointer over any state bubble to see a tooltip that shows the state

variables in that state.

- *PowerSwitchFSM*: the graph of the FSM generated by exploring the *PowerSwitch*

model program

- *SpeedControl*: the graph of the *SpeedControl* FSM

- *PowerSpeed*: the graph of the composition of *PowerSwitch* and

*SpeedControl*, showing how states combine and actions interleave

There is no stepper in this sample.

Revised Mar 2013