模型检查数字精简版游戏

Question

我正在通过 模型检查 方法，我想使用这些技术来解决一个名为 Numbers Paranoia lite 的游戏 规划问题。

给定一个 MxN，(MxN > 8) 矩阵，其中每个板是 Problem Image - 空的 - 由 唯一 数字标识，范围从 1 到 8

目标是找到一条从标有 1 的盘子开始、覆盖所有矩阵中的盘子并 >ends在标有 8 的盘子上。有效路径中的所有非空盘子必须按从 1 到 8 的升序排序。

我对将游戏建模为过渡状态并运行 NuSMV 以获得结果感到困惑。这是我的解决方案

--·¹º§ : 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))))))))

Answer 1

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

---

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

您的 LTL 属性过于复杂，而且完全没有原因。 goal_state 不应该比 不存在从 A 到 B 的路径更复杂，其中 A 是初始状态，B 是期望的结束状态。

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

1.每个盘子最多可以访问一次

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

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

对于 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

希望这个答案对您有所帮助。

Answer 2

作为解决您自己问题的示例，我将游戏编码为 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

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

你可以很容易地为更大的表扩展这个模型，我建议你写一个python脚本来自动完成，因为模型的结构保持不变，只有几个参数和初始化值改变。

希望这个答案对您有所帮助。