Search code examples
model-checkingplanningnusmv

Model Checking For Numbers Lite Game

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

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