4 по счету с НУСМВ

Я пытаюсь создать реализацию 4 в ряд в NuSMV. К сожалению, я новичок в NuSMV, и мне трудно его создать. Я попытался определить все случаи выигрыша для игрока 1 и использовал 2D-массив для представления сетки. Теперь я получаю сообщение об ошибке от компилятора NUSMV, в котором говорится: «недопустимые типы операндов «=»: целое и логическое» в следующем блоке (перемещение). С seq1 по seq6 я определяю все будущие действия, которые может выполнить игрок (например, в начале игры игрок может класть камень только в первые 7 ячеек).

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) & (player2_turn)=FALSE & (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
  seq2 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
  TRUE: seq2;
  esac;  

  next(seq3) := case --21 cases
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
  seq3 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
  TRUE: seq3;
  esac;

  next(seq4) := case --28 cases
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
  seq4 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
  TRUE: seq4;
  esac;

  next(seq5) := case --35 cases
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[4] = TRUE) : occupied_by[4][0] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[4] = TRUE) : occupied_by[4][1] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[4] = TRUE) : occupied_by[4][2] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[4] = TRUE) : occupied_by[4][3] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[4] = TRUE) : occupied_by[4][4] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[4] = TRUE) : occupied_by[4][5] ={player1};
  seq5 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[4] = TRUE) : occupied_by[4][6] ={player1};
  TRUE: seq5;
  esac;

  next(seq6) := case --42 cases
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[0] = TRUE) : occupied_by[0][0] ={player1}; 
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[0] = TRUE) : occupied_by[0][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[0] = TRUE) : occupied_by[0][2] ={player1};  
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[0] = TRUE) : occupied_by[0][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[0] = TRUE) : occupied_by[0][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[0] = TRUE) : occupied_by[0][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[0] = TRUE) : occupied_by[0][6] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[1] = TRUE) : occupied_by[1][0] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[1] = TRUE) : occupied_by[1][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[1] = TRUE) : occupied_by[1][2] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[1] = TRUE) : occupied_by[1][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[1] = TRUE) : occupied_by[1][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[1] = TRUE) : occupied_by[1][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[1] = TRUE) : occupied_by[1][6] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[2] = TRUE) : occupied_by[2][0] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[2] = TRUE) : occupied_by[2][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[2] = TRUE) : occupied_by[2][2] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[2] = TRUE) : occupied_by[2][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[2] = TRUE) : occupied_by[2][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[2] = TRUE) : occupied_by[2][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[2] = TRUE) : occupied_by[2][6] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[3] = TRUE) : occupied_by[3][0] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[3] = TRUE) : occupied_by[3][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[3] = TRUE) : occupied_by[3][2] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[3] = TRUE) : occupied_by[3][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[3] = TRUE) : occupied_by[3][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[3] = TRUE) : occupied_by[3][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[3] = TRUE) : occupied_by[3][6] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[4] = TRUE) : occupied_by[4][0] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[4] = TRUE) : occupied_by[4][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[4] = TRUE) : occupied_by[4][2] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[4] = TRUE) : occupied_by[4][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[4] = TRUE) : occupied_by[4][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[4] = TRUE) : occupied_by[4][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_g[4] = TRUE) : occupied_by[4][6] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_a[5] = TRUE) : occupied_by[5][0] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_b[5] = TRUE) : occupied_by[5][1] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_c[5] = TRUE) : occupied_by[5][2] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_d[5] = TRUE) : occupied_by[5][3] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_e[5] = TRUE) : occupied_by[5][4] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (put_in_f[5] = TRUE) : occupied_by[5][5] ={player1};
  seq6 = (player1_turn = TRUE) & (player2_turn)=FALSE & (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;

georgi georgiev 26.11.2019 источник

Ответы (1)

arrow_upward
0
arrow_downward

Этот:

next(seq2) := case
    seq2 = (player1_turn = TRUE) : ...
esac;

не является синтаксически правильным. Что вы, вероятно, хотите сделать, это:

next(seq2) := case
    (player1_turn = TRUE) : ...
esac;

четыре в ряд.

Вот моя попытка решить проблему, в качестве ссылки.

MODULE cell(under_state, input)
VAR
    state  : { FREE, PLAYER01, PLAYER02 };

ASSIGN
    init(state) := FREE;

    next(state) := case
        state = FREE & input = PLAYER01 & under_state != FREE : PLAYER01;
        state = FREE & input = PLAYER02 & under_state != FREE : PLAYER02;
        TRUE                                                  : state;
    esac;

DEFINE
    output := case
        under_state = FREE : input;
        TRUE               : FREE;
    esac;

MODULE check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i1, i2, i3, i4)
DEFINE
    win := i1 = i2 & i2 = i3 & i3 = i4 & i1 != FREE;
    winner := case
        win  : i1;
        TRUE : FREE;
    esac;

