This sample includes a very simple model program and an 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