How can i change these into CTL SPEC in NuSMV mode

Question

I need help writing these CTL. I don't reall understand how to write in NuSMV format yet, hopefully my code will make sense to you since it is incomplete atm.

2)If a process is waiting, it will eventually get to its critical section

3)The two processes must 'take turns' entering the critical section

4)It is possible for one process to get into the critical section twice in succession (before the other process does).

5)Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

6)2 more non-trivial properties of your choice

MODULE thread1(flag2,turn)
VAR
   state : {W0,F1,W1,T1,F2,Wait,F3,C1,T2,F4};
   flag1 : boolean;

ASSIGN
   init(state) := W0;
   next(state) :=
case
   state = W0                 : F1;  
   state = F1                 : W1;  
   state = W1 & flag2         : T1; 
   (state = W1) & !flag2      : C1;  
   (state = T1)&(turn = 2)    : F2;  
   (state = T1)&(turn != 2)   : W1;  
   (state = F2)               : Wait; 
   (state = Wait)&(turn = 1)  : F3;   
   (state = Wait)&(turn != 1) : Wait; 
   (state = F3)               : W1; 
   (state = C1)               : T2; 
   (state = T2)               : F4; 
   (state = F4)               : W0;
    TRUE : state;
esac;

init(flag1) := FALSE;
next(flag1) := 
case
   state = F1 | state = F3 : TRUE;  
   state = F2 | state = F4 : FALSE; 
   TRUE                    : flag1;
esac;

DEFINE
  critical := (state = C1);
  trying := (state = F1 | state = W1 | state = T1 | state = F2 |     state = Wait | state = F3);  

MODULE thread2(flag1,turn)
VAR
   state1 : {N0,N1,N2,N3,N4,Wait1,N5,Critical1,N7,N8};
   flag2 : boolean;

ASSIGN
   init(state1) := N0;
   next(state1) :=
case
   (state1 = N0)               : N1;  
   (state1 = N1)               : N2;  
   (state1 = N2) & flag1       : N3;  
   (state1 = N2) & !flag1      : Critical1;
   (state1 = N3) & (turn = 1)  : N4;  
   (state1 = N3) & (turn != 2) : N2;  
   (state1 = F4)               : Wait1; 
   (state1 = Wait1)&(turn = 2) : N5;   
   (state1 = Wait1)&(turn != 2): Wait1; 
   (state1 = N5)               : N2; 
   (state1 = Critical1)        : N7; 
   (state1 = N7)               : N8;
   (state1 = N8)               : N0;
    TRUE : state1;
esac;

init(flag2) := FALSE;
next(flag2) := 
case
   state1 = N1 | state1 = N5 : TRUE;  
   state1 = N4 | state1 = N8 : FALSE;
   TRUE                    : flag2;
esac;

DEFINE
  critical := (state1 = Critical1);
  trying := (state1 = N1 | state1 = N2 | state1 = N3 | state1 = N4 |     state1 = Wait1 | state1 = N5);  

MODULE main

VAR

turn: {1, 2};
proc1: process thread1(proc2.flag2,turn);
proc2: process thread2(proc1.flag1,turn);

ASSIGN

init(turn) := 1;
next(turn) := 
case
   proc1.state = T2 : 2;
   proc2.state1 = N7 : 1;
   TRUE : turn;
esac;

SPEC 

AG !(proc1.critical & proc2.critical); 
--two processes are never in the critical section at the same time

SPEC 
AG (proc1.trying -> AF proc1.critical);

Answer 1

Note: giving you a comprehensive introduction to CTL in an answer is quite unrealistic. In addition to this quick and dirty course on NuSMV/nuXmv, you might benefit from looking at these slides, which provide a theoretical background on CTL Model Checking.

---

CTL OPERATORS

Assume that for simplicity your program has a unique initial state.

The semantics of the CTL operators is the following:

• AF P: in all possible execution paths, sooner or later P will be true.
• AG P: in all possible execution paths, P is always true.
• AX P: in all possible execution paths, in the next state P is true.

• A[P U Q]: in all possible execution paths, P is true * until Q is true (at least once).

• EF P: in at least one execution path, sooner or later P will be true.

• EG P: in at least one execution path, P is always true.
• EX P: in at least one execution path, in the next state P is true.
• E[P U Q]: in at least one execution path, P is true * until Q is true (at least once).

*: until is true also on a path in which P is never true, provided that Q is immediately verified. [Also, see: weak/strong until]

If you have multiple initial states, then the CTL property holds if it is true for every initial state.

---

Properties:

Note that since your NuSMV model is currently broken and this appears to be a homework, I will provide you with a pseudo-code version of the properties and leave it to you to fit them on your own code.

• if a process is waiting, then it will eventually get to its critical section

  CTLSPEC AG (proc1.waiting -> AF proc1.critical);
  

  explanation: the content of the parenthesis encodes exactly the sentence as you read it. I added AG because the property must clearly hold for every possible state in your model. If you omit it, then the model checker will simply test whether proc1.waiting -> AF proc1.critical is true in your initial state(s).

• the two processes must 'take turns' entering the critical section

  CTLSPEC AG ((proc1.critical -> AX A[!proc1.critical U proc2.critical]) &
             (proc2.critical -> AX A[!proc2.critical U proc1.critical]));
  

  explanation: let me premise that this encoding works because both proc1 and proc2 stay in the critical section for only one state. The idea of proc1.critical -> AX A[!proc1.critical U proc2.critical] is the following: "if process 1 is in the critical section, then starting from the next state process 1 will never be in the critical section (again) until when process 2 is in the critical section".

• It is possible for one process to get into the critical section twice in succession (before the other process does).

  CTLSPEC EF (proc1.critical -> EX A[!proc2.critical U proc1.critical]);
  

  explanation: similar to the previous one. Here I use EF because it suffices the property holds just once.

• Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

  edit: I removed this encoding because on a second thought the formula I wrote is much stronger than required. However, I don't think it's possible to weaken it with the E operator, as it would become much weaker than required. At the time being I can't think of a possible alternative other than modify your model to count the number of cycles, whatever that means.