> State: 1.1 State: 1.2 State: 1.3 State: 1.4 State: 1.5 State: 1.6 State: 1.7 State: 1.8 State: 1.9 State: 1.10 State: 1.11 State: 1.ProB provides support for LTL (linear temporal logic) model checking.
specification AF (AG bricks != 0) is false If instead you want to find a possible solution, just flip the property: > check_ctlspec -p "AF AG (bricks != 0)" specification AF (AG bricks = 0) is true You can run it with both NuSMV and nuXmv using the following commands: > read_model -i game.smv I think the code is quite self-explanatory. zero for every possible state in every possible path, Sooner or later the number of bricks will always be bricks, and equal to zero when there are still bricks to take.
forbid q values from being both larger than the remaining number of as demonstrated by the following execution sequence In fact, using this property results in a counter-example similar to your own: - specification AF (AG winner = a | AG winner = b) is false The property that you seem to really want to verify is AF (AG winner = a | AG winner = b). Perhaps you simulated the program and simply observed that it behaves in an unexpected manner. I am not sure how you provided a counter-example, since the property you specified is verified by the model: - specification AF (winner = a | winner = b) is true i = 1Īs you can see, model still provide a counter example where player b win the game after playe a already won. I want to express that "eventually there is a winner",but my code doesn't work because it does not prevent player taking brick after brick=0, so eventually player a,b will both become winner.Īnd here is my output on SPEC AF (winner = a | winner = none) to illustrate my point. Assume player A go first, and here is my attempt.
There are 10 bricks in a pile, each player can take 1-3 brick per turn, whoever take the last brick wins the game. I'm new to NuSMV and try to model this simple turn-based game.
0 kommentar(er)
