Parse PRISM in notebook (#35)

* Parse PRISM in notebook

* Print model in notebook

* Check whether we are in notebook in __init__

---------

Co-authored-by: Linus Heck <[email protected]>

docs/getting_started/prism.ipynb

@@ -0,0 +1,158 @@
+{
+  "cells": [
+    {
+      "cell_type": "code",
+      "execution_count": 8,
+      "id": "2552891a-8d96-4c77-aa97-0a1ddf5bc02b",
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "import stormvogel\n",
+        "import stormpy"
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": 9,
+      "id": "a00a5906-af87-4fb8-8f5f-ad5690129d33",
+      "metadata": {},
+      "outputs": [
+        {
+          "data": {
+            "text/plain": [
+              "<stormpy.storage.storage.PrismProgram at 0x104a1c370>"
+            ]
+          },
+          "execution_count": 9,
+          "metadata": {},
+          "output_type": "execute_result"
+        }
+      ],
+      "source": [
+        "%%prism nand\n",
+        "dtmc\n",
+        "\n",
+        "const int N = 5; // number of inputs in each bundle\n",
+        "const int K = 2; // number of restorative stages\n",
+        "\n",
+        "const int M = 2*K+1; // total number of multiplexing units\n",
+        "\n",
+        "const double perr = 0.02; // probability nand works correctly\n",
+        "const double prob1 = 0.9; // probability initial inputs are stimulated\n",
+        "\n",
+        "module multiplex\n",
+        "\n",
+        "\tu : [1..M]; // number of stages\n",
+        "\tc : [0..N]; // counter (number of copies of the nand done)\n",
+        "\n",
+        "\ts : [0..4]; // local state\n",
+        "\t// 0 - initial state\n",
+        "\t// 1 - set x inputs\n",
+        "\t// 2 - set y inputs\n",
+        "\t// 3 - set outputs\n",
+        "\t// 4 - done\n",
+        "\n",
+        "\tz : [0..N]; // number of new outputs equal to 1\n",
+        "\tzx : [0..N]; // number of old outputs equal to 1\n",
+        "\tzy : [0..N]; // need second copy for y\n",
+        "\t// initially 9 since initially probability of stimulated state is 0.9\n",
+        "\n",
+        "\tx : [0..1]; // value of first input\n",
+        "\ty : [0..1]; // value of second input\n",
+        "\t\n",
+        "\t[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet\n",
+        "\t[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished\n",
+        "\t[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)\n",
+        "\n",
+        "\t// choose x permute selection (have zx stimulated inputs)\n",
+        "\t// note only need y to be random\t\n",
+        "\t[] s=1 & u=1  -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random\n",
+        "\t[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);\n",
+        "\t[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);\n",
+        "\n",
+        "\t// choose x randomly from selection (have zy stimulated inputs)\n",
+        "\t[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random\n",
+        "\t[] s=2 & u>1 & zy<(N-c) & zy>0  -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);\n",
+        "\t[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);\n",
+        "\t[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);\n",
+        "\n",
+        "\t// use nand gate\n",
+        "\t[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty\n",
+        "\t         + perr    : (z'=z+(x*y))    & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault\n",
+        "\t\n",
+        "\t[] s=4 -> (s'=s);\n",
+        "\t\n",
+        "endmodule\n",
+        "\n",
+        "// rewards: final value of gate\n",
+        "rewards\n",
+        "\t// [] s=0 & (c=N) & (u=M) : z/N;\n",
+        "\ts=0 & (c=N) & (u=M) : z/N;\n",
+        "endrewards\n",
+        "\n",
+        "label \"target\" = s=4 & z/N<0.1;\n",
+        "label \"end\" = s=4;\n"
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": 12,
+      "id": "049cb9f5-2e69-4092-982f-be446aee0012",
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "nand_model = stormpy.build_model(nand, stormpy.parse_properties(\"P=? [F \\\"target\\\"]\", nand))"
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": 13,
+      "id": "eb11837e-5c59-42d3-97ed-cedb76eca63c",
+      "metadata": {},
+      "outputs": [
+        {
+          "name": "stdout",
+          "output_type": "stream",
+          "text": [
+            "-------------------------------------------------------------- \n",
+            "Model type: \tDTMC (sparse)\n",
+            "States: \t1728\n",
+            "Transitions: \t2505\n",
+            "Reward Models:  none\n",
+            "State Labels: \t3 labels\n",
+            "   * deadlock -> 0 item(s)\n",
+            "   * init -> 1 item(s)\n",
+            "   * target -> 1 item(s)\n",
+            "Choice Labels: \tnone\n",
+            "-------------------------------------------------------------- \n",
+            "\n"
+          ]
+        }
+      ],
+      "source": [
+        "print(nand_model)"
+      ]
+    }
+  ],
+  "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.4"
+    }
+  },
+  "nbformat": 4,
+  "nbformat_minor": 5
+}

stormvogel/__init__.py

@@ -1 +1,21 @@
 """The stormvogel package"""
+
+
+def is_in_notebook():
+    try:
+        from IPython.core.getipython import get_ipython
+
+        ipython = get_ipython()
+
+        if ipython is None or "IPKernelApp" not in ipython.config:
+            return False
+    except ImportError:
+        return False
+    except AttributeError:
+        return False
+    return True
+
+
+if is_in_notebook():
+    # Import and init magic
+    from stormvogel import magic as magic

stormvogel/magic.py

@@ -0,0 +1,41 @@
+"""Cell magic for writing models directly in notebooks."""
+
+import tempfile
+from warnings import warn
+from IPython.core.magic import register_cell_magic
+from IPython.core.getipython import get_ipython
+import stormpy
+
+
+def parse_program(line, cell, parser_function, name):
+    """Parse a program using stormpy."""
+    store_to_var = True
+    # The line should be one word, which is the variable we write the result into
+    if len(line.split()) != 1:
+        warn(f"Write the program to a variable by doing %%{name} <variable>.")
+        store_to_var = False
+
+    with tempfile.NamedTemporaryFile(delete=False) as temp_file:
+        temp_file.write(cell.encode("utf-8"))
+        prism_filename = temp_file.name
+
+    program = parser_function(prism_filename)
+    if store_to_var:
+        ipython = get_ipython()
+        if ipython is not None:
+            ipython.user_ns[line] = program
+        else:
+            raise RuntimeError("IPython not available, but variable provided")
+    return program
+
+
+@register_cell_magic
+def prism(line, cell):
+    """Prism cell magic."""
+    return parse_program(line, cell, stormpy.parse_prism_program, "prism")
+
+
+@register_cell_magic
+def jani(line, cell):
+    """JANI cell magic."""
+    return parse_program(line, cell, stormpy.parse_jani_model, "jani")