model-checking - Model Checking For Numbers Lite Game

Question

I am going through the model checking methods and I want to use the techniques in order to solve a game called Numbers Paranoia lite as a planning problem.

Given an MxN, (MxN > 8), matrix in which each plate is either Problem Image - empty - identified by a unique number ranging from 1 to 8

the goal is to find a path that starts from the plate labelled with 1, covers all the plates in the matrix and ends on the plate labelled with 8. All non-empty plates in a valid path must be sorted in increasing order from 1 to 8.

I am confused with modelling the game into transition state and running NuSMV for results. Here is my solution

--·¹º§ : 01
MODULE main
VAR
rec: {101,102,103,104,105,106,107,201,202,203,204,205,206,207,301,302,303,304,305,306,307,401,402,403,404,405,406,407,501,502,503,504,505,506,507};
ASSIGN
init(rec) := 101;
next(rec) := case
rec = 101 : {102, 201};
rec = 102 : {101,202,103};
rec = 103 : {102,203,104};
rec = 104 : {103, 204,105};
rec = 105 : {104,205,106};
rec = 106 : {105,206,107};
rec = 107 : {106,207};
rec = 201 : {101, 202, 301};
rec = 202 : {201,102,203,302};
rec = 203 : {103, 202, 204, 303};
rec = 204 : {203, 104, 304,205};
rec = 205 : {105,305,206,204};
rec = 206 : {106,207,205,306};
rec = 207 : {107,206,307};
rec = 301 : {201, 302,401};
rec = 302 : {301, 303, 202,402};
rec = 303 : {302, 304, 203,403};
rec = 304 : {303, 204,305,404};
--rec = 305 : {305};
rec = 306 : {305,206,307,406};
rec = 307 : {306,207,407};
rec = 401 : {301,402,501};
rec = 402 : {401,302,403,502};
rec = 403 : {402,303,404,503};
rec = 404 : {403,304,405,504};
rec = 405 : {404,305,406,505};
rec = 406 : {405,306,407,506};
rec = 407 : {406,307,507};
rec = 501 : {401,502};
rec = 502 : {501,402,503};
rec = 503 : {502,403,504};
rec = 504 : {503,404,505};
rec = 505 : {504,405,506};
rec = 506 : {505,406,507};
rec = 507 : {506,407};
TRUE : rec;
esac;
LTLSPEC !(G(rec=101 -> X(!(rec=101) U rec=305))
& G(rec=102 -> X(!(rec=102) U rec=305))
& G(rec=103 -> X(!(rec=103) U rec=305))
& G(rec=104 -> X(!(rec=104) U rec=305))
& G(rec=105 -> X(!(rec=105) U rec=305))
& G(rec=106 -> X(!(rec=106) U rec=305))
& G(rec=107 -> X(!(rec=107) U rec=305))
& G(rec=201 -> X(!(rec=201) U rec=305))
& G(rec=202 -> X(!(rec=202) U rec=305))
& G(rec=203 -> X(!(rec=203) U rec=305))
& G(rec=204 -> X(!(rec=204) U rec=305))
& G(rec=205 -> X(!(rec=205) U rec=305))
& G(rec=206 -> X(!(rec=206) U rec=305))
& G(rec=207 -> X(!(rec=207) U rec=305))
& G(rec=301 -> X(!(rec=304) U rec=305))
& G(rec=302 -> X(!(rec=302) U rec=305))
& G(rec=303 -> X(!(rec=303) U rec=305))
& G(rec=304 -> X(!(rec=304) U rec=305))
--& G(rec=305 -> X(!(rec=305)))
& G(rec=306 -> X(!(rec=306) U rec=305))
& G(rec=307 -> X(!(rec=307) U rec=305))
& G(rec=401 -> X(!(rec=401) U rec=305))
& G(rec=402 -> X(!(rec=402) U rec=305))
& G(rec=403 -> X(!(rec=403) U rec=305))
& G(rec=404 -> X(!(rec=404) U rec=305))
& G(rec=405 -> X(!(rec=405) U rec=305))
& G(rec=406 -> X(!(rec=406) U rec=305))
& G(rec=407 -> X(!(rec=407) U rec=305))
& G(rec=501 -> X(!(rec=501) U rec=305))
& G(rec=502 -> X(!(rec=502) U rec=305))
& G(rec=503 -> X(!(rec=503) U rec=305))
& G(rec=504 -> X(!(rec=504) U rec=305))
& G(rec=505 -> X(!(rec=505) U rec=305))
& G(rec=506 -> X(!(rec=506) U rec=305))
& G(rec=507 -> X(!(rec=507) U rec=305))
& (F rec=101 & F rec=102 & F rec=103 & F rec=104 & F rec=105 & F rec=106 & F rec=107 & F rec=201 & F rec=202 & F rec=203 & F rec=204 & F rec=205 & F rec=206 & F rec=207 & F rec=301 & F rec=302 & F rec=303 & F rec=304 & F rec=305 & F rec=306 & F rec=307 & F rec=401 & F rec=402 & F rec=403 & F rec=404 & F rec=405 & F rec=406 & F rec=407  & F rec=501 & F rec=502 & F rec=503 & F rec=504 & F rec=505 & F rec=506 & F rec=507)& (F(rec=402 & F(rec=107 & F(rec=303 & F(rec=202  &  F(rec=102 & F(rec=205 U rec=305))))))))

