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模型检查：创建一个简单的游戏模型

回答

相关问题