**[« Back to LFS website](https://csci1710.github.io)**

# Lab I: Tic-Tac-Toe

:::warning
**Lab Dates:** Wednesday, January 29th - Thursday, January 30th
:::

**Stencil**: Download the stencil [here](https://drive.google.com/file/d/1BfX7TXzCYfqziwHRDKKQTe7K9oBkxkf7/view?usp=drive_link).

## Overview
In this lab, we’ll start by expanding the tic-tac-toe board model that you saw in class on Wednesday. By the end of these exercises, you will have gained valuable practice with:
writing predicates in Forge;

- using Forge to produce example instances that you can view;
- using Forge to check properties (in this case, about moves in tic-tac-toe); and
- using Forge to compare two different predicates that might seem equivalent.

After this, we’ll move on to an informal experiment with specification in a very different domain: generative AI.

## Part 1: Forge
This week in class, we’ve been modeling the game of tic-tac-toe. By the time class ended on Wednesday, we had modeled boards, and started to model moves between boards. The starter model for this lab contains one possible finished move predicate.

A game of tic-tac-toe is a system. Although it’s fairly simple, we’ll model more complex systems in much the same way later in the semester: we used constraints to describe:

- the initial state(s) of the board;
- how one board can transition to another board via a move of the game;
- what constitutes a valid board and a winning board; and even
- checked that certain properties of a board were preserved by the move action.

## Assignment
:::success
**Task:** Fill in the [provided stencil](https://drive.google.com/file/d/1BfX7TXzCYfqziwHRDKKQTe7K9oBkxkf7/view?usp=drive_link) to complete the following steps:
:::
1. Read the code provided for the Tic-Tac-Toe model. If you have any questions at this point, call over a TA before moving on.
2. Check whether it’s possible for a valid board to have both X and O as winners.
3. Observe different starting moves from the first player (run your predicate and click Next in the top right of the Sterling visualizer).
4. Investigate what would happen if you rewrote the move predicate to eliminate the `p = O implies oturn[pre]` constraint, and then explain why removing that constraint has an impact. To do this, you can copy the old version into a different predicate with a different name, and then ask Forge for an instance where one predicate is true and the other is false. E.g., `(oldMove[...]) and (not newMove[...])`. Remember to check both directions: it might also be that it's `oldMove` that evaluates to false.

After completing all of the steps, call over a TA to be checked off for Part 1.

## Part 2: Specification and LLM Prompts
As you might be aware, there’s a lot of excitement about Large Language Models (LLMs) for answering questions and producing written artifacts—even, in many cases, code. We’ll be talking more about it and other generative AI tools this semester, and you’ll be getting the chance to explore them on some of our assignments.

But 1710 isn’t an AI class; it’s a class on modeling, specification, and verification. So why are we complicating things by bringing in LLMs? Simply put, whether you’re asking it for code, or text, or even a Forge model:
- Getting what you want is heavily reliant on phrasing your goals carefully.
- Evaluating what you’re given requires you to test your goals carefully.
- Generative AI isn’t going away, and the ability to think critically about your goals directly impacts how effective, professional, and even safe it is to use.
- Thinking critically about what we want and how we describe it? That’s 1710!

### Caveats
Because ChatGPT and other LLMs are often non-deterministic and their model may be refined over time, it’s possible that your results will vary from ours—that’s OK; use this as an opportunity to experiment, think critically, and prepare for a discussion later. There is not a “correct answer” to this exercise.

:::success
**Task:** Explore whether ChatGPT (or another LLM of your choice) can accurately express, and use, the rules of tic-tac-toe. Concretely, follow these rough steps:
:::
1. Ask the LLM for a specification of a tic-tac-toe board.
2. Ask the LLM for a specification of valid moves in tic-tac-toe, and then do the same for the winning criteria of the game.
3. Ask the LLM if a given move is valid on a particular board.
4. Reflect on those answers. If the LLM were playing tic-tac-toe with you, could you find a way to “cheat” in the game? E.g., does it seem like it would let you place multiple marks at a time, or overwrite one of its marks, move one of yours, etc.?
5. Finally, ask the LLM for a Forge model of tic-tac-toe. (It may be helpful to frame this with a reminder like “The Forge modeling language is a variant of Alloy” since Alloy is better known than Forge, and GPT is limited by its training data.) How good is the model it gives you? Was it difficult to get a model that ran, or produced results that looked right? Does the response from the LLM seem to agree with its replies to your earlier questions?

:::info
**Note:** Remember that this exercise isn’t about disparaging LLMs (as some news articles do). It’s about critically thinking about what they provide, what they might need help with, and how the amount of careful thought behind your goals can influence the quality of your results.
:::

### TA Checkoff
Call over a TA and share your findings!