diff --git a/docs/getting_started/prism.ipynb b/docs/getting_started/prism.ipynb new file mode 100644 index 0000000..6294645 --- /dev/null +++ b/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": [ + "" + ] + }, + "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 (s'=1); // do next nand if have not done N yet\n", + "\t[] s=0 & (c=N) & (u (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 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 (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 +} diff --git a/stormvogel/__init__.py b/stormvogel/__init__.py index bcf0d99..4ed1da8 100644 --- a/stormvogel/__init__.py +++ b/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 diff --git a/stormvogel/magic.py b/stormvogel/magic.py new file mode 100644 index 0000000..d42d291 --- /dev/null +++ b/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} .") + 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")