NuSMV tutorial

Introductory NuSMV exercises

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

See the lecture slides for more information on the exercises.

How to upload

Unfortunately, Canvas does not allow more than one file upload at once. You can upload the files one by one, but you can also upload an archive:

1. as an archive (e.g., .tar.gz);
2. as a URL to a publicly accessible shared folder (Google Drive, Dropbox, KTH Box, etc.);
3. as a text file that contains a URL pointing to each part of the solution.

Peer reviews

Peer reviews are optional. You can get in touch with another group if you would like their opinion or advice on your model and if you offer to do the same for them.

It is a bit difficult to conduct peer reviews remotely, so you can also ask teaching assistants instead during the lab sessions.

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.

Bridge crossing

Files:

• ferryman.smv Download ferryman.smv (for reference)
• bridge-torch.smv Download bridge-torch.smv (skeleton; edit this file)

1. Develop the full game model and the formula to find the solution.
2. Study the resulting trace(s) and show the optimal solution. Add the trace with an explanation, or another form of depicting the optimal solution, at the bottom as a comment.
   

Upload the commented source; add the trace and explanation as a comment at the bottom.

Semaphore/processes (optional)

Start with semaphore.smv Download semaphore.smv, and convert it to a model that does not use SMV processes. Use the guidance from the lecture slides.

Strengthen the fairness condition(s) to avoid a livelock.

Upload the commented model code. At the bottom, include a failed trace where fairness is not enabled, and briefly explain the resulting problem.