NuSMVモデルチェック：シンプルなゲームモデルを作成

Question

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（勝者=なし勝者=）の私の出力は次のとおりです。

は、ここに私のコードです。

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 

あなたが見ることができるように、モデルは依然としてプレーヤーbが既に勝った後にゲームに勝つ反例を提供します。

Answer 1

あなたがを指定されたプロパティは、モデルによって検証あるので、私は、あなたが反例を提供する方法がわからない：

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

この回答が役に立ったら嬉しいです。