score 1 · Accepted Answer

在这个新答案中，我将为您提供另一种可能的解决方案，与我之前的解决方案不同，它可以在NuSMV和nuXmv上运行。

您当前对解决方案的尝试超出了内存，并且--尽管目前我对 NuSMV 的具体内部知识还不够了解，无法解释确切的原因--我很清楚，这是由于相当差的问题的编码。

您的LTL财产过于复杂，而且完全没有理由。目标状态不应该比不存在从 A 到 B 的路径更复杂，其中A是初始状态，B是所需的最终状态。

为此，您需要首先将以下内容编码为过渡系统的一部分：

1.每个板块最多可访问一次

2.必须按正确的顺序访问每个编号的车牌

第1点的一种可能方法是保留整个矩阵的本地副本并将每个位置标记为已访问，然后相应地修改转换关系，以删除那些最终会在已经访问过的板上的转换。

对于第2点，相反，由于您已经知道编号板之间的所需顺序是什么，那么您可以简单地对两个过渡系统进行（某种）同步组合。

让我们再次考虑下图中显示的难题：

然后，解决这个难题的编码是：

-- Numbers Paranoia lite game model example
--
-- author: Patrick Trentin
--
MODULE main
VAR
  index    : 0..11;        -- current position
  sequence : {3, 4, 2, 5}; -- last numbered plate visited
  plates   : array 0..11 of { 0, 1 };
                           -- 0: plate not visited, 1: plate visited

DEFINE
  goal_state := sequence = 5 & index = 5 &
                plates[0] = 1 & plates[1] = 1 & plates[2] = 1  & plates[3] = 1 &
                plates[4] = 1 & plates[5] = 1 & plates[6] = 1  & plates[7] = 1 &
                plates[8] = 1 & plates[9] = 1 & plates[10] = 1 & plates[11] = 1;

ASSIGN
  init(index) := 3;
  init(sequence) := 3;

  init(plates[0])  := 0;
  init(plates[1])  := 0;
  init(plates[2])  := 0;
  init(plates[3])  := 1; -- starting plate, marked as visited
  init(plates[4])  := 0;
  init(plates[5])  := 0;
  init(plates[6])  := 0;
  init(plates[7])  := 0;
  init(plates[8])  := 0;
  init(plates[9])  := 0;
  init(plates[10]) := 0;
  init(plates[11]) := 0;


  -- possible moves from any given plate, ignoring
  -- the restriction over visiting the same plate
  -- more than once
  next(index) := case
    index = 0  : {1, 4};
    index = 1  : {0, 2, 5};
    index = 2  : {1, 3, 6};
    index = 3  : {2, 7};
    index = 4  : {0, 5, 8};
--  end plate: omitted
    index = 6  : {2, 5, 7, 10};
    index = 7  : {3, 6, 11};
    index = 8  : {4, 9};
    index = 9  : {5, 8, 10};
    index = 10 : {6, 9, 11};
    index = 11 : {7, 10};
    TRUE : index;
  esac;

  -- advance sequence only when we hit the correct plate on the table
  next(sequence) := case
