logicmodel-checkingctlnusmv

NuSMV model checking: create a simple game model


I'm new to NuSMV and try to model this simple turn-based game. There are 10 bricks in a pile, each player can take 1-3 brick per turn, whoever take the last brick wins the game. Assume player A go first, and here is my attempt. 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.

here is my code:

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)

and here is my output on SPEC AF (winner = a | winner = none) to illustrate my point.

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

as you can see, model still provide a counter example where player b win the game after playe a already won.


Solution

  • 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
    

    Perhaps you simulated the program and simply observed that it behaves in an unexpected manner. The property that you seem to really want to verify is AF (AG winner = a | AG winner = b). In fact, using this property results in a counter-example similar to your own:

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

    The problem is that you flip turns even when the game is finished, and as a result of this, the winner continuously flips among A and B too.

    I re-wrote your solution in a better way:

    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)
    

    I think the code is quite self-explanatory.

    You can run it with both NuSMV and nuXmv using the following commands:

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

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

    I hope you'll find this answer helpful.