MODULE check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(i0, i1, i2, i3, i4, i5, i6)
VAR
    check_at_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i0, i1, i2, i3);
    check_at_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i1, i2, i3, i4);
    check_at_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i2, i3, i4, i5);
    check_at_3 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i3, i4, i5, i6);
DEFINE
    win    := check_at_0.win | check_at_1.win | check_at_2.win | check_at_3.win;
    winner := case
        check_at_0.win : check_at_0.winner;
        check_at_1.win : check_at_1.winner;
        check_at_2.win : check_at_2.winner;
        check_at_3.win : check_at_3.winner;
        TRUE           : FREE;
    esac;

MODULE check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(i0, i1, i2, i3, i4, i5)
VAR
    check_at_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i0, i1, i2, i3);
    check_at_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i1, i2, i3, i4);
    check_at_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(i2, i3, i4, i5);
DEFINE
    win    := check_at_0.win | check_at_1.win | check_at_2.win;
    winner := case
        check_at_0.win : check_at_0.winner;
        check_at_1.win : check_at_1.winner;
        check_at_2.win : check_at_2.winner;
        TRUE           : FREE;
    esac;

MODULE board(inputs)
VAR
    -- NOTE: PLAYER01 is a dummy value to indicate that
    --       the under_cell is not FREE
    cell_r0_c0 : cell(PLAYER01, cell_r1_c0.output);
    cell_r0_c1 : cell(PLAYER01, cell_r1_c1.output);
    cell_r0_c2 : cell(PLAYER01, cell_r1_c2.output);
    cell_r0_c3 : cell(PLAYER01, cell_r1_c3.output);
    cell_r0_c4 : cell(PLAYER01, cell_r1_c4.output);
    cell_r0_c5 : cell(PLAYER01, cell_r1_c5.output);
    cell_r0_c6 : cell(PLAYER01, cell_r1_c6.output);

    cell_r1_c0 : cell(cell_r0_c0.state, cell_r2_c0.output);
    cell_r1_c1 : cell(cell_r0_c1.state, cell_r2_c1.output);
    cell_r1_c2 : cell(cell_r0_c2.state, cell_r2_c2.output);
    cell_r1_c3 : cell(cell_r0_c3.state, cell_r2_c3.output);
    cell_r1_c4 : cell(cell_r0_c4.state, cell_r2_c4.output);
    cell_r1_c5 : cell(cell_r0_c5.state, cell_r2_c5.output);
    cell_r1_c6 : cell(cell_r0_c6.state, cell_r2_c6.output);

    cell_r2_c0 : cell(cell_r1_c0.state, cell_r3_c0.output);
    cell_r2_c1 : cell(cell_r1_c1.state, cell_r3_c1.output);
    cell_r2_c2 : cell(cell_r1_c2.state, cell_r3_c2.output);
    cell_r2_c3 : cell(cell_r1_c3.state, cell_r3_c3.output);
    cell_r2_c4 : cell(cell_r1_c4.state, cell_r3_c4.output);
    cell_r2_c5 : cell(cell_r1_c5.state, cell_r3_c5.output);
    cell_r2_c6 : cell(cell_r1_c6.state, cell_r3_c6.output);

    cell_r3_c0 : cell(cell_r2_c0.state, cell_r4_c0.output);
    cell_r3_c1 : cell(cell_r2_c1.state, cell_r4_c1.output);
    cell_r3_c2 : cell(cell_r2_c2.state, cell_r4_c2.output);
    cell_r3_c3 : cell(cell_r2_c3.state, cell_r4_c3.output);
    cell_r3_c4 : cell(cell_r2_c4.state, cell_r4_c4.output);
    cell_r3_c5 : cell(cell_r2_c5.state, cell_r4_c5.output);
    cell_r3_c6 : cell(cell_r2_c6.state, cell_r4_c6.output);

    cell_r4_c0 : cell(cell_r3_c0.state, cell_r5_c0.output);
    cell_r4_c1 : cell(cell_r3_c1.state, cell_r5_c1.output);
    cell_r4_c2 : cell(cell_r3_c2.state, cell_r5_c2.output);
    cell_r4_c3 : cell(cell_r3_c3.state, cell_r5_c3.output);
    cell_r4_c4 : cell(cell_r3_c4.state, cell_r5_c4.output);
    cell_r4_c5 : cell(cell_r3_c5.state, cell_r5_c5.output);
    cell_r4_c6 : cell(cell_r3_c6.state, cell_r5_c6.output);

    cell_r5_c0 : cell(cell_r4_c0.state, inputs[0]);
    cell_r5_c1 : cell(cell_r4_c1.state, inputs[1]);
    cell_r5_c2 : cell(cell_r4_c2.state, inputs[2]);
    cell_r5_c3 : cell(cell_r4_c3.state, inputs[3]);
    cell_r5_c4 : cell(cell_r4_c4.state, inputs[4]);
    cell_r5_c5 : cell(cell_r4_c5.state, inputs[5]);
    cell_r5_c6 : cell(cell_r4_c6.state, inputs[6]);

-- prevent invalid move when column full
INVAR inputs[0] != FREE -> cell_r5_c0.state = FREE;
INVAR inputs[1] != FREE -> cell_r5_c1.state = FREE;
INVAR inputs[2] != FREE -> cell_r5_c2.state = FREE;
INVAR inputs[3] != FREE -> cell_r5_c3.state = FREE;
INVAR inputs[4] != FREE -> cell_r5_c4.state = FREE;
INVAR inputs[5] != FREE -> cell_r5_c5.state = FREE;
INVAR inputs[6] != FREE -> cell_r5_c6.state = FREE;

-- evaluate victory/draw conditions
VAR
    check_row_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r0_c0.state,
                                 cell_r0_c1.state,
                                 cell_r0_c2.state,
                                 cell_r0_c3.state,
                                 cell_r0_c4.state,
                                 cell_r0_c5.state,
                                 cell_r0_c6.state);
    check_row_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r1_c0.state,
                                 cell_r1_c1.state,
                                 cell_r1_c2.state,
                                 cell_r1_c3.state,
                                 cell_r1_c4.state,
                                 cell_r1_c5.state,
                                 cell_r1_c6.state);
    check_row_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r2_c0.state,
                                 cell_r2_c1.state,
                                 cell_r2_c2.state,
                                 cell_r2_c3.state,
                                 cell_r2_c4.state,
                                 cell_r2_c5.state,
                                 cell_r2_c6.state);
    check_row_3 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r3_c0.state,
                                 cell_r3_c1.state,
                                 cell_r3_c2.state,
                                 cell_r3_c3.state,
                                 cell_r3_c4.state,
                                 cell_r3_c5.state,
                                 cell_r3_c6.state);
    check_row_4 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r4_c0.state,
                                 cell_r4_c1.state,
                                 cell_r4_c2.state,
                                 cell_r4_c3.state,
                                 cell_r4_c4.state,
                                 cell_r4_c5.state,
                                 cell_r4_c6.state);
    check_row_5 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_7(cell_r5_c0.state,
                                 cell_r5_c1.state,
                                 cell_r5_c2.state,
                                 cell_r5_c3.state,
                                 cell_r5_c4.state,
                                 cell_r5_c5.state,
                                 cell_r5_c6.state);
    check_col_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c0.state,
                                 cell_r1_c0.state,
                                 cell_r2_c0.state,
                                 cell_r3_c0.state,
                                 cell_r4_c0.state,
                                 cell_r5_c0.state);
    check_col_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c1.state,
                                 cell_r1_c1.state,
                                 cell_r2_c1.state,
                                 cell_r3_c1.state,
                                 cell_r4_c1.state,
                                 cell_r5_c1.state);
    check_col_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c2.state,
                                 cell_r1_c2.state,
                                 cell_r2_c2.state,
                                 cell_r3_c2.state,
                                 cell_r4_c2.state,
                                 cell_r5_c2.state);
    check_col_3 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c3.state,
                                 cell_r1_c3.state,
                                 cell_r2_c3.state,
                                 cell_r3_c3.state,
                                 cell_r4_c3.state,
                                 cell_r5_c3.state);
    check_col_4 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c4.state,
                                 cell_r1_c4.state,
                                 cell_r2_c4.state,
                                 cell_r3_c4.state,
                                 cell_r4_c4.state,
                                 cell_r5_c4.state);
    check_col_5 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c5.state,
                                 cell_r1_c5.state,
                                 cell_r2_c5.state,
                                 cell_r3_c5.state,
                                 cell_r4_c5.state,
                                 cell_r5_c5.state);
    check_col_6 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r0_c6.state,
                                 cell_r1_c6.state,
                                 cell_r2_c6.state,
                                 cell_r3_c6.state,
                                 cell_r4_c6.state,
                                 cell_r5_c6.state);

    check_diag_down_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(cell_r3_c0.state,
                                       cell_r2_c1.state,
                                       cell_r1_c2.state,
                                       cell_r0_c3.state);
    check_diag_down_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(FREE,
                                       cell_r4_c0.state,
                                       cell_r3_c1.state,
                                       cell_r2_c2.state,
                                       cell_r1_c3.state,
                                       cell_r0_c4.state);
    check_diag_down_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r5_c0.state,
                                       cell_r4_c1.state,
                                       cell_r3_c2.state,
                                       cell_r2_c3.state,
                                       cell_r1_c4.state,
                                       cell_r0_c5.state);
    check_diag_down_3 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r5_c1.state,
                                       cell_r4_c2.state,
                                       cell_r3_c3.state,
                                       cell_r2_c4.state,
                                       cell_r1_c5.state,
                                       cell_r0_c6.state);
    check_diag_down_4 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(FREE,
                                       cell_r5_c2.state,
                                       cell_r4_c3.state,
                                       cell_r3_c4.state,
                                       cell_r2_c5.state,
                                       cell_r1_c6.state);
    check_diag_down_5 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(cell_r5_c3.state,
                                       cell_r4_c4.state,
                                       cell_r3_c5.state,
                                       cell_r2_c3.state);

    check_diag_up_0 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(cell_r3_c6.state,
                                     cell_r2_c5.state,
                                     cell_r1_c4.state,
                                     cell_r0_c3.state);
    check_diag_up_1 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(FREE,
                                     cell_r4_c6.state,
                                     cell_r3_c5.state,
                                     cell_r2_c4.state,
                                     cell_r1_c3.state,
                                     cell_r0_c2.state);
    check_diag_up_2 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r5_c6.state,
                                     cell_r4_c5.state,
                                     cell_r3_c4.state,
                                     cell_r2_c3.state,
                                     cell_r1_c2.state,
                                     cell_r0_c1.state);
    check_diag_up_3 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(cell_r5_c5.state,
                                     cell_r4_c4.state,
                                     cell_r3_c3.state,
                                     cell_r2_c2.state,
                                     cell_r1_c1.state,
                                     cell_r0_c0.state);
    check_diag_up_4 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_6(FREE,
                                     cell_r5_c4.state,
                                     cell_r4_c3.state,
                                     cell_r3_c2.state,
                                     cell_r2_c1.state,
                                     cell_r1_c0.state);
    check_diag_up_5 : check~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...