--  starting plate: omitted
    sequence = 3 & next(index) = 4 : 4;
    sequence = 4 & next(index) = 2 : 2;
    sequence = 2 & next(index) = 5 : 5;
    TRUE : sequence;
  esac;

  -- mark each plate as visited as soon as we move on it
  next(plates[0])  := case next(index) = 0  : 1; TRUE : plates[0]; esac;
  next(plates[1])  := case next(index) = 1  : 1; TRUE : plates[1]; esac;
  next(plates[2])  := case next(index) = 2  : 1; TRUE : plates[2]; esac;
  next(plates[3])  := case next(index) = 3  : 1; TRUE : plates[3]; esac;
  next(plates[4])  := case next(index) = 4  : 1; TRUE : plates[4]; esac;
  next(plates[5])  := case next(index) = 5  : 1; TRUE : plates[5]; esac;
  next(plates[6])  := case next(index) = 6  : 1; TRUE : plates[6]; esac;
  next(plates[7])  := case next(index) = 7  : 1; TRUE : plates[7]; esac;
  next(plates[8])  := case next(index) = 8  : 1; TRUE : plates[8]; esac;
  next(plates[9])  := case next(index) = 9  : 1; TRUE : plates[9]; esac;
  next(plates[10]) := case next(index) = 10 : 1; TRUE : plates[10]; esac;
  next(plates[11]) := case next(index) = 11 : 1; TRUE : plates[11]; esac;

-- forbid stepping over an already visited plate,
-- unless it is the end plate
TRANS
  (index = 5) | (plates[next(index)] != 1)

-- There is no possible path that reaches the goal state
LTLSPEC !(F goal_state)

您可以使用以下命令在NuSMV（或nuXmv ）中验证模型：

 ~$ NuSMV -int
 NuSMV> read_model -i numbers_lite.smv
 NuSMV> go;
 NuSMV> check_property

您还可以使用命令模拟模型

 NuSMV> pick_state -v
 NuSMV> simulate -i -v -k 11

求解器找到的解决方案如下：

-- specification !(F goal_state)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  index = 3
  sequence = 3
  plates[0] = 0
  plates[1] = 0
  plates[2] = 0
  plates[3] = 1
  plates[4] = 0
  plates[5] = 0
  plates[6] = 0
  plates[7] = 0
  plates[8] = 0
  plates[9] = 0
  plates[10] = 0
  plates[11] = 0
  goal_state = FALSE
-> State: 1.2 <-
  index = 7
  plates[7] = 1
-> State: 1.3 <-
  index = 11
  plates[11] = 1
-> State: 1.4 <-
  index = 10
  plates[10] = 1
-> State: 1.5 <-
  index = 9
  plates[9] = 1
-> State: 1.6 <-
  index = 8
  plates[8] = 1
-> State: 1.7 <-
  index = 4
  sequence = 4
  plates[4] = 1
-> State: 1.8 <-
  index = 0
  plates[0] = 1
-> State: 1.9 <-
  index = 1
  plates[1] = 1
-> State: 1.10 <-
  index = 2
  sequence = 2
  plates[2] = 1
-> State: 1.11 <-
  index = 6
  plates[6] = 1
-- Loop starts here
-> State: 1.12 <-
  index = 5
  sequence = 5
  plates[5] = 1
  goal_state = TRUE

我希望你会发现这个答案很有帮助。

score 0 · Accepted Answer

作为解决您自己的问题的示例，我将游戏编码为nuXmv的过渡状态系统，这是一个通过一些有趣的新功能扩展NuSMV的工具。

更详细地说，我模拟了以下谜题：

因此，在我的模型中，解决方案必须恰好采用11 个步骤，因为矩阵中只有12 个板。

smv代码如下：

-- Numbers Paranoia lite game model example
--
-- author: Patrick Trentin
--

MODULE main()
VAR
  table : array 0..11 of {1, 2, 3, 4, 0};
  index : 0..11;
  cur_max : 0..4;
  steps : 0..11;

