CODEWITHSUNDEEP
triggersverificationdafny
Jofbr
Jofbr

Reputation: 473

Dafny no terms to trigger on predicate

I have the following snippet Dafny code for a tic tac toe game to check if player 1 has a winning row on the board:

predicate isWinRowForPlayer1(board: array2<int>)
  reads board
  requires board.Length0 == board.Length1 == 3 && isValidBoard(board)
{
  exists i :: 0 <= i < board.Length0 ==> (forall j :: 0 <= j < board.Length1 ==> board[i, j] == 1)
}

Currently I am getting a /!\ No terms found to trigger on. error on the body of this predicate and all other predicates I have in my program (for winColumn, winDiag, ... etc)

Would appreciate if someone can help me to fix this

Upvotes: 4

Views: 331

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Here is one way to do it: introduce a helper function to hold the forall quantifier. Dafny will then use this helper function as the trigger for the outer exists quantifier, fixing the warning.

predicate RowIsWinRowForPlayer1(board: array2<int>, row: int)
    reads board
    requires 0 <= row < board.Length0
{
    forall j :: 0 <= j < board.Length1 ==> board[row, j] == 1
}

predicate isWinRowForPlayer1(board: array2<int>)
  reads board
  requires board.Length0 == board.Length1 == 3 && isValidBoard(board)
{
  exists i :: 0 <= i < board.Length0 ==> RowIsWinRowForPlayer1(board, i)
}

See this answer for more information about triggers.

Upvotes: 1

Related Questions