over_4(cell_r5_c3.state,
                                     cell_r4_c2.state,
                                     cell_r3_c1.state,
                                     cell_r2_c0.state);

DEFINE
    win := check_row_0.win | check_row_1.win | check_row_2.win | check_row_3.win | check_row_4.win | check_row_5.win |
           check_col_0.win | check_col_1.win | check_col_2.win | check_col_3.win | check_col_4.win | check_col_5.win | check_col_6.win |
           check_diag_down_0.win | check_diag_down_1.win | check_diag_down_2.win | check_diag_down_3.win | check_diag_down_4.win | check_diag_down_5.win |
           check_diag_up_0.win | check_diag_up_1.win | check_diag_up_2.win | check_diag_up_3.win | check_diag_up_4.win | check_diag_up_5.win;
    full := cell_r5_c0.state != FREE & cell_r5_c1.state != FREE & cell_r5_c2.state != FREE &
            cell_r5_c3.state != FREE & cell_r5_c4.state != FREE & cell_r5_c5.state != FREE &
            cell_r5_c6.state != FREE;
    winner := case
        check_row_0.win       : check_row_0.winner;
        check_row_1.win       : check_row_1.winner;
        check_row_2.win       : check_row_2.winner;
        check_row_3.win       : check_row_3.winner;
        check_row_4.win       : check_row_4.winner;
        check_row_5.win       : check_row_5.winner;
        check_col_0.win       : check_col_0.winner;
        check_col_1.win       : check_col_1.winner;
        check_col_2.win       : check_col_2.winner;
        check_col_3.win       : check_col_3.winner;
        check_col_4.win       : check_col_4.winner;
        check_col_5.win       : check_col_5.winner;
        check_col_6.win       : check_col_6.winner;
        check_diag_down_0.win : check_diag_down_0.winner;
        check_diag_down_1.win : check_diag_down_1.winner;
        check_diag_down_2.win : check_diag_down_2.winner;
        check_diag_down_3.win : check_diag_down_3.winner;
        check_diag_down_4.win : check_diag_down_4.winner;
        check_diag_down_5.win : check_diag_down_5.winner;
        check_diag_up_0.win   : check_diag_up_0.winner;
        check_diag_up_1.win   : check_diag_up_1.winner;
        check_diag_up_2.win   : check_diag_up_2.winner;
        check_diag_up_3.win   : check_diag_up_3.winner;
        check_diag_up_4.win   : check_diag_up_4.winner;
        check_diag_up_5.win   : check_diag_up_5.winner;
        TRUE                  : FREE;
    esac;

