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 Comments
Leave a Reply. |