Model Checking For Numbers Lite Game

2
votes

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))))))))
2
model-checkingplanningnusmv

2 Answers

1
votes

In this new answer I will provide you with another possible solution that, differently from my previous one, can be run on both NuSMV and nuXmv.

Your current attempt of a solution goes out of memory and --although at the time being I don't know enough on the specific internals of NuSMV to explain the exact reason-- it is clear to me that this is due to a rather poor encoding of the problem.

Your LTL property is overly complicated, and for no reason at all. The goal_state shouldn't be more complicated than there exists no path from A to B, where A is the initial state and B is the desired end state.

For doing this, you need to encode the following things as part of your transition system first:

1. each plate can be visited at most once

2. each numbered plate must be visited in the correct order

A possible approach for point 1. is to keep a local copy of the whole matrix and mark each location as visited, and then modify the transition relation accordingly so to remove those transitions that would end up over an already visited plate.

For the point 2., instead, since you already know what is the desired order among the numbered plates, then you can simply do a (sort of) synchronous composition of the two transitions systems.

Let's consider again the puzzle shown in the following picture:

enter image description here

Then, an encoding that solves that puzzle is:

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

You can verify the model in NuSMV (or nuXmv) with the following commands:

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

You can also simulate the model with the commands

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

The solution found by the solver is the following one:

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

I hope you'll find this answer helpful.

0
votes

As an example for solving your own problem, I encoded the game into a transition state system for nuXmv, which is a tool that extends NuSMV with some interesting new features.

More in detail, I modelled the following puzzle:

enter image description here

Thus, in my model the solution must take exactly 11 steps, as there are only 12 plates in the matrix.

The smv code follows:

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

You can verify the model with the following commands, which rely on the underlying MathSAT5 SMT Solver for doing the verification step:

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

You can also simulate the model with the commands

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

The solution found by the solver is the following one:

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

Notice that the option -k 11 for the command msat_check_ltlspec_bmc requires the solver to look for any solution whose number of transitions is up to 11. Given my encoding of the problem, if no solution is found within 11 steps then we can safely conclude that there exists no possible solution for the input table.

You can easily extend this model for larger tables, I suggest you to write a python script for doing it automatically, as the structure of the model remains the same and only a few parameters and initialization values change.

I hope you'll find this answer helpful.