MODULE four_in_a_row()
VAR
    inputs : array 0..6 of { FREE, PLAYER01, PLAYER02 };
    b      : board(inputs);
    move : { PLAYER01, PLAYER02 };

ASSIGN
    init(move) := PLAYER01;
    next(move) := case
        move = PLAYER01 & !victory & !draw: PLAYER02;
        move = PLAYER02 & !victory & !draw: PLAYER01;
        TRUE            : move;
    esac;

DEFINE
    victory := b.win;
    draw    := b.full & !b.win;
    winner  := b.winner;

INVAR inputs[0] != FREE -> inputs[1] = FREE & inputs[2] = FREE & inputs[3] = FREE &
                           inputs[4] = FREE & inputs[5] = FREE & inputs[6] = FREE;
INVAR inputs[1] != FREE -> inputs[0] = FREE & inputs[2] = FREE & inputs[3] = FREE &
                           inputs[4] = FREE & inputs[5] = FREE & inputs[6] = FREE;
INVAR inputs[2] != FREE -> inputs[0] = FREE & inputs[1] = FREE & inputs[3] = FREE &
                           inputs[4] = FREE & inputs[5] = FREE & inputs[6] = FREE;
INVAR inputs[3] != FREE -> inputs[0] = FREE & inputs[1] = FREE & inputs[2] = FREE &
                           inputs[4] = FREE & inputs[5] = FREE & inputs[6] = FREE;
INVAR inputs[4] != FREE -> inputs[0] = FREE & inputs[1] = FREE & inputs[2] = FREE &
                           inputs[3] = FREE & inputs[5] = FREE & inputs[6] = FREE;
INVAR inputs[5] != FREE -> inputs[0] = FREE & inputs[1] = FREE & inputs[2] = FREE &
                           inputs[3] = FREE & inputs[4] = FREE & inputs[6] = FREE;
