NuSMV模型檢查：創建一個簡單的遊戲模型

我是NuSMV的新手，並嘗試對這個簡單的回合制遊戲進行建模。一堆中有10塊磚，每個玩家每回合可以拿1-3塊磚，誰拿走最後一塊磚就贏得比賽。假設玩家A先去，這是我的嘗試。我想表達的是，「最終有一個勝利者」，但是我的代碼不起作用，因爲它不阻止玩家在磚塊= 0之後採取磚塊，所以最終玩家a，b都會成爲贏家。NuSMV模型檢查：創建一個簡單的遊戲模型

這裏是我的代碼：

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

正如你所看到的，模型仍然提供了一個反例的例子，其中玩家b已經贏得比賽後贏得比賽。

來源

2016-03-28 user97919

我不知道你是如何提供一個反例，因爲你指定是通過模型驗證屬性：

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

我認爲的代碼是相當不言自明。相反，如果你想找到一個可行的解決方案

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

，只需扳動屬性：

您可以NuSMV和都使用下面的命令運行它nuXmv

> 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-01 13:24:13

NuSMV模型檢查：創建一個簡單的遊戲模型

回答

相關問題