• kth.se
  • Studentwebben
  • Intranät
  • kth.se
  • Studentwebben
  • Intranät
Logga in
DD2460 VT21 (60553)
NuSMV tutorials
Hoppa över till innehåll
Översikt
  • Logga in
  • Översikt
  • Kalender
  • Inkorg
  • Historik
  • Hjälp
Stäng
  • Min översikt
  • DD2460 VT21 (60553)
  • Uppgifter
  • NuSMV tutorials
  • Startsida
  • Uppgifter
  • Quiz
  • Moduler
  • Media Gallery
  • Course Evaluation

NuSMV tutorials

  • Inlämningsdatum 30 apr 2021 av 23.59
  • Poäng 1
  • Lämnar in en textimatningsruta, en länk till webbplats, eller en filuppladdning

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 ≥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

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.

1619819940 04/30/2021 11:59pm
Inkludera en beskrivning
Ytterligare kommentarer:
Maxresultat för gradering till > poäng
Inkludera en bedömningstitel

Matris

Hitta matris
Inkludera en titel
Hitta en matris
Titel
Du har redan bedömt studenter med den här matrisen. Större ändringar kan påverka resultaten för deras uppgifter.
 
 
 
 
 
 
 
     
Det går inte att ändra en matris efter att du börjat använda den.  
Titel
Kriterier Bedömningar Poäng
Det här kriteriet är länkat till ett lärandemål Beskrivning av kriterium
tröskel: 5 poäng
Redigera beskrivning av kriterium Ta bort kriterium rad
5 till >0 poäng Full poäng blank
0 till >0 poäng Inga poäng blank_2
Det här området kommer användas av utvärderaren för kommentarer relaterade till det här kriteriet.
poäng
  / 5 poäng
--
Ytterligare kommentarer
Det här kriteriet är länkat till ett lärandemål Beskrivning av kriterium
tröskel: 5 poäng
Redigera beskrivning av kriterium Ta bort kriterium rad
5 till >0 poäng Full poäng blank
0 till >0 poäng Inga poäng blank_2
Det här området kommer användas av utvärderaren för kommentarer relaterade till det här kriteriet.
poäng
  / 5 poäng
--
Ytterligare kommentarer
Poängsumma: 5 av 5
Föregående
Nästa
Quiz on "The SLAM Toolkit" Advanced NuSMV exercise