INVAR inputs[6] != FREE -> inputs[0] = FREE & inputs[1] = FREE & inputs[2] = FREE &
                           inputs[3] = FREE & inputs[4] = FREE & inputs[5] = FREE;
INVAR (move = PLAYER01 & !victory & !draw) -> inputs[0] = PLAYER01 |
      inputs[1] = PLAYER01 | inputs[2] = PLAYER01 | inputs[3] = PLAYER01 |
      inputs[4] = PLAYER01 | inputs[5] = PLAYER01 | inputs[6] = PLAYER01;
INVAR (move = PLAYER02 & !victory & !draw) -> inputs[0] = PLAYER02 |
      inputs[1] = PLAYER02 | inputs[2] = PLAYER02 | inputs[3] = PLAYER02 |
      inputs[4] = PLAYER02 | inputs[5] = PLAYER02 | inputs[6] = PLAYER02;
INVAR (victory | draw) -> inputs[0] = FREE & inputs[1] = FREE & inputs[2] = FREE &
      inputs[3] = FREE & inputs[4] = FREE & inputs[5] = FREE & inputs[6] = FREE;

MODULE main()
VAR
    game : four_in_a_row();

LTLSPEC G !game.victory;

Используя проверку ограниченной модели, можно найти трассировку выполнения, в которой кто-то выигрывает:

~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > check_ltlspec_bmc -k 43             
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G !game.victory    is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample 
Trace Type: Counterexample 
    ...

Игра также может быть смоделирована:

~$ NuSMV -int
NuSMV > reset; read_model -i four_in_a_row.smv ; go_bmc
NuSMV > bmc_pick_state -iv
    ...
NuSMV > bmc_simulate -v -k 43
    ...

Patrick Trentin 27.11.2019

comment

Большое спасибо. Я также должен проверить с проверкой модели, если: - игрок 1 всегда будет побеждать, если он положит свой первый камень в средний столбец (столбец 3)

LTLSPEC G ( game.inputs[3] = PLAYER01 & game.b.cell_r0_c3.state =PLAYER01 & game.turns_count=1 & game.move = PLAYER01) -> G F (game.winner = PLAYER01 & game.victory = TRUE & game.draw = FALSE );

- georgi georgiev; 01.12.2019

comment

игрок 1 никогда не выиграет, если он поставит свой первый камень во внешние столбцы (столбец 0 или 6)

LTLSPEC G (( game.inputs[0] = PLAYER01 |game.inputs[0] = PLAYER01) & (game.b.cell_r0_c0.state =PLAYER01 | game.b.cell_r0_c6.state =PLAYER01) & game.turns_count=1 & game.move = PLAYER01) -> G F (game.winner = PLAYER02 & game.victory = TRUE) | game.draw = FALSE;

Я пишу в консоли NuSMV :go_bmc NuSMV > check_ltlspec_bmc -k 43 Вывод: -- no counterexample found with bound 0 ... -- no counterexample found with bound 43 Это выглядит правильно? - georgi georgiev; 01.12.2019

comment

@georgigeorgiev 1. ни одно из свойств LTL не кодирует то, что вы выразили на естественном языке 2. Я сомневаюсь, что свойство, выраженное на естественном языке, верно: PLAYER01 всегда может сделать принять правильное первое решение, но затем предпринять последовательность глупых шагов и все равно проиграть. - Patrick Trentin; 01.12.2019

comment

3. Вам, вероятно, нужно закодировать следующее: если ИГРОК01 помещает свой первый камень в среднюю колонку, то у ИГРОК01 есть стратегия всегда выигрывать игру, несмотря ни на что. что делает PLAYER02, вы можете посмотреть здесь примеры свойства о выигрышной/проигрышной стратегии для классической игры Крестики-нолики. Однако имейте в виду, что этот класс свойств требует проверки модели CTL, но модель, которую я включил в свой ответ, слишком сложна для проверки модели CTL (она использует слишком много Память) - Patrick Trentin; 01.12.2019

4 по счету с НУСМВ

Ответы (1)

Вопросы по теме