{ "cells": [ { "cell_type": "markdown", "id": "5bb61e58", "metadata": {}, "source": [ "# Step One: Modeling" ] }, { "cell_type": "markdown", "id": "4a115f4f", "metadata": {}, "source": [ "## The Orchard Game\n", "The *Orchard game* (also called *Obstgarten*, *Le verger*, *Boomgaard*, *El Frutal*, *Første Frukthage*) is a simple children’s game. In the following, we model the\n", "First Orchard game variant based on the official rule book [available online](https://cdn.hff.de/image/upload/v1/22/30/28/14/22302814.pdf).\n", "\n", "The game is played cooperatively.\n", "There are four types of **fruit**: **apples** 🍏, **pears** 🍐, **cherries** 🍒 and **plums** 🍇. (We use the grape symbol here as there is no plum symbol).\n", "For each type of fruit, there is a **tree** with four pieces of this fruit.\n", "There is a **basket** 🧺 for collecting fruit.\n", "As antagonist, there is a **raven** 🐦‍⬛ which reaches the orchard after five steps.\n", "\n", "The goal of the game is to collect all fruit before the raven reaches the orchard. In each round, a player throws a six-sided dice and performs an action depending on its outcome:\n", "- If the outcome is a type of fruit 🍏🍐🍒🍇, then the player picks a piece of this type from the tree and places it in the basket. If no fruit is left on the tree, the player cannot pick anything.\n", "- If the outcome is the fruit basket 🧺, then the player may pick any fruit.\n", "- If the outcome is the raven 🐦‍⬛, the raven moves one step towards the orchard.\n", "\n", "The players win iff they collect all fruit before the raven arrives at the orchard." ] }, { "cell_type": "markdown", "id": "0b2aff19", "metadata": {}, "source": [ "## The Orchard Model\n", "Before starting the actual modeling, we make some general modeling decisions.\n", "First, we decide which parts are relevant for the model. In the Orchard game,\n", "we need to keep track of the remaining fruit on the trees and the position of the\n", "raven. As the game is cooperative, it is irrelevant how many players are playing\n", "and we assume one player. We also do not need to keep track of the basket as\n", "only the remaining fruit on the trees are relevant for the winning condition.\n", "\n", "In our Orchard model, we divide each round into two distinct phases: first\n", "throwing the dice and then acting on the outcome. This allows to separate the\n", "probabilistic dice throw from the player’s (potentially nondeterministic) action.\n", "\n", "Lastly, to facilitate analysis of different variants of the game, we parameterize\n", "the model in terms of fruit types, number of fruit and distance of the raven." ] }, { "cell_type": "markdown", "id": "238b0853", "metadata": {}, "source": [ "## Data structures with Stormvogel\n", "We start by importing the stormvogel library and additional Python libraries." ] }, { "cell_type": "code", "execution_count": 1, "id": "ed767efb", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.567352Z", "iopub.status.busy": "2026-03-26T10:39:31.567171Z", "iopub.status.idle": "2026-03-26T10:39:31.800964Z", "shell.execute_reply": "2026-03-26T10:39:31.800217Z" }, "lines_to_next_cell": 2 }, "outputs": [], "source": [ "# Imports\n", "import stormvogel\n", "\n", "from enum import Enum\n", "from copy import deepcopy" ] }, { "cell_type": "markdown", "id": "d42cf34d", "metadata": { "lines_to_next_cell": 2 }, "source": [ "We start the modelling by defining some general data structures for the Orchard game, for the different types of fruit `Fruit`, for the possible outcomes of the dice `DiceOutcome` and for the game state `GameState`." ] }, { "cell_type": "code", "execution_count": 2, "id": "1b9c0929", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.803328Z", "iopub.status.busy": "2026-03-26T10:39:31.803044Z", "iopub.status.idle": "2026-03-26T10:39:31.807296Z", "shell.execute_reply": "2026-03-26T10:39:31.806815Z" }, "lines_to_next_cell": 2 }, "outputs": [], "source": [ "# General data structures\n", "class Fruit(Enum):\n", " APPLE = \"🍏\"\n", " PEAR = \"🍐\"\n", " CHERRY = \"🍒\"\n", " PLUM = \"🍇\" # Use grape as there is no Emoji for plum\n", "\n", " def __str__(self):\n", " return self.value\n", "\n", "\n", "class DiceOutcome(Enum):\n", " FRUIT = \"🍉\"\n", " BASKET = \"🧺\"\n", " RAVEN = \"🐦‍⬛\"\n", "\n", " def __str__(self):\n", " return self.value\n", "\n", "\n", "class GameState(Enum):\n", " NOT_ENDED = 0\n", " PLAYERS_WON = 1\n", " RAVEN_WON = 2" ] }, { "cell_type": "markdown", "id": "2d89515d", "metadata": { "lines_to_next_cell": 2 }, "source": [ "We introduce a class `Orchard` which represents the current state of the game.\n", "This class inherits from the Stormvogel `State` class.\n", "The Orchard object is initialized with a list of configuration parameters such as the considered types of fruit `fruit_types`, the number of fruit per tree `num_fruits`, and the distance of the raven `raven_distance`.\n", "The game initializes the variable `trees` which keeps track of the remaining number of fruit per tree. It also keeps\n", "track of the outcome of the `dice` which can be either 🧺, 🐦‍⬛ or a fruit.\n", "In case of a fruit, the second entry of the dice tuple denotes the specific type of fruit which was thrown.\n", "Value `None` represents that the dice needs to be thrown first." ] }, { "cell_type": "code", "execution_count": 3, "id": "08a52241", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.809220Z", "iopub.status.busy": "2026-03-26T10:39:31.808998Z", "iopub.status.idle": "2026-03-26T10:39:31.816063Z", "shell.execute_reply": "2026-03-26T10:39:31.815431Z" } }, "outputs": [], "source": [ "# Main class for the orchard game\n", "class Orchard(stormvogel.bird.State):\n", " def __init__(self, fruit_types, num_fruits, raven_distance):\n", " self.trees = {fruit: num_fruits for fruit in fruit_types}\n", " self.raven = raven_distance\n", " self.dice = None\n", "\n", " def game_state(self):\n", " if all(self.is_tree_empty(tree) for tree in self.trees.keys()):\n", " assert self.raven > 0\n", " return GameState.PLAYERS_WON\n", " elif self.raven == 0:\n", " return GameState.RAVEN_WON\n", " else:\n", " return GameState.NOT_ENDED\n", "\n", " def is_tree_empty(self, tree):\n", " return self.trees[tree] == 0\n", "\n", " def pick_fruit(self, fruit):\n", " if self.trees[fruit] > 0:\n", " self.trees[fruit] -= 1\n", "\n", " def next_round(self):\n", " self.dice = None\n", "\n", " def move_raven(self):\n", " self.raven -= 1\n", "\n", " def __hash__(self):\n", " trees = [hash((f, n)) for f, n in self.trees.items()]\n", " return hash((tuple(trees), self.raven, self.dice))\n", "\n", " def label(self):\n", " if self.dice is None:\n", " # Output game state\n", " return str(self)\n", " else:\n", " if self.dice[0] == DiceOutcome.FRUIT:\n", " return \"🎲\" + str(self.dice[1])\n", " else:\n", " return \"🎲\" + str(self.dice[0])\n", "\n", " def __str__(self):\n", " s = \", \".join([\"{}{}\".format(n, f) for f, n in self.trees.items()])\n", " s += \", {}←{}\".format(self.raven, DiceOutcome.RAVEN)\n", " return s" ] }, { "cell_type": "markdown", "id": "7f652353", "metadata": {}, "source": [ "The Orchard class also defines various functions for ease of modeling.\n", "For instance, `game_state` returns whether the game is ongoing or who has won.\n", "Function `is_tree_empty` returns whether the tree for a given fruit type is contains no fruits anymore.\n", "Function `pick_fruit` picks the given fruit from the tree (if available).\n", "Function `next_round` resets the dice for the next round, `move_raven` moves the raven.\n", "Modeling these functions separately also yields a modular design which allows to easily modify specific behavior, such as the movement of the raven." ] }, { "cell_type": "markdown", "id": "9a98591e", "metadata": {}, "source": [ "An important aspect of the Orchard class is the hash function `__hash__`.\n", "The hash combines the number of left-over fruit per tree (via `self.trees.items()`), the position of the raven (`self.raven`) and the dice outcome (`self.dice`).\n", "All other information, for example whose turn it is, is deemed irrelevant to distinguish states.\n", "The hash function is crucial in reducing the size of the state space by only focusing on the relevant parts.\n", "If not explicitly given, the bird API hashes all members of a class, which could increase the state space." ] }, { "cell_type": "markdown", "id": "60820ae9", "metadata": {}, "source": [ "The function `label` is used to either output the current game state or the outcome of the dice.\n", "Lastly, we add a custom string representation `__str__`to nicely represent states." ] }, { "cell_type": "markdown", "id": "0a1eb95e", "metadata": {}, "source": [ "## Defining the Orchard MDP\n", "An MDP is represented by the tuple $\\mathcal{M} = (S, s_0, \\textit{Act}, \\mathbf{P}, AP, L)$ where\n", "- $S$ is a finite set of **states**\n", "- $s_0 \\in S$ is the **initial state**\n", "- $\\textit{Act}$ is a finite set of **actions**\n", "- $\\mathbf{P}: S \\times Act \\nrightarrow \\mathsf{Distr}(S)$ is the partial **transition function** mapping state-action pairs to distributions over successors\n", "- $AP$ is a finite set of **atomic propositions**\n", "- $L: S \\to 2^{AP}$ is the **labeling function**" ] }, { "cell_type": "markdown", "id": "ee5b8631", "metadata": {}, "source": [ "In order to create the MDP model of the Orchard game in Stormvogel, we need to provide all ingredients of the tuple in the following." ] }, { "cell_type": "markdown", "id": "09b293b2", "metadata": {}, "source": [ "### Initial state\n", "The initial state $s_0$ is given by the initialization of our `Orchard` class.\n", "At first, we use a smaller configuration of the game with only two different types of fruit, two pieces of fruit per tree, and a distance of two for the raven." ] }, { "cell_type": "code", "execution_count": 4, "id": "878e0540", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:31.818389Z", "iopub.status.busy": "2026-03-26T10:39:31.818133Z", "iopub.status.idle": "2026-03-26T10:39:31.821122Z", "shell.execute_reply": "2026-03-26T10:39:31.820599Z" }, "slideshow": { "slide_type": "" } }, "outputs": [], "source": [ "# Initialize the game\n", "init_small = Orchard([Fruit.APPLE, Fruit.CHERRY], num_fruits=2, raven_distance=2)" ] }, { "cell_type": "markdown", "id": "cb557f6f", "metadata": {}, "source": [ "Printing the initial state of the simplified game shows that there are two apples and two cherries on the trees, and the raven is two steps away from its goal." ] }, { "cell_type": "code", "execution_count": 5, "id": "22759724", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.823129Z", "iopub.status.busy": "2026-03-26T10:39:31.822909Z", "iopub.status.idle": "2026-03-26T10:39:31.826376Z", "shell.execute_reply": "2026-03-26T10:39:31.825820Z" }, "lines_to_next_cell": 2 }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "2🍏, 2🍒, 2←🐦‍⬛\n" ] } ], "source": [ "print(init_small)" ] }, { "cell_type": "markdown", "id": "1ef647e3", "metadata": { "lines_to_next_cell": 2 }, "source": [ "### Available actions\n", "The transition function returning successor states requires information which actions are enabled in each state. We define $\\textit{Act}(s)$ for any state $s$.\n", "In the Orchard game, we use the following actions:\n", "- `gameEnded`: the only action available once the game has ended. This action represents the self-loop for such final states.\n", "- `nextRound`: the dice must be thrown again.\n", "- `pickF`: the dice outcome is one of 🍏,🍐,🍒,🍇 and the player picks the corresponding fruit $F$ from the tree.\n", "- `chooseF`: the dice outcome is 🧺 and a fruit (🍏,🍐,🍒,🍇) is chosen.\n", "- `moveRaven`: the dice outcome is 🐦‍⬛ and the raven should be moved next." ] }, { "cell_type": "code", "execution_count": 6, "id": "ffc388c6", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:31.828479Z", "iopub.status.busy": "2026-03-26T10:39:31.828223Z", "iopub.status.idle": "2026-03-26T10:39:31.833413Z", "shell.execute_reply": "2026-03-26T10:39:31.832668Z" }, "lines_to_next_cell": 2, "slideshow": { "slide_type": "" } }, "outputs": [], "source": [ "# Define available actions\n", "def available_actions(state):\n", " if state.game_state() != GameState.NOT_ENDED:\n", " return [\"gameEnded\"]\n", " if state.dice is None:\n", " return [\"nextRound\"]\n", " if state.dice[0] == DiceOutcome.FRUIT:\n", " return [\"pick{}\".format(state.dice[1].name)]\n", " if state.dice[0] == DiceOutcome.BASKET:\n", " available_fruits = []\n", " # Choice over available fruits\n", " for fruit in state.trees.keys():\n", " if not state.is_tree_empty(fruit):\n", " available_fruits.append(fruit)\n", " return [\"choose{}\".format(fruit.name) for fruit in available_fruits]\n", " if state.dice[0] == DiceOutcome.RAVEN:\n", " return [\"moveRaven\"]\n", " assert False" ] }, { "cell_type": "markdown", "id": "50a0887e", "metadata": {}, "source": [ "For most states, a single action is available.\n", "The only exception is dice outcome 🧺, for which we list all fruit which are still available for choosing by the player." ] }, { "cell_type": "markdown", "id": "d52e0b9c", "metadata": { "lines_to_next_cell": 2 }, "source": [ "### Transition function\n", "Stormvogel defines the transition function $\\mathbf{P}$ via function `delta` which takes as arguments a state and an available action, and returns\n", "the distribution over successor states as a sparse list of nonzero transition probabilities for different target states." ] }, { "cell_type": "code", "execution_count": 7, "id": "b38b76c9", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:31.835824Z", "iopub.status.busy": "2026-03-26T10:39:31.835586Z", "iopub.status.idle": "2026-03-26T10:39:31.842668Z", "shell.execute_reply": "2026-03-26T10:39:31.842023Z" }, "lines_to_next_cell": 2, "slideshow": { "slide_type": "" } }, "outputs": [], "source": [ "# The transition function\n", "def delta(state, action):\n", " if state.game_state() != GameState.NOT_ENDED:\n", " assert action == \"gameEnded\"\n", " # Game has ended -> self loop\n", " return [(1, state)]\n", "\n", " if state.dice is None:\n", " assert action == \"nextRound\"\n", " # Player throws dice and considers outcomes\n", " outcomes = []\n", " # Probability of fair dice throw over\n", " # each fruit type + 1 basket + 1 raven\n", " fair_dice_prob = 1 / (len(state.trees.keys()) + 2)\n", "\n", " # 1. Dice shows fruit\n", " for fruit in state.trees.keys():\n", " next_state = deepcopy(state)\n", " next_state.dice = DiceOutcome.FRUIT, fruit\n", " outcomes.append((fair_dice_prob, next_state))\n", "\n", " # 2. Dice shows basket\n", " next_state = deepcopy(state)\n", " next_state.dice = DiceOutcome.BASKET, None\n", " outcomes.append((fair_dice_prob, next_state))\n", "\n", " # 3. Dice shows raven\n", " next_state = deepcopy(state)\n", " next_state.dice = DiceOutcome.RAVEN, None\n", " outcomes.append((fair_dice_prob, next_state))\n", "\n", " assert sum([o[0] for o in outcomes]) == 1\n", " return outcomes\n", "\n", " elif state.dice[0] == DiceOutcome.FRUIT:\n", " assert action.startswith(\"pick\")\n", " # Player picks specified fruit\n", " fruit = state.dice[1]\n", " next_state = deepcopy(state)\n", " next_state.pick_fruit(fruit)\n", " next_state.next_round()\n", " return [(1, next_state)]\n", "\n", " elif state.dice[0] == DiceOutcome.BASKET:\n", " assert action.startswith(\"choose\")\n", " # Player chooses fruit specified by action\n", " fruit = Fruit[action.removeprefix(\"choose\")]\n", " next_state = deepcopy(state)\n", " next_state.pick_fruit(fruit)\n", " next_state.next_round()\n", " return [(1, next_state)]\n", "\n", " elif state.dice[0] == DiceOutcome.RAVEN:\n", " assert action == \"moveRaven\"\n", " next_state = deepcopy(state)\n", " next_state.move_raven()\n", " next_state.next_round()\n", " return [(1, next_state)]\n", "\n", " assert False" ] }, { "cell_type": "markdown", "id": "b91de929", "metadata": {}, "source": [ "If the game has ended, we add a self-loop to the same state with probability one.\n", "Otherwise, we perform each round in two phases:\n", "first throwing the dice and then acting on the outcome. These are two separate\n", "transitions in the model.\n", "\n", "In the first phase, the dice outcome is `None` and the player needs to throw\n", "the dice. We need to consider the outcomes for the different fruit types plus two\n", "additional outcomes 🧺 and 🐦‍⬛. Each outcome has the same uniform probability\n", "`fair_dice_prob`, which is `1 / (len(state.trees.keys()) + 2)`.\n", "The rest of the first phase creates the different successor states depending on the dice outcomes.\n", "To this end, we create the next_state as a copy of the current state, and set the dice outcome\n", "`next_state.dice`.\n", "Afterwards, we store the successor state together with the\n", "corresponding probability in the list outcomes of successor states.\n", "\n", "The remainder of the `delta` function handles the second phase, where the player\n", "acts depending on the dice outcome `state.dice`.\n", "If the dice outcome is a fruit,\n", "the player performs `pick_fruit(fruit)` on the next_state and then finishes\n", "the turn with `next_round`.\n", "If the dice outcome is 🧺, the player needs to choose\n", "a fruit. This choice is modeled by the different available actions `chooseF` in this\n", "state. Based on the chosen `action` given as argument to the `delta` function, we\n", "can extract the chosen fruit. For example, action name `chooseAPPLE` corresponds\n", "to 🍏. In the successor state, we pick the chosen fruit and then continue with\n", "the next round.\n", "\n", "Lastly, if dice outcome is 🐦‍⬛, the raven moves." ] }, { "cell_type": "markdown", "id": "1628963d", "metadata": { "lines_to_next_cell": 2 }, "source": [ "### Labeling\n", "We use a labeling $L$ to associate atomic propositions $AP$ to states\n", "which satisfy them. These labels help identify states which fulfill a certain property which is relevant to our analysis.\n", "\n", "In Stormvogel, the function `labels()` returns a list of atomic propositions\n", "per state. As we are mainly interested in the winner of a game, we introduce\n", "two labels `\"PlayersWon\"` and `\"RavenWon'` which mark each state with the party who won.\n", "We also label each state with the string representation of the game state (`state.label()`) to help understanding and investigating the resulting model as the internals of a state become visible.\n", "For scalable analysis, such kind of internal information is typically omitted in the final version of a model." ] }, { "cell_type": "code", "execution_count": 8, "id": "e54cb18e", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.845248Z", "iopub.status.busy": "2026-03-26T10:39:31.845021Z", "iopub.status.idle": "2026-03-26T10:39:31.848353Z", "shell.execute_reply": "2026-03-26T10:39:31.847805Z" }, "lines_to_next_cell": 2 }, "outputs": [], "source": [ "# Add labels for game state\n", "def labels(state):\n", " labels = [state.label()]\n", " if state.game_state() == GameState.PLAYERS_WON:\n", " labels.append(\"PlayersWon\")\n", " elif state.game_state() == GameState.RAVEN_WON:\n", " labels.append(\"RavenWon\")\n", " return labels" ] }, { "cell_type": "markdown", "id": "bdc9d5cb", "metadata": { "lines_to_next_cell": 2 }, "source": [ "### Rewards\n", "Lastly, we specify **rewards** (also called costs).\n", "A model can have multiple reward structures that each associate rewards to states (or to state-action pairs).\n", "Visiting a state or action accumulates the associated rewards.\n", "As example, we define a reward that counts the number of rounds.\n", "Every state in which the dice is thrown (`state.dice is None`) is associated with one additional round of the game. All other states have reward zero." ] }, { "cell_type": "code", "execution_count": 9, "id": "8defb2b3", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:31.850220Z", "iopub.status.busy": "2026-03-26T10:39:31.850034Z", "iopub.status.idle": "2026-03-26T10:39:31.853052Z", "shell.execute_reply": "2026-03-26T10:39:31.852561Z" }, "slideshow": { "slide_type": "" } }, "outputs": [], "source": [ "# Reward function\n", "def rewards(state):\n", " if state.game_state() == GameState.NOT_ENDED:\n", " if state.dice is None:\n", " return {\"rounds\": 1}\n", " return {\"rounds\": 0}" ] }, { "cell_type": "markdown", "id": "73ce557c", "metadata": {}, "source": [ "## Building the models\n", "All ingredients for the model have been specified and we can finally build the MDP model for the Orchard game.\n", "The function specifies the type of model (MDP here) and the MDP tuple entries we defined before." ] }, { "cell_type": "code", "execution_count": 10, "id": "0740fa83", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:31.854903Z", "iopub.status.busy": "2026-03-26T10:39:31.854722Z", "iopub.status.idle": "2026-03-26T10:39:31.864943Z", "shell.execute_reply": "2026-03-26T10:39:31.864454Z" }, "slideshow": { "slide_type": "" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "ModelType.MDP model with 90 states, 98 choices, and 33 distinct labels.\n" ] } ], "source": [ "# Build the simple orchard model\n", "orchard_simple = stormvogel.bird.build_bird(\n", " modeltype=stormvogel.ModelType.MDP,\n", " init=init_small,\n", " available_actions=available_actions,\n", " delta=delta,\n", " labels=labels,\n", " rewards=rewards,\n", ")\n", "\n", "print(orchard_simple.summary())" ] }, { "cell_type": "markdown", "id": "496cdee2", "metadata": {}, "source": [ "We see that we built an MDP model with 90 states." ] }, { "cell_type": "markdown", "id": "d3fa7bca", "metadata": {}, "source": [ "We can also easily build the full model by configuring the initial state `init_game` accordingly and calling `build_bird()` as before.\n", "Note that we need to increase the `max_size` of the explored state space as the resulting model has around $22,500$ states." ] }, { "cell_type": "code", "execution_count": 11, "id": "a55b7b90", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:31.866872Z", "iopub.status.busy": "2026-03-26T10:39:31.866679Z", "iopub.status.idle": "2026-03-26T10:39:33.763484Z", "shell.execute_reply": "2026-03-26T10:39:33.762889Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "ModelType.MDP model with 22469 states, 29349 choices, and 3 distinct labels.\n" ] } ], "source": [ "# Build the full model\n", "init_game = Orchard(\n", " [Fruit.APPLE, Fruit.CHERRY, Fruit.PEAR, Fruit.PLUM], num_fruits=4, raven_distance=5\n", ")\n", "\n", "\n", "# For the full model, we only set the relevant labels for the winning conditions\n", "# and do not expose the internal state information\n", "def labels_full(state):\n", " labels = []\n", " if state.game_state() == GameState.PLAYERS_WON:\n", " labels.append(\"PlayersWon\")\n", " elif state.game_state() == GameState.RAVEN_WON:\n", " labels.append(\"RavenWon\")\n", " return labels\n", "\n", "\n", "orchard = stormvogel.bird.build_bird(\n", " modeltype=stormvogel.ModelType.MDP,\n", " init=init_game,\n", " available_actions=available_actions,\n", " delta=delta,\n", " labels=labels_full,\n", " rewards=rewards,\n", " max_size=100000,\n", ")\n", "\n", "print(orchard.summary())" ] }, { "cell_type": "markdown", "id": "455ac71c", "metadata": {}, "source": [ "Some of the analyses in the following require a representation of the Orchard model in Storm data structures.\n", "We can simply translate the model via `stormvogel_to_stormpy`." ] }, { "cell_type": "code", "execution_count": 12, "id": "ce4e3020", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:33.765465Z", "iopub.status.busy": "2026-03-26T10:39:33.765237Z", "iopub.status.idle": "2026-03-26T10:39:34.238920Z", "shell.execute_reply": "2026-03-26T10:39:34.238250Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "-------------------------------------------------------------- \n", "Model type: \tMDP (sparse)\n", "States: \t22469\n", "Transitions: \t44949\n", "Choices: \t29349\n", "Reward Models: rounds\n", "State Labels: \t3 labels\n", " * PlayersWon -> 5 item(s)\n", " * RavenWon -> 624 item(s)\n", " * init -> 1 item(s)\n", "Choice Labels: \t11 labels\n", " * pickPLUM -> 3120 item(s)\n", " * choosePLUM -> 2500 item(s)\n", " * gameEnded -> 629 item(s)\n", " * pickCHERRY -> 3120 item(s)\n", " * chooseCHERRY -> 2500 item(s)\n", " * choosePEAR -> 2500 item(s)\n", " * pickPEAR -> 3120 item(s)\n", " * moveRaven -> 3120 item(s)\n", " * chooseAPPLE -> 2500 item(s)\n", " * nextRound -> 3120 item(s)\n", " * pickAPPLE -> 3120 item(s)\n", "-------------------------------------------------------------- \n", "\n" ] } ], "source": [ "# Stormpy model\n", "import stormpy\n", "\n", "orchard_storm = stormvogel.mapping.stormvogel_to_stormpy(orchard)\n", "print(orchard_storm)" ] }, { "cell_type": "markdown", "id": "fcbbfb66", "metadata": {}, "source": [ "## Defining the MDP in the Prism language\n", "We showed how to create an MDP model via Stormvogel.\n", "Storm also supports creating models from other input formats such as the [Prism language](https://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction) or the [JANI interchange format](https://jani-spec.org/).\n", "Here, we also provide a Prism model for our Orchard game. The specification is given in `orchard/orchard_stormvogel.pm` and we print it here." ] }, { "cell_type": "code", "execution_count": 13, "id": "a1f79b9a", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:34.240922Z", "iopub.status.busy": "2026-03-26T10:39:34.240741Z", "iopub.status.idle": "2026-03-26T10:39:34.375996Z", "shell.execute_reply": "2026-03-26T10:39:34.375381Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "// Orchard (Obstgarten) kid's game\r\n", "// Corresponds exactly to the Stormvogel model\r\n", "mdp\r\n", "\r\n", "// constants\r\n", "const int NUM_FRUIT; //=10; // Number of fruits per fruit type\r\n", "const int DISTANCE_RAVEN; //=9; // Distance of raven from orchard\r\n", "const double probRaven = 1/6;\r\n", "const double probBucket = 1/6;\r\n", "const double probFruit = 1 - probRaven - probBucket;\r\n", "\r\n", "// Module for the player\r\n", "module player0\r\n", "\t// Game states of the player\r\n", "\t// s=0 : roll dice\r\n", "\t// s=1 : perform action (pick fruit, choose fruit for 'bucket', move raven)\r\n", "\ts : [0..1] init 0;\r\n", "\t// Dice outcome\r\n", "\t// 0: not thrown, 1: apple, 2:pear, 3:cherry, 4:plum, 5:bucket, 6:raven\r\n", "\td : [0..6] init 1;\r\n", "\r\n", "\t// Perform actions\r\n", "\t// Throw dice\r\n", "\t[nextRound] (s=0) & (!game_ended) -> 1/4 * probFruit : (s'=1) & (d'=1)\r\n", "\t + 1/4 * probFruit : (s'=1) & (d'=2)\r\n", "\t + 1/4 * probFruit : (s'=1) & (d'=3)\r\n", "\t + 1/4 * probFruit : (s'=1) & (d'=4)\r\n", "\t + probBucket : (s'=1) & (d'=5)\r\n", "\t + probRaven : (s'=1) & (d'=6)\r\n", "\t ;\r\n", "\t[nextRound] (s=0) & ( game_ended) -> 1: true;\r\n", "\r\n", "\t// Pick fruit\r\n", "\t[pickAPPLE] (s=1) & (d=1) -> 1: (s'=0) & (d'=0);\r\n", "\t[pickPEAR] (s=1) & (d=2) -> 1: (s'=0) & (d'=0);\r\n", "\t[pickCHERRY] (s=1) & (d=3) -> 1: (s'=0) & (d'=0);\r\n", "\t[pickPLUM] (s=1) & (d=4) -> 1: (s'=0) & (d'=0);\r\n", "\r\n", "\t// Choose fruit (because of 'bucket')\r\n", "\t[chooseAPPLE] (s=1) & (d=5) -> 1 : (s'=0) & (d'=0);\r\n", "\t[choosePEAR] (s=1) & (d=5) -> 1 : (s'=0) & (d'=0);\r\n", "\t[chooseCHERRY] (s=1) & (d=5) -> 1 : (s'=0) & (d'=0);\r\n", "\t[choosePLUM] (s=1) & (d=5) -> 1 : (s'=0) & (d'=0);\r\n", "\t// No fruit can be chosen\r\n", "\t[nochoice] (s=1) & (d=5) & (all_trees_empty)\r\n", "\t\t -> 1 : (s'=0) & (d'=0);\r\n", "\r\n", "\t// Move raven\r\n", "\t[moveRaven] (s=1) & (d=6) -> 1 : (s'=0) & (d'=0);\r\n", "endmodule\r\n", "\r\n", "// Module for the orchard with the trees\r\n", "module orchard\r\n", "\t// Fruits\r\n", "\tapple : [0..NUM_FRUIT] init NUM_FRUIT;\r\n", "\tpear : [0..NUM_FRUIT] init NUM_FRUIT;\r\n", "\tcherry : [0..NUM_FRUIT] init NUM_FRUIT;\r\n", "\tplum : [0..NUM_FRUIT] init NUM_FRUIT;\r\n", "\r\n", "\t// Pick fruit\r\n", "\t[pickAPPLE] (apple>0) -> 1: (apple'=apple-1);\r\n", "\t[pickAPPLE] (apple=0) -> 1: true;\r\n", "\t[pickPEAR] (pear>0) -> 1: (pear'=pear-1);\r\n", "\t[pickPEAR] (pear=0) -> 1: true;\r\n", "\t[pickCHERRY] (cherry>0) -> 1: (cherry'=cherry-1);\r\n", "\t[pickCHERRY] (cherry=0) -> 1: true;\r\n", "\t[pickPLUM] (plum>0) -> 1: (plum'=plum-1);\r\n", "\t[pickPLUM] (plum=0) -> 1: true;\r\n", "\r\n", "\t// Choose fruit\r\n", "\t[chooseAPPLE] (apple>0) -> 1: (apple'=apple-1);\r\n", "\t[choosePEAR] (pear>0) -> 1: (pear'=pear-1);\r\n", "\t[chooseCHERRY] (cherry>0) -> 1: (cherry'=cherry-1);\r\n", "\t[choosePLUM] (plum>0) -> 1: (plum'=plum-1);\r\n", "\t[noChoice] (all_trees_empty) -> 1: true;\r\n", "endmodule\r\n", "\r\n", "// Module for the raven\r\n", "module raven\r\n", "\t// Raven\r\n", "\traven : [0..DISTANCE_RAVEN] init DISTANCE_RAVEN;\r\n", "\r\n", "\t// Move raven\r\n", "\t[moveRaven] (raven>0) -> 1 : (raven'=raven-1);\r\n", "\t[moveRaven] (raven=0) -> 1 : true;\r\n", "endmodule\r\n", "\r\n", "// labels\r\n", "formula all_trees_empty = apple = 0\r\n", " & pear = 0\r\n", " & cherry = 0\r\n", " & plum = 0\r\n", " ;\r\n", "formula game_ended = all_trees_empty | raven = 0;\r\n", "label \"PlayersWon\" = all_trees_empty & raven > 0;\r\n", "label \"RavenWon\" = !all_trees_empty & raven = 0;\r\n", "label \"AllCherriesPicked\" = cherry = 0 & raven > 0;\r\n", "label \"RavenOneAway\" = raven = 1;\r\n", "\r\n", "// rewards\r\n", "rewards \"rounds\"\r\n", "\ts=0 : 1;\r\n", "endrewards\r\n" ] } ], "source": [ "# Print the Prism model\n", "!cat orchard/orchard_stormvogel.pm" ] }, { "cell_type": "markdown", "id": "5eae8180", "metadata": {}, "source": [ "The Prism specification follows the same structure as the Stormvogel model.\n", "It can be configured via global constants such as `NUM_FRUIT` and `DISTANCE_RAVEN`.\n", "The current game state is represented by variables such as `raven` or `apple`.\n", "\n", "The Prism specification can be built via stormpy." ] }, { "cell_type": "code", "execution_count": 14, "id": "db8f3cb0", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:39:34.378278Z", "iopub.status.busy": "2026-03-26T10:39:34.378079Z", "iopub.status.idle": "2026-03-26T10:39:34.489373Z", "shell.execute_reply": "2026-03-26T10:39:34.488835Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Model with 22469 states and 44954 transitions\n" ] } ], "source": [ "# Build the prism model\n", "prism_program = stormpy.parse_prism_program(\"orchard/orchard_stormvogel.pm\")\n", "constants = \"NUM_FRUIT=4, DISTANCE_RAVEN=5\"\n", "prism_program = stormpy.preprocess_symbolic_input(prism_program, [], constants)[\n", " 0\n", "].as_prism_program()\n", "options = stormpy.BuilderOptions()\n", "options.set_build_state_valuations()\n", "options.set_build_choice_labels()\n", "options.set_build_with_choice_origins()\n", "orchard_prism = stormpy.build_sparse_model_with_options(prism_program, options)\n", "print(\n", " \"Model with {} states and {} transitions\".format(\n", " orchard_prism.nr_states, orchard_prism.nr_transitions\n", " )\n", ")" ] }, { "cell_type": "markdown", "id": "c7927c41", "metadata": {}, "source": [ "We can see that the model from the Prism specification has the same number of states than the model defined via Stormvogel." ] }, { "cell_type": "markdown", "id": "6a8dd366", "metadata": {}, "source": [ "## Model inspection\n", "Before applying model checking, we inspect the model to spot potential modelling issues.\n", "Stormvogel visualizes the model with `stormvogel.show(orchard_simple)`.\n", "\n", "The interactive visualization is based on JavaScript and can be seen directly in this notebook when executing the command below.\n", "Note that the visualization might take a couple of seconds to load.\n", "\n", "Note that a potential warning of the form `Test request failed` can be safely ignored." ] }, { "cell_type": "code", "execution_count": 15, "id": "5250f8d8", "metadata": { "editable": true, "execution": { "iopub.execute_input": "2026-03-26T10:39:34.491201Z", "iopub.status.busy": "2026-03-26T10:39:34.491024Z", "iopub.status.idle": "2026-03-26T10:39:34.700514Z", "shell.execute_reply": "2026-03-26T10:39:34.699894Z" }, "slideshow": { "slide_type": "" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# Visualize\n", "vis = stormvogel.show(orchard_simple)" ] }, { "cell_type": "markdown", "id": "692d961e", "metadata": {}, "source": [ "One can zoom in/out as usual, and move the viewpoint by dragging the view.\n", "Elements are automatically arranged but can also be dragged.\n", "\n", "States are depicted as ellipses, actions by blue boxes and transitions by arrows.\n", "Labels are given inside the states and actions, and the rewards are indicated by the € symbol.\n", "\n", "The initial state should be visible on the right hand side and is the only state with the additional label `init`.\n", "Starting from this initial state, the only possible action is `nextRound`, which corresponds to throwing the dice. It has reward one.\n", "The four outcomes are depicted by the four successor states with symbol 🎲 and are each\n", "reached with transition probability $\\frac{1}{4}$.\n", "Afterwards, the corresponding action can be performed. For example, from state 🎲🍏, action `pickAPPLE` is possible and\n", "leads to a state 1🍏, 2🍒, 2←🐦‍⬛ where only one apple is remaining." ] } ], "metadata": { "kernelspec": { "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.12.13" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "1532bb462d21418c97f3b0be047e7cbc": { "model_module": "@jupyter-widgets/base", "model_module_version": "2.0.0", "model_name": "LayoutModel", "state": { "_model_module": "@jupyter-widgets/base", "_model_module_version": "2.0.0", "_model_name": "LayoutModel", "_view_count": null, "_view_module": "@jupyter-widgets/base", "_view_module_version": "2.0.0", "_view_name": "LayoutView", "align_content": null, "align_items": null, "align_self": null, "border_bottom": null, "border_left": null, "border_right": null, "border_top": null, "bottom": null, "display": null, "flex": null, "flex_flow": null, "grid_area": null, "grid_auto_columns": null, "grid_auto_flow": null, "grid_auto_rows": null, "grid_column": null, "grid_gap": null, "grid_row": null, "grid_template_areas": null, "grid_template_columns": null, "grid_template_rows": null, "height": null, "justify_content": null, "justify_items": null, "left": null, "margin": null, "max_height": null, "max_width": null, "min_height": null, "min_width": null, "object_fit": null, "object_position": null, "order": null, "overflow": null, "padding": null, "right": null, "top": null, "visibility": null, "width": null } }, "1d27c06143ee476c89371adb6c00bd6b": { "model_module": "@jupyter-widgets/base", "model_module_version": "2.0.0", "model_name": "LayoutModel", "state": { "_model_module": "@jupyter-widgets/base", "_model_module_version": "2.0.0", "_model_name": "LayoutModel", "_view_count": null, "_view_module": "@jupyter-widgets/base", "_view_module_version": "2.0.0", "_view_name": "LayoutView", "align_content": null, "align_items": null, "align_self": null, "border_bottom": null, "border_left": null, "border_right": null, "border_top": null, "bottom": null, "display": null, "flex": null, "flex_flow": null, "grid_area": null, "grid_auto_columns": null, "grid_auto_flow": null, "grid_auto_rows": null, "grid_column": null, "grid_gap": null, "grid_row": null, "grid_template_areas": null, "grid_template_columns": null, "grid_template_rows": null, "height": null, "justify_content": null, "justify_items": null, "left": null, "margin": null, "max_height": null, "max_width": null, "min_height": null, "min_width": null, "object_fit": null, "object_position": null, "order": null, "overflow": null, "padding": null, "right": null, "top": null, "visibility": null, "width": null } }, "5e44cc14ef7b49ebbbbedb60b67a1486": { "model_module": "@jupyter-widgets/output", "model_module_version": "1.0.0", "model_name": "OutputModel", "state": { "_dom_classes": [], "_model_module": "@jupyter-widgets/output", "_model_module_version": "1.0.0", "_model_name": "OutputModel", "_view_count": null, "_view_module": "@jupyter-widgets/output", "_view_module_version": "1.0.0", "_view_name": "OutputView", "layout": "IPY_MODEL_1d27c06143ee476c89371adb6c00bd6b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "a5e30ed4664e4ccf9e821906116e0d48": { "model_module": "@jupyter-widgets/output", "model_module_version": "1.0.0", "model_name": "OutputModel", "state": { "_dom_classes": [], "_model_module": "@jupyter-widgets/output", "_model_module_version": "1.0.0", "_model_name": "OutputModel", "_view_count": null, "_view_module": "@jupyter-widgets/output", "_view_module_version": "1.0.0", "_view_name": "OutputView", "layout": "IPY_MODEL_1532bb462d21418c97f3b0be047e7cbc", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }