Assignment: NuSMV tutorial

Introductory NuSMV exercise

The goal of these exercises is to make you familiar with NuSMV.

See the lecture slides Download lecture slides for more information on the exercises. If you like, you can watch the following lecture video that walks you through the example problem (vending machine):

This is an individual exercise; the goal is that everyone masters the basics of NuSMV before continuing in your group with Part 3, Project.

How to upload

You can upload the final .smv file as a text file. Comments can be written in lines starting with --.

Vending machine

Start with vending1.smv. Download vending1.smv.

1. Use NuSMV on vending1.smv .
   1. Study error trace. Copy it as a multi-line comment to the bottom of the model, and add explanations.
      
   2. Refine transition ( case condition). The new model should have no property violations anymore.
      
2. Counting remaining items.
   1. Add a counter n_items (see above).
   2. Write LTL or CTL properties for these three new properties:
      
      1. Number of items should always be $\ge$0.
      2. Payment should only be accepted if number of items > 0.
      3. If an item is dispensed, the counter of items is always reduced by 1.
   3. Ensure your model fulfills all properties.

Upload the commented source file with your solution.