퍼즐 게임(Theseus and the Minotau)을 model checker를 이용해 자동으로 해결하기

• 매 턴, 테세우스는 최대 1칸, 미노타우르스는 최대 2칸 까지 움직일 수 있음.
• 테세우스가 탈출구로 이동하면 승리.
• 미노타우르스는 항상 다음과 같이 움직임
  1. 미노타우르스가 가로로 움직여 테세우스와 가까워질 수 있는가? 그렇다면 2번, 아니면 3번.
  2. 테세우스를 향해 가로로 한 칸 움직인 후 5번.
  3. 미노타우르스가 세로로 움직여 테세우스와 가까 워질 수 있는가? 그렇다면 4번, 아니면 5번.
  4. 테세우스를 향해 세로로 한 칸 움직인 후 5번.
  5. 한 턴 종료.

맵의 행렬을 인코딩하고 벽의 위치에 따라 notLeft, notRight, notUp, notDown 등의 boolean 값을 정의한다.

예를 들어 notLeft = black=101 | black=201; 이면 black(미노타우르스)이 101이나 201에 있을때는 왼쪽으로 이동하지 못한다는 뜻이다. 이 값은 밑에 next state를 정의할때 사용된다.

테세우스

1. case 문을 통해 아래와 같은 네가지 케이스에서 테세우스의 next state를 정의해준다.

   이때 turn이 true일때만 동작할 수 있다.

   1. 상하좌우 모두 움직일 수 있을때 -> 모두 갈 수 있음
   2. 한면이 막혀있을때 -> 막혀있지 않은 세면만 갈 수 있음
   3. 두면이 막혀있을때 -> 막혀있지 않은 두면만 갈 수 있음
   4. 세면이 막혀있을때 -> 막혀있지 않은 한면만 갈 수 있음

미노타우르스

1. case 문을 통해 아래와 같은 네가지 케이스에서 미노타우르스의 next state를 정의해준다.

   테세우스가 1번 동작할때 미노타우르스는 2번 동작하기 때문에 turn(boolean)의 값에 상관없이 수행된다.

   1. 위에서 움직인 테세우스가 미노타우르스보다 오른쪽에 있다 & 오른쪽으로 갈 수 있다. -> 오른쪽으로 이동

   2. 위에서 움직인 테세우스가 미노타우르스보다 왼쪽에 있다 & 왼쪽으로 갈 수 있다. -> 왼쪽으로 이동

   3. 좌우로 움직이지 않는다. & 위에서 움직인 테세우스가 미노타우르스보다 위에 있다 & 위로 갈 수 있다. -> 위로 이동

      좌우로 움직이지 않는 상황 수 없는 상황은 다음과 같다.

      1. 테세우스와 미노타우르스와 x 위치가 같다. (이 상황에서 좌/우로 이동하면 더 멀어질뿐이다)
      2. 좌/우로 움직이면 가까워지지만 벽에 막혀있다.

   4. 좌우로 움직이지 않는다. & 위에서 움직인 테세우스가 미노타우르스보다 아래에 있다 & 아래로 갈 수 있다. -> 아래로 이동

      좌우로 움직이지 않는 상황 수 없는 상황은 다음과 같다.

      1. 테세우스와 미노타우르스와 x 위치가 같다. (이 상황에서 좌/우로 이동하면 더 멀어질뿐이다)
      2. 좌/우로 움직이면 가까워지지만 벽에 막혀있다.

"goal일때까지 red가 black에게 잡히지 않는 상황은 전체적으로 없다" 라고 속성을 명세한다. 만약 반례가 있다면 해당 반례를 return할 것이다. 이는 곧 solution이 된다.

! G ((!(red = black)) U (red = redGoal));

• Code 폴더

  • 2.smv, 87.smv : 스테이지 별 솔루션 코드 (stage2, stage87)

• Log 폴더

  • 2.txt, 87.txt : 스테이지 별 model checking 결과 log

    실행 방법

    ./NuSMV 2.smv > 2.txt

• Visualize 폴더

  • 2_solution.png, 87.solution.png : 스테이지 별 솔루션 그림
  • 2_filter.txt, 87_filter.txt : 솔루션 그림을 편하게 그리기 위해 테세우스의 path 만 남겨놓은 파일
  • log_filter.ipynb : 테세우스의 path 만 남겨놓기 위해 기존 log 수정 코드