{ "cells": [ { "cell_type": "markdown", "id": "3396690e", "metadata": {}, "source": [ "# Parametric models\n", "Instead of setting numeric values as transition probabilities, we may also use parameters, polynomials or even rational functions in multiple variables." ] }, { "cell_type": "code", "execution_count": 1, "id": "9a28976b", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:19.802219Z", "iopub.status.busy": "2026-03-26T10:47:19.801987Z", "iopub.status.idle": "2026-03-26T10:47:19.994905Z", "shell.execute_reply": "2026-03-26T10:47:19.994272Z" } }, "outputs": [], "source": [ "from stormvogel import parametric" ] }, { "cell_type": "markdown", "id": "c72114b8", "metadata": {}, "source": [ "Polynomials are represented as dictionaries where the keys are the exponents and the values are coefficients. In addition, we must also supply a list of variable names. Rational functions are then represented as a pair of two polynomials (numerator and denominator)." ] }, { "cell_type": "code", "execution_count": 2, "id": "5132c171", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:19.997206Z", "iopub.status.busy": "2026-03-26T10:47:19.996966Z", "iopub.status.idle": "2026-03-26T10:47:20.000883Z", "shell.execute_reply": "2026-03-26T10:47:20.000424Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "x^2 + y^2\n", "2.0*1 + z + 6.0*z^3\n", "(x^2 + y^2)/(2.0*1 + z + 6.0*z^3)\n" ] } ], "source": [ "polynomial1 = parametric.Polynomial([\"x\", \"y\"])\n", "polynomial1.add_term((2, 0), 1)\n", "polynomial1.add_term((0, 2), 1)\n", "\n", "print(polynomial1)\n", "\n", "polynomial2 = parametric.Polynomial([\"z\"])\n", "polynomial2.add_term((0,), 2)\n", "polynomial2.add_term((1,), 1)\n", "polynomial2.add_term((3,), 6)\n", "\n", "print(polynomial2)\n", "\n", "rational_function = parametric.RationalFunction(polynomial1, polynomial2)\n", "\n", "print(rational_function)" ] }, { "cell_type": "markdown", "id": "b9784951", "metadata": {}, "source": [ "To create a parametric model (e.g. pmc or pmdp) we simply have to set such a value as a transition probability. As an example, we provide the knuth yao dice, but with parameters instead of concrete probabilities." ] }, { "cell_type": "code", "execution_count": 3, "id": "d7b8dc31", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:20.002536Z", "iopub.status.busy": "2026-03-26T10:47:20.002377Z", "iopub.status.idle": "2026-03-26T10:47:20.208604Z", "shell.execute_reply": "2026-03-26T10:47:20.208032Z" } }, "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": [ "from stormvogel import model, bird\n", "from stormvogel.show import show\n", "\n", "# we first make polynomials 'x' and '1-x'\n", "x = parametric.Polynomial([\"x\"])\n", "x.add_term((1,), 1)\n", "\n", "invx = parametric.Polynomial([\"x\"])\n", "invx.add_term((1,), -1)\n", "invx.add_term((0,), 1)\n", "\n", "\n", "# we build the knuth yao dice using the bird model builder\n", "def delta(\n", " s: bird.State,\n", ") -> list[tuple[float | parametric.Polynomial, bird.State]] | None:\n", " match s.s:\n", " case 0:\n", " return [(x, bird.State(s=1)), (invx, bird.State(s=2))]\n", " case 1:\n", " return [(x, bird.State(s=3)), (invx, bird.State(s=4))]\n", " case 2:\n", " return [(x, bird.State(s=5)), (invx, bird.State(s=6))]\n", " case 3:\n", " return [(x, bird.State(s=1)), (invx, bird.State(s=7, d=1))]\n", " case 4:\n", " return [\n", " (x, bird.State(s=7, d=2)),\n", " (invx, bird.State(s=7, d=3)),\n", " ]\n", " case 5:\n", " return [\n", " (x, bird.State(s=7, d=4)),\n", " (invx, bird.State(s=7, d=5)),\n", " ]\n", " case 6:\n", " return [(x, bird.State(s=2)), (invx, bird.State(s=7, d=6))]\n", " case 7:\n", " return [(1, s)]\n", "\n", "\n", "def labels(s: bird.State):\n", " if s.s == 7:\n", " return f\"rolled{str(s.d)}\"\n", "\n", "\n", "knuth_yao_pmc = bird.build_bird(\n", " delta=delta,\n", " init=bird.State(s=0),\n", " labels=labels,\n", " modeltype=model.ModelType.DTMC,\n", ")\n", "\n", "vis = show(knuth_yao_pmc)" ] }, { "cell_type": "markdown", "id": "007908f1", "metadata": {}, "source": [ "We can now evaluate the model by assigning the variable x to any concrete value. This induces a regular dtmc with fixed probabilities." ] }, { "cell_type": "code", "execution_count": 4, "id": "a1d86378", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:20.215863Z", "iopub.status.busy": "2026-03-26T10:47:20.215564Z", "iopub.status.idle": "2026-03-26T10:47:20.244835Z", "shell.execute_reply": "2026-03-26T10:47:20.244262Z" } }, "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": [ "p = 1 / 2\n", "\n", "\n", "eval_knuth_yao_pmc = knuth_yao_pmc.parameter_valuation({\"x\": p})\n", "vis = show(eval_knuth_yao_pmc)" ] }, { "cell_type": "markdown", "id": "289206e7", "metadata": {}, "source": [ "# Interval Models\n", "We can also set an interval between two values x and y as transition value, meaning that we don't know the probability precisely, but we know it is between x and y. We represent intervals using a class in model.py, where we have two attributes: bottom and top. Both of these should be an element of type Number, i.e., int, float or fraction." ] }, { "cell_type": "code", "execution_count": 5, "id": "23607e4b", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:20.251793Z", "iopub.status.busy": "2026-03-26T10:47:20.251623Z", "iopub.status.idle": "2026-03-26T10:47:20.254744Z", "shell.execute_reply": "2026-03-26T10:47:20.254251Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[0.3333333333333333,0.6666666666666666]\n" ] } ], "source": [ "interval = model.Interval(1 / 3, 2 / 3)\n", "print(interval)" ] }, { "cell_type": "markdown", "id": "9cb7e964", "metadata": {}, "source": [ "Similar to parametric models, creating an interval model is as straightforward as just setting some interval objects as transition values." ] }, { "cell_type": "code", "execution_count": 6, "id": "9d24618e", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:20.256426Z", "iopub.status.busy": "2026-03-26T10:47:20.256232Z", "iopub.status.idle": "2026-03-26T10:47:20.288570Z", "shell.execute_reply": "2026-03-26T10:47:20.287977Z" } }, "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": [ "from stormvogel import bird\n", "from stormvogel.show import show\n", "\n", "# We create our interval values\n", "interval = model.Interval(2 / 7, 6 / 7)\n", "inv_interval = model.Interval(1 / 7, 5 / 7)\n", "\n", "\n", "# we build the knuth yao dice using the bird model builder\n", "def delta(s: bird.State) -> list[tuple[float | model.Interval, bird.State]] | None:\n", " match s.s:\n", " case 0:\n", " return [(interval, bird.State(s=1)), (inv_interval, bird.State(s=2))]\n", " case 1:\n", " return [(interval, bird.State(s=3)), (inv_interval, bird.State(s=4))]\n", " case 2:\n", " return [(interval, bird.State(s=5)), (inv_interval, bird.State(s=6))]\n", " case 3:\n", " return [(interval, bird.State(s=1)), (inv_interval, bird.State(s=7, d=1))]\n", " case 4:\n", " return [\n", " (interval, bird.State(s=7, d=2)),\n", " (invx, bird.State(s=7, d=3)),\n", " ]\n", " case 5:\n", " return [\n", " (interval, bird.State(s=7, d=4)),\n", " (invx, bird.State(s=7, d=5)),\n", " ]\n", " case 6:\n", " return [(interval, bird.State(s=2)), (inv_interval, bird.State(s=7, d=6))]\n", " case 7:\n", " return [(1, s)]\n", "\n", "\n", "def labels(s: bird.State):\n", " if s.s == 7:\n", " return f\"rolled{str(s.d)}\"\n", "\n", "\n", "knuth_yao_imc = bird.build_bird(\n", " delta=delta,\n", " init=bird.State(s=0),\n", " labels=labels,\n", " modeltype=model.ModelType.DTMC,\n", ")\n", "\n", "vis = show(knuth_yao_imc)" ] }, { "cell_type": "code", "execution_count": null, "id": "2f4354ad", "metadata": {}, "outputs": [], "source": [] } ], "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": { "2c128e07521548e8b1942f273b41c7ce": { "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_df33acfe479747b592e723f4f225dc46", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "38b9732d4fe8479d886f7ba8cd0ad9ca": { "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_da40f7c922054f1ba7799533fcbdddc7", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4debe367d5e54c67846a56b186372ad6": { "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_860a40f3901e4c90b4693cdf49005d52", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "633ff41d3c4b49f488dc1f18abb6432d": { "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_94cdb7fbba304a8890a5ffe9e7f75905", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7300cef66c3b4cae9afbca39da78aced": { "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 } }, "860a40f3901e4c90b4693cdf49005d52": { "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 } }, "94cdb7fbba304a8890a5ffe9e7f75905": { "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 } }, "d284c48220034be8b57cdc9e3fc22d3e": { "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_7300cef66c3b4cae9afbca39da78aced", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "da40f7c922054f1ba7799533fcbdddc7": { "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 } }, "ddc44a9d81924910b2635e62338be7c0": { "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_f0542684af944fd2b4cec8603597f005", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "df33acfe479747b592e723f4f225dc46": { "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 } }, "f0542684af944fd2b4cec8603597f005": { "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 } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }