Can You Use Formal Verification on a Table Top Game? (Solutions)
--
Practicing breaking down and generalizing problems into formal logic… for fun.
Last month I talked about using formal verification in game design and the challenge of trying to define a problem so that it can be verified. This is part 2 of that story, detailing the various approaches I’ve been using to iterate on game rules and deck structure.
Make It Look Like a State Machine
My first step in specifying any system is usually to make it look like a state machine. Exactly what this state machine looks like depends on what properties we want to verify. The problem I needed the most help thinking through was how many of each card should be in the deck? The composition of the deck will determine whether people feel satisfied or discouraged and bored playing the game with others.
The real function of the game play is to move points from one stock in the deck to another stock on the game board. And because the question is about the composition of the deck, it is better to think about each card value as a different stock storing a certain number of cards. That might look like this:
Build It the Stupid Way First
What’s true in software systems is generally true for other systems as well: build it a naive (stupid) way and see what stands out.
A normal deck of playing cards has 4 suits of 13 cards each. Since this game has 4 categories that’s a good a place to start. The stupid way to design a deck would be to evenly distribute the negative and positive cards so that there are as many negative tens as positive tens, negative twenties as positive twenties and so on. Why is this the stupid way? Because it means that when you play all the cards the total value of points is zero. All games as they continue will creep closer and closer to a stalemate of zero points. The scenario where someone earns enough points to win the game is an edge case that gets less likely as the game plays on. The exact opposite of what we want.
