title: 4 in a row with NUSMV
body: <p>I'm trying to create a 4 in a row implementation in NuSMV. Unfortunately I am new to NuSMV and I have difficulty to creating it.
  I have tried to define all the winning cases for player 1 and have used 2D array to represent the grid.
  Now im getting an error from the NUSMV compiler which says:"illegal operand types of "=" : integer and boolean" at the next(move)- block.
  With seq1 to seq6 im defining all the future actions the player can do(e.g. at the beginning of the game the player can put stone only in the first 7 spaces).</p>
  
  <pre><code>MODULE main
  
   VAR
    win_p1 : boolean;
    win_p2 : boolean;
    loss_p1 : boolean;
    loss_p2 : boolean;
    end_game : boolean;
    player1_turn : boolean;
    player2_turn : boolean;
    move : 1..42; --at least 7 turns to win, turn is var which can take values 1 to 42
    seq1:boolean;
    seq2:boolean;
    seq3:boolean;
    seq4:boolean;
    seq5:boolean;
    seq6:boolean;
    p1_strategy:{nan ,perfect,imperfect};
    four_in_a_row: boolean; 
    four_in_a_column: boolean;
    four_in_a_diagonal: boolean;
    occupied_by : array 0..5 of array 0..6 of {free,player1,player2}; --2D array to represent the grid 6X7
  
    --every column as 1D array with 6 elements
    put_in_a : array 0..5 of boolean; -- array of 6 elements for column a
    put_in_b : array 0..5 of boolean; -- array of 6 elements for column b
    put_in_c : array 0..5 of boolean; -- array of 6 elements for column c
    put_in_d : array 0..5 of boolean; -- array of 6 elements for column d
    put_in_e : array 0..5 of boolean; -- array of 6 elements for column e
    put_in_f : array 0..5 of boolean; -- array of 6 elements for column f
    put_in_g : array 0..5 of boolean; -- array of 6 elements for column g
  
  
    ASSIGN
    init(seq1):=FALSE;
    init(seq2):=FALSE;
    init(seq3):=FALSE;
    init(seq4):=FALSE;
    init(seq5):=FALSE;
    init(seq6):=FALSE;
  
    init(win_p1):=FALSE;
    init(win_p2):=FALSE;
    init(loss_p1):=FALSE;
    init(loss_p2):=FALSE;
    init(end_game):=FALSE;
    init(p1_strategy):= {nan};
  
  
      init(occupied_by[0][0]) := {free};
      init(occupied_by[0][1]) := {free}; 
      init(occupied_by[0][2]) := {free}; 
      init(occupied_by[0][3]) := {free}; 
      init(occupied_by[0][4]) := {free}; 
      init(occupied_by[0][5]) := {free}; 
      init(occupied_by[0][6]) := {free};
  
      init(occupied_by[1][0]) := {free}; 
      init(occupied_by[1][1]) := {free}; 
      init(occupied_by[1][2]) := {free}; 
      init(occupied_by[1][3]) := {free};
      init(occupied_by[1][4]) := {free}; 
      init(occupied_by[1][5]) := {free};
      init(occupied_by[1][6]) := {free}; 
  
      init(occupied_by[2][0]) := {free}; 
      init(occupied_by[2][1]) := {free}; 
      init(occupied_by[2][2]) := {free}; 
      init(occupied_by[2][3]) := {free};
      init(occupied_by[2][4]) := {free}; 
      init(occupied_by[2][5]) := {free}; 
      init(occupied_by[2][6]) := {free};
  
      init(occupied_by[3][0]) := {free};
      init(occupied_by[3][1]) := {free}; 
      init(occupied_by[3][2]) := {free}; 
      init(occupied_by[3][3]) := {free}; 
      init(occupied_by[3][4]) := {free}; 
      init(occupied_by[3][5]) := {free};  
      init(occupied_by[3][6]) := {free};
  
      init(occupied_by[4][0]) := {free};
      init(occupied_by[4][1]) := {free};   
      init(occupied_by[4][2]) := {free};   
      init(occupied_by[4][3]) := {free};   
      init(occupied_by[4][4]) := {free};   
      init(occupied_by[4][5]) := {free}; 
      init(occupied_by[4][6]) := {free};
  
      init(occupied_by[5][0]) := {free};
      init(occupied_by[5][1]) := {free};   
      init(occupied_by[5][2]) := {free};   
      init(occupied_by[5][3]) := {free};   
      init(occupied_by[5][4]) := {free};   
      init(occupied_by[5][5]) := {free};   
      init(occupied_by[5][6]) := {free};
  
  
    init(player1_turn):=TRUE;
    init(player2_turn):=FALSE;
    init(move):=1;
    init(four_in_a_column):= FALSE;
    init(four_in_a_row):= FALSE; 
    init(four_in_a_diagonal):= FALSE;
  
    next(seq1) := case --7 initial cases
    seq1 = (put_in_a[0] = TRUE): occupied_by[0][0] ={player1}; 
    seq1 = (put_in_b[0] = TRUE): occupied_by[0][1] ={player1};
    seq1 = (put_in_c[0] = TRUE): occupied_by[0][2] ={player1};  
    seq1 = (put_in_d[0] = TRUE): occupied_by[0][3] ={player1};
    seq1 = (put_in_e[0] = TRUE): occupied_by[0][4] ={player1};
    seq1 = (put_in_f[0] = TRUE): occupied_by[0][5] ={player1};
    seq1 = (put_in_g[0] = TRUE): occupied_by[0][6] ={player1};
    TRUE: seq1;
    esac;
  
    next(seq2) := case -- 14 cases
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
    seq2 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
    TRUE: seq2;
    esac;  
  
    next(seq3) := case --21 cases
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
    seq3 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
    TRUE: seq3;
    esac;
  
    next(seq4) := case --28 cases
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
    seq4 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
    TRUE: seq4;
    esac;
  
    next(seq5) := case --35 cases
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[4] = TRUE) : occupied_by[4][0] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[4] = TRUE) : occupied_by[4][1] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[4] = TRUE) : occupied_by[4][2] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[4] = TRUE) : occupied_by[4][3] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[4] = TRUE) : occupied_by[4][4] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[4] = TRUE) : occupied_by[4][5] ={player1};
    seq5 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[4] = TRUE) : occupied_by[4][6] ={player1};
    TRUE: seq5;
    esac;
  
    next(seq6) := case --42 cases
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[4] = TRUE) : occupied_by[4][0] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[4] = TRUE) : occupied_by[4][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[4] = TRUE) : occupied_by[4][2] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[4] = TRUE) : occupied_by[4][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[4] = TRUE) : occupied_by[4][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[4] = TRUE) : occupied_by[4][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[4] = TRUE) : occupied_by[4][6] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_a[5] = TRUE) : occupied_by[5][0] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_b[5] = TRUE) : occupied_by[5][1] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_c[5] = TRUE) : occupied_by[5][2] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_d[5] = TRUE) : occupied_by[5][3] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_e[5] = TRUE) : occupied_by[5][4] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_f[5] = TRUE) : occupied_by[5][5] ={player1};
    seq6 = (player1_turn = TRUE) &amp; (player2_turn)=FALSE &amp; (put_in_g[5] = TRUE) : occupied_by[5][6] ={player1};
    TRUE: seq6;  
    esac;
  
    next(player2_turn) := case
    player2_turn = (player1_turn = FALSE) : (player2_turn)=TRUE;
    TRUE: player2_turn;  
    esac;
  
    next(move) := case
    move = (put_in_a[0] = TRUE): move+1;
    move = (put_in_a[1] = TRUE): move+1;
    move = (put_in_a[2] = TRUE): move+1;
    move = (put_in_a[3] = TRUE): move+1;
    move = (put_in_a[4] = TRUE): move+1;
    move = (put_in_a[5] = TRUE): move+1;
    move = (put_in_b[0] = TRUE): move+1;
    move = (put_in_b[1] = TRUE): move+1;
    move = (put_in_b[2] = TRUE): move+1;
    move = (put_in_b[3] = TRUE): move+1;
    move = (put_in_b[4] = TRUE): move+1;
    move = (put_in_b[5] = TRUE): move+1;
    move = (put_in_c[0] = TRUE): move+1;
    move = (put_in_c[1] = TRUE): move+1;
    move = (put_in_c[2] = TRUE): move+1;
    move = (put_in_c[3] = TRUE): move+1;
    move = (put_in_c[4] = TRUE): move+1;
    move = (put_in_c[5] = TRUE): move+1;
    move = (put_in_d[0] = TRUE): move+1;
    move = (put_in_d[1] = TRUE): move+1;
    move = (put_in_d[2] = TRUE): move+1;
    move = (put_in_d[3] = TRUE): move+1;
    move = (put_in_d[4] = TRUE): move+1;
    move = (put_in_d[5] = TRUE): move+1;
    move = (put_in_e[0] = TRUE): move+1;
    move = (put_in_e[1] = TRUE): move+1;
    move = (put_in_e[2] = TRUE): move+1;
    move = (put_in_e[3] = TRUE): move+1;
    move = (put_in_e[4] = TRUE): move+1;
    move = (put_in_e[5] = TRUE): move+1;  
    move = (put_in_f[0] = TRUE): move+1;
    move = (put_in_f[1] = TRUE): move+1;
    move = (put_in_f[2] = TRUE): move+1;
    move = (put_in_f[3] = TRUE): move+1;
    move = (put_in_f[4] = TRUE): move+1;
    move = (put_in_f[5] = TRUE): move+1;
    move = (put_in_g[0] = TRUE): move+1;
    move = (put_in_g[1] = TRUE): move+1;
    move = (put_in_g[2] = TRUE): move+1;
    move = (put_in_g[3] = TRUE): move+1;
    move = (put_in_g[4] = TRUE): move+1;
    move = (put_in_g[5] = TRUE): move+1;
    TRUE: move;  
    esac;
  </code></pre>