ASSIGN
  init(steps) := 0;

  -- starting position is known
  init(index) := 3;
  init(cur_max) := 1;

  -- initialize table configuration
  init(table[0])  := 0;
  init(table[1])  := 0;
  init(table[2])  := 3;
  init(table[3])  := 1;
  init(table[4])  := 2;
  init(table[5])  := 4;
  init(table[6])  := 0;
  init(table[7])  := 0;
  init(table[8])  := 0;
  init(table[9])  := 0;
  init(table[10]) := 0;
  init(table[11]) := 0;

  -- update max value each time we hit a plate with greater value
  next(cur_max) := case
     table[index] > cur_max : table[index];
     TRUE : cur_max;
  esac;

  -- overwrite the value in the plate each time we visit it,
  -- to prevent visiting it again from another plate
  next(table[0])  := case index = 0  : cur_max; TRUE : table[0]; esac;
  next(table[1])  := case index = 1  : cur_max; TRUE : table[1]; esac;
  next(table[2])  := case index = 2  : cur_max; TRUE : table[2]; esac;
  next(table[3])  := case index = 3  : cur_max; TRUE : table[3]; esac;
  next(table[4])  := case index = 4  : cur_max; TRUE : table[4]; esac;
  next(table[5])  := case index = 5  : cur_max; TRUE : table[5]; esac;
  next(table[6])  := case index = 6  : cur_max; TRUE : table[6]; esac;
  next(table[7])  := case index = 7  : cur_max; TRUE : table[7]; esac;
  next(table[8])  := case index = 8  : cur_max; TRUE : table[8]; esac;
  next(table[9])  := case index = 9  : cur_max; TRUE : table[9]; esac;
  next(table[10]) := case index = 10 : cur_max; TRUE : table[10]; esac;
  next(table[11]) := case index = 11 : cur_max; TRUE : table[11]; esac;

DEFINE
  upper_plate := (index - 4);
  lower_plate := (index + 4);
  left_plate  := (index - 1);
  right_plate := (index + 1);

  upper_exists := upper_plate >= 0;
  lower_exists := lower_plate <= 11;
  left_exists  := (left_plate >= 0)  &
                  (left_plate <= 11) &
                  (left_plate mod 4) < (index mod 4); 
  right_exists := (right_plate >= 0)  &
                  (right_plate <= 11) &
                  (right_plate mod 4) > (index mod 4);

  can_go_upper := upper_exists &
                  (table[upper_plate] = 0 |
                  table[upper_plate] = cur_max + 1);
  can_go_lower := lower_exists &
                  (table[lower_plate] = 0 |
                  table[lower_plate] = cur_max + 1);
  can_go_left  := left_exists &
                  (table[left_plate] = 0 |
                  table[left_plate] = cur_max + 1);
  can_go_right := right_exists &
                  (table[right_plate] = 0 |
                  table[right_plate] = cur_max + 1);

-- set of legal moves
TRANS
  !can_go_upper -> next(index) != upper_plate
TRANS
  !can_go_lower -> next(index) != lower_plate
TRANS
  !can_go_left  -> next(index) != left_plate
TRANS
  !can_go_right -> next(index) != right_plate
TRANS
  next(index) = index | next(index) = upper_plate |
  next(index) = lower_plate | next(index) = left_plate |
  next(index) = right_plate

-- loop on the current plate only when search has ended
TRANS
  (!can_go_upper & !can_go_lower & !can_go_left & !can_go_right) -> next(index) = index
TRANS
  (can_go_upper | can_go_lower | can_go_left | can_go_right) -> next(index) != index

-- increase steps value if plate changes
TRANS
  index != next(index) -> next(steps) = steps + 1
TRANS
  index = next(index) -> next(steps) = steps

-- there does not exist a path that terminates on the 
-- highest value and takes exactly N = size(array)-1 
-- steps to reach.
-- A path violating this property is a possible solution
-- for the Numbers Paranoia lite game.
LTLSPEC !(F (table[index] = 4 & steps = 11))

您可以使用以下命令验证模型，这些命令依赖于底层MathSAT5 SMT Solver来执行验证步骤：

 ~$ nuXmv -int
 nuXmv> read_model -i numbers_lite.smv
 nuXmv> go_msat;
 nuXmv> msat_check_ltlspec_bmc -k 11

