diff --git a/docs/getting_started/00_die.ipynb b/docs/getting_started/00_die.ipynb index 55bf8bf..7c84273 100644 --- a/docs/getting_started/00_die.ipynb +++ b/docs/getting_started/00_die.ipynb @@ -39,7 +39,7 @@ "text/html": [ "\n", " fetch('http://127.0.0.1:8892/ifNagYWiMW/MESSAGE/' + 'test message')" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "text/html": [ - "" + "\n", + " " ], "text/plain": [ "" @@ -210,44 +418,16 @@ }, "metadata": {}, "output_type": "display_data" - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "fdbfe0ff407a4a308031b5e7e783cf40", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "Output()" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "78d798387dbc4a6b8896a4d6125884ee", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ - "vis = show(mdp, layout=Layout(\"layouts/pinkgreen.json\"), name=\"study\", save_and_embed=True)" + "vis = show(mdp, layout=Layout(\"layouts/pinkgreen.json\"), name=\"study\", show_editor=False)" ] }, { "cell_type": "code", "execution_count": null, - "id": "260bfa16-9971-4ee9-9744-0478ee31dbe4", + "id": "a9e68b97-49d8-47dc-8ba1-5d179bcecc52", "metadata": {}, "outputs": [], "source": [] @@ -269,7 +449,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.12.3" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/docs/getting_started/02_naive_value_iteration.ipynb b/docs/getting_started/02_naive_value_iteration.ipynb index 316705a..365d36b 100644 --- a/docs/getting_started/02_naive_value_iteration.ipynb +++ b/docs/getting_started/02_naive_value_iteration.ipynb @@ -11,365 +11,19 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 5, "id": "7f3692d1-ad64-449d-809c-01ceb84e6bb4", "metadata": {}, "outputs": [ { "data": { - "text/html": [ - "\n", - " " - ], + "application/vnd.jupyter.widget-view+json": { + "model_id": "9990ef5a93aa41729419d45003428d66", + "version_major": 2, + "version_minor": 0 + }, "text/plain": [ - "" + "Output()" ] }, "metadata": {}, @@ -444,7 +98,7 @@ "\n", "from stormvogel.show import show\n", "from stormvogel.layout import Layout\n", - "vis = show(lion, layout=Layout(\"layouts/lion.json\"), name=\"lion\", save_and_embed=True)" + "vis = show(lion, layout=Layout(\"layouts/lion.json\"), name=\"lion\", show_editor=False)" ] }, { @@ -457,7 +111,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 6, "id": "8807425f-1d69-4522-9077-b902c90bd0b2", "metadata": {}, "outputs": [], @@ -515,7 +169,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 7, "id": "a606dc3e-5d22-45a2-8234-30d3fe8b6bc5", "metadata": {}, "outputs": [ @@ -547,7 +201,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 8, "id": "12b57306-780c-4a40-898a-f3a95f7ff9eb", "metadata": {}, "outputs": [], @@ -574,7 +228,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.12.3" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/docs/getting_started/03_prism.ipynb b/docs/getting_started/03_prism.ipynb index f61674d..a9dd69c 100644 --- a/docs/getting_started/03_prism.ipynb +++ b/docs/getting_started/03_prism.ipynb @@ -36,7 +36,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -174,12 +174,12 @@ "Transitions: \t243\n", "Reward Models: (default)\n", "State Labels: \t8 labels\n", - " * deadlock -> 0 item(s)\n", " * init -> 1 item(s)\n", " * whichx -> 42 item(s)\n", - " * target -> 1 item(s)\n", " * selection -> 39 item(s)\n", " * nextnand -> 42 item(s)\n", + " * deadlock -> 0 item(s)\n", + " * target -> 1 item(s)\n", " * gate -> 52 item(s)\n", " * end -> 3 item(s)\n", "Choice Labels: \tnone\n", @@ -251,7 +251,7 @@ "text/html": [ "\n", " " + "" ] }, "execution_count": 2, @@ -162,7 +162,7 @@ "Choice Labels: \tnone\n", "-------------------------------------------------------------- \n", "\n", - "['__class__', '__delattr__', '__dir__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__getstate__', '__gt__', '__hash__', '__init__', '__init_subclass__', '__le__', '__lt__', '__module__', '__ne__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', '_as_sparse_ctmc', '_as_sparse_dtmc', '_as_sparse_exact_dtmc', '_as_sparse_exact_mdp', '_as_sparse_imdp', '_as_sparse_ma', '_as_sparse_mdp', '_as_sparse_pctmc', '_as_sparse_pdtmc', '_as_sparse_pma', '_as_sparse_pmdp', '_as_sparse_pomdp', '_as_sparse_ppomdp', '_as_symbolic_ctmc', '_as_symbolic_dtmc', '_as_symbolic_ma', '_as_symbolic_mdp', '_as_symbolic_pctmc', '_as_symbolic_pdtmc', '_as_symbolic_pma', '_as_symbolic_pmdp', 'add_reward_model', 'apply_scheduler', 'backward_transition_matrix', 'choice_labeling', 'choice_origins', 'get_choice_index', 'get_nr_available_actions', 'get_reward_model', 'has_choice_labeling', 'has_choice_origins', 'has_parameters', 'has_reward_model', 'has_state_valuations', 'initial_states', 'initial_states_as_bitvector', 'is_discrete_time_model', 'is_exact', 'is_nondeterministic_model', 'is_partially_observable', 'is_sink_state', 'is_sparse_model', 'is_symbolic_model', 'labeling', 'labels_state', 'model_type', 'nondeterministic_choice_indices', 'nr_choices', 'nr_states', 'nr_transitions', 'reduce_to_state_based_rewards', 'reward_models', 'set_initial_states', 'state_valuations', 'states', 'supports_parameters', 'supports_uncertainty', 'to_dot', 'transition_matrix']\n" + "['__class__', '__delattr__', '__dir__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__getstate__', '__gt__', '__hash__', '__init__', '__init_subclass__', '__le__', '__lt__', '__module__', '__ne__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', '_as_sparse_ctmc', '_as_sparse_dtmc', '_as_sparse_exact_dtmc', '_as_sparse_exact_mdp', '_as_sparse_imdp', '_as_sparse_ma', '_as_sparse_mdp', '_as_sparse_pctmc', '_as_sparse_pdtmc', '_as_sparse_pma', '_as_sparse_pmdp', '_as_sparse_pomdp', '_as_sparse_ppomdp', '_as_sparse_smg', '_as_symbolic_ctmc', '_as_symbolic_dtmc', '_as_symbolic_ma', '_as_symbolic_mdp', '_as_symbolic_pctmc', '_as_symbolic_pdtmc', '_as_symbolic_pma', '_as_symbolic_pmdp', 'add_reward_model', 'apply_scheduler', 'backward_transition_matrix', 'choice_labeling', 'choice_origins', 'get_choice_index', 'get_nr_available_actions', 'get_reward_model', 'has_choice_labeling', 'has_choice_origins', 'has_parameters', 'has_reward_model', 'has_state_valuations', 'initial_states', 'initial_states_as_bitvector', 'is_discrete_time_model', 'is_exact', 'is_nondeterministic_model', 'is_partially_observable', 'is_sink_state', 'is_sparse_model', 'is_symbolic_model', 'labeling', 'labels_state', 'model_type', 'nondeterministic_choice_indices', 'nr_choices', 'nr_states', 'nr_transitions', 'reduce_to_state_based_rewards', 'reward_models', 'set_initial_states', 'state_valuations', 'states', 'supports_parameters', 'supports_uncertainty', 'to_dot', 'transition_matrix']\n" ] } ], @@ -284,7 +284,7 @@ "text/html": [ "\n", " 5 item(s)\n", - " * (1,2) -> 1 item(s)\n", " * escaped -> 1 item(s)\n", + " * (1,2) -> 1 item(s)\n", + " * \u2193 -> 4 item(s)\n", + " * (3,1) -> 5 item(s)\n", + " * (3,2) -> 5 item(s)\n", + " * (2,1) -> 5 item(s)\n", + " * \u2190 -> 4 item(s)\n", " * (1,1) -> 5 item(s)\n", " * \u2192 -> 4 item(s)\n", " * e -> 1 item(s)\n", " * \u2191 -> 4 item(s)\n", - " * \u2190 -> 4 item(s)\n", " * t -> 4 item(s)\n", - " * (3,2) -> 5 item(s)\n", + "Choice Labels: \t4 labels\n", + " * \u2192 -> 4 item(s)\n", " * \u2193 -> 4 item(s)\n", - " * (2,1) -> 5 item(s)\n", - "Choice Labels: \t0 labels\n", + " * \u2191 -> 4 item(s)\n", + " * \u2190 -> 4 item(s)\n", "-------------------------------------------------------------- \n", "\n" ] + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "e082253a591e4b1aa4a6a1b8dd15b5d7", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "344d0554115e4dc381c93683abac404f", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "5b90190eb6d74a98b10e97be81cb567e", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -772,11 +842,11 @@ "stormpy_model = stormvogel_to_stormpy(pomdp)\n", "print(stormpy_model)\n", "pomdp2 = stormpy_to_stormvogel(stormpy_model)\n", - "#vis2 = show(pomdp2, layout=Layout(\"layouts/grid.json\"), separate_labels=[\"t\", \"e\"], show_editor=True)\n", + "vis2 = show(pomdp2, layout=Layout(\"layouts/grid.json\"), separate_labels=[\"t\", \"e\"], show_editor=True)\n", "\n", "\n", - "# TODO use stormpy to find the best policy/schedule, i.e. escape the maze as quickly as possible.\n", - "# Ask Pim or Linus for help?" + "# TODO use the stormvogel model checking instead!\n", + "# TODO fix the layout once we switch to sets for displaying labels" ] }, { @@ -789,13 +859,21 @@ "name": "stdout", "output_type": "stream", "text": [ - "{'0': Action(name='0', labels=frozenset()), '1': Action(name='1', labels=frozenset()), '2': Action(name='2', labels=frozenset()), '3': Action(name='3', labels=frozenset()), '4': Action(name='4', labels=frozenset()), '5': Action(name='5', labels=frozenset()), '6': Action(name='6', labels=frozenset()), '7': Action(name='7', labels=frozenset()), '8': Action(name='8', labels=frozenset()), '9': Action(name='9', labels=frozenset()), '10': Action(name='10', labels=frozenset()), '11': Action(name='11', labels=frozenset()), '12': Action(name='12', labels=frozenset()), '13': Action(name='13', labels=frozenset()), '14': Action(name='14', labels=frozenset()), '15': Action(name='15', labels=frozenset()), '16': Action(name='16', labels=frozenset()), '17': Action(name='17', labels=frozenset()), '18': Action(name='18', labels=frozenset()), '19': Action(name='19', labels=frozenset()), '20': Action(name='20', labels=frozenset()), '21': Action(name='21', labels=frozenset()), '22': Action(name='22', labels=frozenset()), '23': Action(name='23', labels=frozenset()), '24': Action(name='24', labels=frozenset()), '25': Action(name='25', labels=frozenset()), '26': Action(name='26', labels=frozenset()), '27': Action(name='27', labels=frozenset()), '28': Action(name='28', labels=frozenset()), '29': Action(name='29', labels=frozenset()), '30': Action(name='30', labels=frozenset()), '31': Action(name='31', labels=frozenset()), '32': Action(name='32', labels=frozenset()), '33': Action(name='33', labels=frozenset())}\n" + "{Action(labels=frozenset()), Action(labels=frozenset({'\u2193'})), Action(labels=frozenset({'\u2192'})), Action(labels=frozenset({'\u2191'})), Action(labels=frozenset({'\u2190'}))}\n" ] } ], "source": [ "print(pomdp2.actions)\n" ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "ea8bceb9-a0c5-49ee-9fb3-b03b0389fb9f", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -814,7 +892,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.12.3" } }, "nbformat": 4, diff --git a/docs/getting_started/die.html b/docs/getting_started/die.html index 43d594b..7cc9d70 100644 --- a/docs/getting_started/die.html +++ b/docs/getting_started/die.html @@ -1,6 +1,6 @@