Missing enticing running example for analysis

[vrozen]

We require interesting running examples for analysis.

The most complex model so far is simwar_v1.mm I always wanted to know: "how does Random beat Turtle?". Perhaps now we can find out.

Modeling bonus cards in Risk is not as easy as it seems. Sometimes the rules are such that the bonus increases every time someone exchanges cards. This results in interesting gameplay, but is there something interesting to analyze?

[vrozen]

In both examples I have observed that turn based games are tricky to model with MM. Relying on the step semantics is clumsy because "synchronicity" between concurrent nodes is easily lost. Additionally, resources move at most between two nodes per step. This can cause the effect that a resource did not "propagate as far as intended". How to resolve this?

Approach: By modeling it. I introduce a resource called the Turn, hold on to it during turn activities and release it back to the game when it is another player's turn. This ensures as many MM steps are taken as necessary and we can model-check that turns always end, so the game can't get stuck. The turn resource is a contract beween MM and its engine environment, between designer and engineers and between players and a game.

Note: This solution differs from full Machinations, which introduces "a turn based execution mode" which seems more theoretical.

[vrozen]

The above sketched solution will be necessary in many paces when integrating MM into games. The game engine calls the step API until the MM model signals it it is done.

Note: Perhaps we can automatically analyze MM models to ensure that every interaction that is started is eventually done.

Note: Machinations isn't a reactive system. Using signals we can work around this shortcoming. Gameplay engineers will be forced to specify when interactions complete and agree on the names of these conditions with software engineers integrating the system. I am not sure if they will like doing this manual work, but at least it is clearly defined and the concerns are well separated.