modellogicmodel-checkingctlnusmv

How can i change these into CTL SPEC in NuSMV model?

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);
Solution

  • 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:

    *: 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.

    CTL operators

    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.