您还可以使用命令模拟模型

 nuXmv> msat_pick_state -i -v
 nuXmv> msat_simulate -i -v -k 11

求解器找到的解决方案如下：

-- specification !( F (table[index] = 4 & steps = 11))  is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    table[0] = 0
    table[1] = 0
    table[2] = 3
    table[3] = 1
    table[4] = 2
    table[5] = 4
    table[6] = 0
    table[7] = 0
    table[8] = 0
    table[9] = 0
    table[10] = 0
    table[11] = 0
    index = 3
    cur_max = 1
    steps = 0
    can_go_right = FALSE
    can_go_left = FALSE
    can_go_lower = TRUE
    right_exists = FALSE
    left_exists = TRUE
    lower_exists = TRUE
    upper_exists = FALSE
    right_plate = 4
    left_plate = 2
    lower_plate = 7
    upper_plate = -1
  -> State: 1.2 <-
    index = 7
    steps = 1
    can_go_left = TRUE
    can_go_upper = FALSE
    upper_exists = TRUE
    right_plate = 8
    left_plate = 6
    lower_plate = 11
    upper_plate = 3
  -> State: 1.3 <-
    table[7] = 1
    index = 11
    steps = 2
    lower_exists = FALSE
    right_plate = 12
    left_plate = 10
    lower_plate = 15
    upper_plate = 7
  -> State: 1.4 <-
    table[11] = 1
    index = 10
    steps = 3
    can_go_upper = TRUE
    right_exists = TRUE
    right_plate = 11
    left_plate = 9
    lower_plate = 14
    upper_plate = 6
  -> State: 1.5 <-
    table[10] = 1
    index = 9
    steps = 4
    can_go_upper = FALSE
    right_plate = 10
    left_plate = 8
    lower_plate = 13
    upper_plate = 5
  -> State: 1.6 <-
    table[9] = 1
    index = 8
    steps = 5
    can_go_left = FALSE
    can_go_upper = TRUE
    left_exists = FALSE
    right_plate = 9
    left_plate = 7
    lower_plate = 12
    upper_plate = 4
  -> State: 1.7 <-
    table[8] = 1
    index = 4
    steps = 6
    can_go_lower = FALSE
    lower_exists = TRUE
    right_plate = 5
    left_plate = 3
    lower_plate = 8
    upper_plate = 0
  -> State: 1.8 <-
    table[4] = 1
    index = 0
    cur_max = 2
    steps = 7
    can_go_right = TRUE
    upper_exists = FALSE
    right_plate = 1
    left_plate = -1
    lower_plate = 4
    upper_plate = -4
  -> State: 1.9 <-
    table[0] = 2
    index = 1
    steps = 8
    left_exists = TRUE
    right_plate = 2
    left_plate = 0
    lower_plate = 5
    upper_plate = -3
  -> State: 1.10 <-
    table[1] = 2
    index = 2
    steps = 9
    can_go_right = FALSE
    can_go_lower = TRUE
    right_plate = 3
    left_plate = 1
    lower_plate = 6
    upper_plate = -2
  -> State: 1.11 <-
    table[2] = 2
    index = 6
    cur_max = 3
    steps = 10
    can_go_left = TRUE
    can_go_lower = FALSE
    can_go_upper = FALSE
    upper_exists = TRUE
    right_plate = 7
    left_plate = 5
    lower_plate = 10
    upper_plate = 2
  -> State: 1.12 <-
    table[6] = 3
    index = 5
    steps = 11
    can_go_left = FALSE
    right_plate = 6
    left_plate = 4
    lower_plate = 9
    upper_plate = 1

请注意，-k 11该命令的选项msat_check_ltlspec_bmc要求求解器查找转换次数最多为11 的任何解决方案。鉴于我对问题的编码，如果在11 步内没有找到解决方案，那么我们可以安全地得出结论，不存在可能的解决方案对于输入表。

您可以轻松地将此模型扩展为更大的表，我建议您编写一个python 脚本来自动执行此操作，因为模型的结构保持不变，只有少数参数和初始化值发生变化。

我希望你会发现这个答案很有帮助。

model-checking - Model Checking For Numbers Lite Game

2 回答 2

Related

Reference