1

私は NuSMV を初めて使用し、この単純なターン制ゲームをモデル化しようとしています。山には10個のレンガがあり、各プレイヤーは1ターンに1〜3個のレンガを取ることができ、最後のレンガを取った人がゲームに勝ちます. プレイヤー A が最初に行くと仮定すると、これが私の試みです。「最終的に勝者がいる」と表現したいのですが、brick=0 の後にプレーヤーがブロックを取得することを妨げないため、私のコードは機能せず、最終的にプレーヤー a,b の両方が勝者になります。

ここに私のコードがあります:

MODULE main

VAR

bricks : 0..10; 
i : 1..3;
j : 1..3;
turn : boolean;
winner : {none, a, b};

ASSIGN

init(winner) := none;
init(bricks) := 10;
init(turn) := TRUE;
next(turn) := case
        turn : FALSE;
        !turn: TRUE;
        esac;
next(bricks) := 
            case
            bricks - j >= 0 : bricks - j;
            bricks - j < 0 : 0;
            TRUE:bricks;
            esac;

next(winner) := case
            turn=TRUE & bricks  = 0: a;
            turn=FALSE & bricks = 0: b;
            TRUE:winner;
            esac;

SPEC AF (winner = a | winner = b)

そして、これが私の要点を説明するための SPEC AF (勝者 = a | 勝者 = なし) での私の出力です。

i = 1
j = 1
turn = TRUE
winner = none
State: 1.2 <-
bricks = 9
j = 3
turn = FALSE
State: 1.3 <-
bricks = 6
turn = TRUE
State: 1.4 <-
bricks = 3
turn = FALSE
State: 1.5 <-
bricks = 0
j = 1
turn = TRUE
State: 1.6 <-
turn = FALSE
winner = a
State: 1.7 <-
turn = TRUE
winner = b

ご覧のとおり、モデルは、プレイヤー a がすでに勝った後にプレイヤー b がゲームに勝つという反例を提供します。

4

1 に答える 1

0

指定したプロパティはモデルによって検証されるため、どのように反例を提供したかわかりません。

-- specification AF (winner = a | winner = b)  is true

おそらく、プログラムをシミュレートして、プログラムが予期しない方法で動作することを観察しただけでしょう。あなたが本当に確認したいと思われるプロパティは ですAF (AG winner = a | AG winner = b)。実際、このプロパティを使用すると、自分自身のような反例が得られます。

-- specification AF (AG winner = a | AG winner = b)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    bricks = 10
    i = 1
    j = 1
    turn = TRUE
    winner = none
  -> State: 1.2 <-
    bricks = 9
    turn = FALSE
  -> State: 1.3 <-
    bricks = 8
    turn = TRUE
  -> State: 1.4 <-
    bricks = 7
    turn = FALSE
  -> State: 1.5 <-
    bricks = 6
    turn = TRUE
  -> State: 1.6 <-
    bricks = 5
    turn = FALSE
  -> State: 1.7 <-
    bricks = 4
    turn = TRUE
  -> State: 1.8 <-
    bricks = 3
    turn = FALSE
  -> State: 1.9 <-
    bricks = 2
    turn = TRUE
  -> State: 1.10 <-
    bricks = 1
    turn = FALSE
  -> State: 1.11 <-
    bricks = 0
    turn = TRUE
  -- Loop starts here
  -> State: 1.12 <-
    turn = FALSE
    winner = a
  -> State: 1.13 <-
    turn = TRUE
    winner = b
  -> State: 1.14 <-
    turn = FALSE
    winner = a

問題は、ゲームが終了してもターンを反転させ、その結果、勝者も A と B の間で連続して反転することです。

私はあなたのソリューションをより良い方法で書き直しました：

MODULE main

VAR
  bricks : 0..10; 
  q : 0..3;
  turn : {A_TURN , B_TURN};

DEFINE
  game_won := next(bricks) = 0;
  a_won := game_won & turn = A_TURN;
  b_won := game_won & turn = B_TURN;

ASSIGN
  init(bricks) := 10;
  init(turn)   := A_TURN;

  next(bricks) := case
     bricks - q >= 0 : bricks - q;
     TRUE : 0;
  esac;

  next(turn) := case
    turn = A_TURN & !game_won: B_TURN;
    turn = B_TURN & !game_won: A_TURN; 
    TRUE : turn;
  esac;

-- forbid q values from being both larger than the remaining number of 
-- bricks, and equal to zero when there are still bricks to take.
INVAR (q <= bricks)
INVAR (bricks > 0) -> (q > 0)
INVAR (bricks <= 0) -> (q = 0)

-- Sooner or later the number of bricks will always be
-- zero for every possible state in every possible path,
-- that is, someone won the game
CTLSPEC
  AF AG (bricks = 0)

コードは非常に自明だと思います。

次のコマンドを使用して、NuSMVとnuXmvの両方で実行できます。

> read_model -i game.smv
> go
> check_property
-- specification AF (AG bricks = 0)  is true

代わりに可能な解決策を見つけたい場合は、プロパティを反転するだけです:

> check_ctlspec -p "AF AG (bricks != 0)"
-- specification AF (AG bricks != 0)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    bricks = 10
    q = 1
    turn = A_TURN
    game_won = FALSE
    b_won = FALSE
    a_won = FALSE
  -> State: 1.2 <-
    bricks = 9
    turn = B_TURN
  -> State: 1.3 <-
    bricks = 8
    turn = A_TURN
  -> State: 1.4 <-
    bricks = 7
    turn = B_TURN
  -> State: 1.5 <-
    bricks = 6
    turn = A_TURN
  -> State: 1.6 <-
    bricks = 5
    turn = B_TURN
  -> State: 1.7 <-
    bricks = 4
    turn = A_TURN
  -> State: 1.8 <-
    bricks = 3
    turn = B_TURN
  -> State: 1.9 <-
    bricks = 2
    turn = A_TURN
  -> State: 1.10 <-
    bricks = 1
    turn = B_TURN
    game_won = TRUE
    b_won = TRUE
  -- Loop starts here
  -> State: 1.11 <-
    bricks = 0
    q = 0
  -> State: 1.12 <-

この回答がお役に立てば幸いです。

于 2016-04-01T13:24:13.793 に答える