Assignment 1B (Alternative 2): UltimateTicTacToe

Assignment 1B (Alternative 2): UltimateTicTacToe

by Wolfgang Schreiner -
Number of replies: 1

I was notified (by an early elaborator of that assignment) that RISCAL often crashes when running the game model to produce the traces to winning games.

Debugging this issue, it seems to me that the problem is not in RISCAL itself but in the underlying graphical toolkit (the SWT library) which (in its current version) for some reason crashes, if too much (or too quickly?) output is produced. While I cannot really do anything about this now, some mitigations:

  1. Setting in the model "val all = false;" (only a single winning game is printed, not all of them) lets the crash occur much more rarely. This might be sufficient for the purpose of this assignment.
  2. Additionally, choosing in the RISCAL "Analysis" panel the red button "Start Logging" writes the screen output also into a file; here much more output is logged than shown in the screen until the crash.

With (1) or (1+2) it should be possible to produce the expected results. If not, just report the error and what game moves you could deduce from the partial output.

In reply to Wolfgang Schreiner

Re: Assignment 1B (Alternative 2): UltimateTicTacToe

by Wolfgang Schreiner -

I was notified that there is some problem with the "winning condition" in the file I handed out. After some inspection, I've indeed identified/corrected the following errors:

  • The invariant should actually state that the other (prevously selected) player has won the game:
  invariant let player = other(player) in wins(board, player) ⇒ ...
  • Also the action should not be allowed any more if the other player has already won the game:
  action play(choice0:Choice) with 
    ¬wins(board, other(player)) ∧ legal(board, choice, choice0);
  {
    board[choice0.global][choice0.local] = player;
    player := other(player);
    choice := choice0;
  }

The definition of the new function "other" is:

// the other player
fun other(player:Player):Player 
  requires player ≠ none;
= if player = first then second else first;

Thank you for pointing out the problem; I've uploaded a new version of "UltimateTicTacToe.txt" in the assignment.