4.1 Tutorial

The objective of this chapter is to get you to a stage where you can use BMotionWeb to visualize Event-B or Classical-B models. We expect that you have already downloaded the BMotionWeb tool (see Section 2.1).

You should be able to work through the tutorial with no or little outside help. We encourage you not to download solutions to the examples but instead to actively build them up yourself as the tutorial progresses. If something is unclear, remember to check the Reference (4.2) for more information.