NuSMV

Last updated Apr 12, 2023 Edit Source

What we want to model:

Livelock where we make a choice and cancel:

Deadlock where we make a payment when no choice is made

We want to accept payment only when choice is made. Introduce new variable acc_payment which is TRUE only if expect payment and payment are true. Deadlock because acc_payment can be set to TRUE even when we cancel our choice:

Case statement must be exhaustive:

• The main module instantiates other modules.
• Each module runs in parallel
• Share state using parameters

• Ferryman wants to cross the river with cabbage, goat and wolf
• Goat will eat cabbage if left alone
• Wolf will eat goat if left alone

We can find the solution by negative the property we want to hold, reach the solution while property is false. Model checker can then find a counter example where we reach the solution while property is true:

• Location of A,B,C,D as array of booleans
• Travelling status of ABCD as another array of booleans
• Torch location as boolean
• Time as a number 0-100

• Torch can change location only if someone travels.
• Model that torch always changes location until solution achieved, since we are interested in efficient solutions, and time does not increase if nobody moves.
• Location is updated iff they want to travel and the torch is at their place
• Timekeeping
  • Time advances according to the slowest person who travels
  • Define a time limit which the problem must be solved

running is a property created by the process keyword internally which indicates which process is running.

Process 2 is always selected by this model “scheduler”. This is unfair trace which can be forbidden using the keyword FAIRNESS running;

Process 1 and 2 alternate between each other but process 2 acquires the semaphore each time before process 1 is able to do so.