CIF 3

Exercise 2: a simple requirement changeΒΆ

For this exercise you’ll again be using the Button/Lamp example from the previous exercise. However, this time you will specify your own requirements.

The goal is now to specify different requirements, to force different behavior. The first time the button is pushed, we want the lamp to go on. Releasing the button should have no effect on the lamp. The second time we push the button, the lamp should go off. This repeats itself. In other words, each button push inverts the status of the lamp.

Change your model (file #_plants_reqs1.eventbased.cif or #_plants_reqs1.statebased.cif, where # is to be replaced by the name of the workstation you’re using) to reflect the new requirements. We recommend making an event-based requirement. Change only the requirement automaton, not the plants. Your physical hardware has not changed, so there is no need to change the plant automata, only the desired behavior has changed.

Try to keep your requirement simple, by leaving out all irrelevant details, and keeping it as small as possible. Once you are convinced you have the correct requirement, synthesize a supervisor, and simulate it. If you need help with modeling, the toolchain, or you run into problems while synthesizing the supervisor, see the Toolchain page for more information.

If you follow the 4K420 course, make sure you discuss your requirements and resulting supervisor with the teachers, before you continue.