From 327d826246884d6ce1a90e36a21c302b206c1f08 Mon Sep 17 00:00:00 2001 From: YouGuessedMyName Date: Sat, 12 Oct 2024 17:10:02 +0200 Subject: [PATCH 1/4] Try to fix the displayed notebooks --- docs/getting_started/die.ipynb | 686 +-------------- docs/getting_started/mdp.ipynb | 789 +----------------- docs/getting_started/model.html | 321 ------- .../naive_value_iteration.ipynb | 673 +-------------- docs/getting_started/study.ipynb | 730 +--------------- stormvogel/communication_server.py | 6 +- stormvogel/show.py | 5 +- 7 files changed, 52 insertions(+), 3158 deletions(-) delete mode 100644 docs/getting_started/model.html diff --git a/docs/getting_started/die.ipynb b/docs/getting_started/die.ipynb index 803f02f..e015427 100644 --- a/docs/getting_started/die.ipynb +++ b/docs/getting_started/die.ipynb @@ -10,14 +10,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:38.879996Z", - "iopub.status.busy": "2024-10-03T08:06:38.879715Z", - "iopub.status.idle": "2024-10-03T08:06:39.041078Z", - "shell.execute_reply": "2024-10-03T08:06:39.040839Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "import stormvogel.model\n", @@ -38,19 +31,13 @@ "cell_type": "code", "execution_count": 2, "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:39.043046Z", - "iopub.status.busy": "2024-10-03T08:06:39.042920Z", - "iopub.status.idle": "2024-10-03T08:06:49.499984Z", - "shell.execute_reply": "2024-10-03T08:06:49.499719Z" - }, "scrolled": true }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "a21acae949ca4ae79a2b6f77015774cd", + "model_id": "a2e7cb659cc0464e89f06cd5105939df", "version_major": 2, "version_minor": 0 }, @@ -60,646 +47,6 @@ }, "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Stormvogel succesfully started the internal communication server, but could not receive the result of a test request.\n", - "Stormvogel is still usable without this, but you will not be able to save node positions in a layout json file.\n", - "1) Restart the kernel and re-run.\n", - "2) Is the port 127.0.0.1:8889 (from the machine where jupyterlab runs) available?\n", - "If you are working remotely, it might help to forward this port. For example: 'ssh -N -L 8889:127.0.0.1:8889 YOUR_SSH_CONFIG_NAME'.\n", - "3) You might also want to consider changing stormvogel.communication_server.localhost_address to the IPv6 loopback address if you are using IPv6.\n", - "If you cannot get the server to work, set stormvogel.communication_server.enable_server to false and re-run. This will speed up stormvogel and ignore this message.\n", - "Please contact the stormvogel developpers if you keep running into issues.\n" - ] - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "d84720b130cd44b59fc1ba5d10e5a5ef", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ @@ -713,43 +60,22 @@ " [(1 / 6, dtmc.new_state(f\"rolled{i}\", {\"rolled\": i})) for i in range(1, 7)]\n", ")\n", "dtmc.add_self_loops()\n", - "vis = stormvogel.show.show(dtmc, show_editor=True)" + "vis = stormvogel.show.show(dtmc, show_editor=False)" ] }, { "cell_type": "code", "execution_count": 3, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:49.555785Z", - "iopub.status.busy": "2024-10-03T08:06:49.555709Z", - "iopub.status.idle": "2024-10-03T08:06:49.558214Z", - "shell.execute_reply": "2024-10-03T08:06:49.557529Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "stormpy_dtmc = stormvogel.mapping.stormvogel_to_stormpy(dtmc)" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { "kernelspec": { - "display_name": ".venv", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -763,7 +89,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.11.2" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index 4226b0e..65ac57a 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -3,14 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:06.970273Z", - "iopub.status.busy": "2024-10-03T08:06:06.970007Z", - "iopub.status.idle": "2024-10-03T08:06:07.146648Z", - "shell.execute_reply": "2024-10-03T08:06:07.146366Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "from stormvogel import visualization, mapping, result, show\n", @@ -20,19 +13,12 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.148795Z", - "iopub.status.busy": "2024-10-03T08:06:07.148678Z", - "iopub.status.idle": "2024-10-03T08:06:07.155809Z", - "shell.execute_reply": "2024-10-03T08:06:07.155553Z" - } - }, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -140,14 +126,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.175749Z", - "iopub.status.busy": "2024-10-03T08:06:07.175618Z", - "iopub.status.idle": "2024-10-03T08:06:07.197932Z", - "shell.execute_reply": "2024-10-03T08:06:07.197677Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "leader_model = stormpy.build_model(leader)\n", @@ -157,14 +136,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.199303Z", - "iopub.status.busy": "2024-10-03T08:06:07.199218Z", - "iopub.status.idle": "2024-10-03T08:06:07.201195Z", - "shell.execute_reply": "2024-10-03T08:06:07.200969Z" - } - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -183,7 +155,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_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" + "['__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" ] } ], @@ -196,14 +168,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.202515Z", - "iopub.status.busy": "2024-10-03T08:06:07.202434Z", - "iopub.status.idle": "2024-10-03T08:06:07.204130Z", - "shell.execute_reply": "2024-10-03T08:06:07.203913Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "prop = stormpy.parse_properties(\"Rmax=? [F \\\"elected\\\"]\", leader)" @@ -212,14 +177,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.205373Z", - "iopub.status.busy": "2024-10-03T08:06:07.205295Z", - "iopub.status.idle": "2024-10-03T08:06:07.207394Z", - "shell.execute_reply": "2024-10-03T08:06:07.206992Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "stormpy_result = stormpy.model_checking(leader_model, prop[0], extract_scheduler=True)" @@ -228,14 +186,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.209102Z", - "iopub.status.busy": "2024-10-03T08:06:07.209008Z", - "iopub.status.idle": "2024-10-03T08:06:07.210629Z", - "shell.execute_reply": "2024-10-03T08:06:07.210414Z" - } - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -252,14 +203,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.211896Z", - "iopub.status.busy": "2024-10-03T08:06:07.211827Z", - "iopub.status.idle": "2024-10-03T08:06:07.213567Z", - "shell.execute_reply": "2024-10-03T08:06:07.213359Z" - } - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -271,9 +215,9 @@ "Transitions: \t56\n", "Reward Models: rounds\n", "State Labels: \t3 labels\n", - " * deadlock -> 3 item(s)\n", - " * init -> 1 item(s)\n", " * elected -> 0 item(s)\n", + " * init -> 1 item(s)\n", + " * deadlock -> 3 item(s)\n", "Choice Labels: \tnone\n", "-------------------------------------------------------------- \n", "\n" @@ -289,14 +233,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.214711Z", - "iopub.status.busy": "2024-10-03T08:06:07.214640Z", - "iopub.status.idle": "2024-10-03T08:06:07.217135Z", - "shell.execute_reply": "2024-10-03T08:06:07.216935Z" - } - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -319,12 +256,6 @@ "cell_type": "code", "execution_count": 10, "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.218326Z", - "iopub.status.busy": "2024-10-03T08:06:07.218240Z", - "iopub.status.idle": "2024-10-03T08:06:07.248079Z", - "shell.execute_reply": "2024-10-03T08:06:07.247857Z" - }, "scrolled": true }, "outputs": [], @@ -336,21 +267,15 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 12, "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:07.249361Z", - "iopub.status.busy": "2024-10-03T08:06:07.249290Z", - "iopub.status.idle": "2024-10-03T08:06:17.727976Z", - "shell.execute_reply": "2024-10-03T08:06:17.727757Z" - }, "scrolled": true }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "c0b3c1743c254b3f9d48881364162eb1", + "model_id": "45d1afe8037e4b20a2e9262bbd0d96e2", "version_major": 2, "version_minor": 0 }, @@ -360,665 +285,18 @@ }, "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Stormvogel succesfully started the internal communication server, but could not receive the result of a test request.\n", - "Stormvogel is still usable without this, but you will not be able to save node positions in a layout json file.\n", - "1) Restart the kernel and re-run.\n", - "2) Is the port 127.0.0.1:8890 (from the machine where jupyterlab runs) available?\n", - "If you are working remotely, it might help to forward this port. For example: 'ssh -N -L 8890:127.0.0.1:8890 YOUR_SSH_CONFIG_NAME'.\n", - "3) You might also want to consider changing stormvogel.communication_server.localhost_address to the IPv6 loopback address if you are using IPv6.\n", - "If you cannot get the server to work, set stormvogel.communication_server.enable_server to false and re-run. This will speed up stormvogel and ignore this message.\n", - "Please contact the stormvogel developpers if you keep running into issues.\n" - ] - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "0336e81cfb924361964758e7ef1cdf17", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ "import stormvogel.layout\n", "\n", - "vis1 = show.show(stormvogel_model, stormvogel_result, layout=stormvogel.layout.EXPLORE())" + "vis1 = show.show(stormvogel_model, stormvogel_result, layout=stormvogel.layout.EXPLORE(), show_editor=False)" ] }, { "cell_type": "code", - "execution_count": 12, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:17.788203Z", - "iopub.status.busy": "2024-10-03T08:06:17.788115Z", - "iopub.status.idle": "2024-10-03T08:06:17.795418Z", - "shell.execute_reply": "2024-10-03T08:06:17.795171Z" - } - }, + "execution_count": 13, + "metadata": {}, "outputs": [], "source": [ "induced_dtmc = stormvogel_result.generate_induced_dtmc()" @@ -1026,20 +304,13 @@ }, { "cell_type": "code", - "execution_count": 13, - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:17.799929Z", - "iopub.status.busy": "2024-10-03T08:06:17.799836Z", - "iopub.status.idle": "2024-10-03T08:06:17.891128Z", - "shell.execute_reply": "2024-10-03T08:06:17.890794Z" - } - }, + "execution_count": 14, + "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "98d8e4ca088c420e80dc87f1f3160c66", + "model_id": "e86249dcc79c4a08924a27214a8c7fab", "version_major": 2, "version_minor": 0 }, @@ -1049,24 +320,10 @@ }, "metadata": {}, "output_type": "display_data" - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "e4304ebb65be496ba499cb52f52ff674", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ - "vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE())" + "vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE(), show_editor=False)" ] }, { @@ -1107,7 +364,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.11.2" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/docs/getting_started/model.html b/docs/getting_started/model.html deleted file mode 100644 index ba51cfc..0000000 --- a/docs/getting_started/model.html +++ /dev/null @@ -1,321 +0,0 @@ - - - - - - - - - - - - - - - -
-

-
- - - - - - -
-

-
- - - - - -
- - -
-
- - - - - - - diff --git a/docs/getting_started/naive_value_iteration.ipynb b/docs/getting_started/naive_value_iteration.ipynb index a9c5a42..c6e1a83 100644 --- a/docs/getting_started/naive_value_iteration.ipynb +++ b/docs/getting_started/naive_value_iteration.ipynb @@ -11,21 +11,14 @@ }, { "cell_type": "code", - "execution_count": 119, + "execution_count": 1, "id": "7f3692d1-ad64-449d-809c-01ceb84e6bb4", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:06:58.249219Z", - "iopub.status.busy": "2024-10-03T08:06:58.248759Z", - "iopub.status.idle": "2024-10-03T08:07:08.690293Z", - "shell.execute_reply": "2024-10-03T08:07:08.689920Z" - } - }, + "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "552f68f4f9b24fe0bd2c2c493c314a8a", + "model_id": "192e4f4d760748e0a4edd3dc3702616d", "version_major": 2, "version_minor": 0 }, @@ -35,646 +28,6 @@ }, "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Stormvogel succesfully started the internal communication server, but could not receive the result of a test request.\n", - "Stormvogel is still usable without this, but you will not be able to save node positions in a layout json file.\n", - "1) Restart the kernel and re-run.\n", - "2) Is the port 127.0.0.1:8889 (from the machine where jupyterlab runs) available?\n", - "If you are working remotely, it might help to forward this port. For example: 'ssh -N -L 8889:127.0.0.1:8889 YOUR_SSH_CONFIG_NAME'.\n", - "3) You might also want to consider changing stormvogel.communication_server.localhost_address to the IPv6 loopback address if you are using IPv6.\n", - "If you cannot get the server to work, set stormvogel.communication_server.enable_server to false and re-run. This will speed up stormvogel and ignore this message.\n", - "Please contact the stormvogel developpers if you keep running into issues.\n" - ] - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "e8dbbb357f754f9986e1beec03e884a0", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ @@ -717,14 +70,7 @@ "cell_type": "code", "execution_count": 2, "id": "8807425f-1d69-4522-9077-b902c90bd0b2", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:08.701868Z", - "iopub.status.busy": "2024-10-03T08:07:08.701716Z", - "iopub.status.idle": "2024-10-03T08:07:08.706787Z", - "shell.execute_reply": "2024-10-03T08:07:08.706363Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "def naive_value_iteration(model, steps, starting_state):\n", @@ -764,14 +110,7 @@ "cell_type": "code", "execution_count": 3, "id": "86b53e1d-2cdb-423e-8dcf-3dacd9e8eb75", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:08.710808Z", - "iopub.status.busy": "2024-10-03T08:07:08.710149Z", - "iopub.status.idle": "2024-10-03T08:07:09.052392Z", - "shell.execute_reply": "2024-10-03T08:07:09.052173Z" - } - }, + "metadata": {}, "outputs": [ { "data": { @@ -841,7 +180,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.11.2" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/docs/getting_started/study.ipynb b/docs/getting_started/study.ipynb index c375946..db48f12 100644 --- a/docs/getting_started/study.ipynb +++ b/docs/getting_started/study.ipynb @@ -12,14 +12,7 @@ "cell_type": "code", "execution_count": 1, "id": "e924f3a4", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.154145Z", - "iopub.status.busy": "2024-10-03T08:07:41.154023Z", - "iopub.status.idle": "2024-10-03T08:07:41.316839Z", - "shell.execute_reply": "2024-10-03T08:07:41.316610Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "import stormvogel.model\n", @@ -40,14 +33,7 @@ "cell_type": "code", "execution_count": 2, "id": "1f2120a8", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.319496Z", - "iopub.status.busy": "2024-10-03T08:07:41.319384Z", - "iopub.status.idle": "2024-10-03T08:07:41.321658Z", - "shell.execute_reply": "2024-10-03T08:07:41.321305Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "mdp = stormvogel.model.new_mdp(\"Monty Hall\")\n", @@ -67,14 +53,7 @@ "cell_type": "code", "execution_count": 3, "id": "1143b6c0", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.323834Z", - "iopub.status.busy": "2024-10-03T08:07:41.323286Z", - "iopub.status.idle": "2024-10-03T08:07:41.326106Z", - "shell.execute_reply": "2024-10-03T08:07:41.325809Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "init.set_transitions([\n", @@ -95,14 +74,7 @@ "cell_type": "code", "execution_count": 4, "id": "64bfb789", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.327849Z", - "iopub.status.busy": "2024-10-03T08:07:41.327632Z", - "iopub.status.idle": "2024-10-03T08:07:41.330009Z", - "shell.execute_reply": "2024-10-03T08:07:41.329727Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "studied.set_transitions([\n", @@ -123,14 +95,7 @@ "cell_type": "code", "execution_count": 5, "id": "89d1d749", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.331655Z", - "iopub.status.busy": "2024-10-03T08:07:41.331348Z", - "iopub.status.idle": "2024-10-03T08:07:41.333216Z", - "shell.execute_reply": "2024-10-03T08:07:41.332980Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "not_studied.set_transitions([\n", @@ -151,14 +116,7 @@ "cell_type": "code", "execution_count": 6, "id": "2f8fb42e", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.334556Z", - "iopub.status.busy": "2024-10-03T08:07:41.334455Z", - "iopub.status.idle": "2024-10-03T08:07:41.335992Z", - "shell.execute_reply": "2024-10-03T08:07:41.335683Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "pass_test.set_transitions([(1, end)])\n", @@ -177,14 +135,7 @@ "cell_type": "code", "execution_count": 7, "id": "bfcbb7fa", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.337269Z", - "iopub.status.busy": "2024-10-03T08:07:41.337188Z", - "iopub.status.idle": "2024-10-03T08:07:41.339069Z", - "shell.execute_reply": "2024-10-03T08:07:41.338833Z" - } - }, + "metadata": {}, "outputs": [], "source": [ "reward_model = mdp.add_rewards(\"R\")\n", @@ -198,26 +149,19 @@ "id": "797e09bb", "metadata": {}, "source": [ - "We'll decorate our model with a nice layout." + "We'll decorate our model with a nice layout. Set show_editor to True to change how the model looks." ] }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 10, "id": "0df1511e-565d-45d0-93a8-adafbfaaaefa", - "metadata": { - "execution": { - "iopub.execute_input": "2024-10-03T08:07:41.341145Z", - "iopub.status.busy": "2024-10-03T08:07:41.341004Z", - "iopub.status.idle": "2024-10-03T08:07:51.792645Z", - "shell.execute_reply": "2024-10-03T08:07:51.792414Z" - } - }, + "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "7bec2df0deeb4659a28b9d1172e4c716", + "model_id": "842f7d395ae045efa313f91bda29eef0", "version_major": 2, "version_minor": 0 }, @@ -227,659 +171,11 @@ }, "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "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": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "Stormvogel succesfully started the internal communication server, but could not receive the result of a test request.\n", - "Stormvogel is still usable without this, but you will not be able to save node positions in a layout json file.\n", - "1) Restart the kernel and re-run.\n", - "2) Is the port 127.0.0.1:8889 (from the machine where jupyterlab runs) available?\n", - "If you are working remotely, it might help to forward this port. For example: 'ssh -N -L 8889:127.0.0.1:8889 YOUR_SSH_CONFIG_NAME'.\n", - "3) You might also want to consider changing stormvogel.communication_server.localhost_address to the IPv6 loopback address if you are using IPv6.\n", - "If you cannot get the server to work, set stormvogel.communication_server.enable_server to false and re-run. This will speed up stormvogel and ignore this message.\n", - "Please contact the stormvogel developpers if you keep running into issues.\n" - ] - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "6d4e09cbf30e485cb5002248de3db411", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ - "vis = show(mdp, show_editor=True, layout=Layout(\"layouts/pinkgreen.json\"))" + "vis = show(mdp, show_editor=False, layout=Layout(\"layouts/pinkgreen.json\"))" ] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "d4fd0009-1632-4318-b4f4-2cc764666295", - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -898,7 +194,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.11.2" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/stormvogel/communication_server.py b/stormvogel/communication_server.py index 69185b7..5a1f030 100644 --- a/stormvogel/communication_server.py +++ b/stormvogel/communication_server.py @@ -120,10 +120,10 @@ def request(self, js: str): awaiting[identifier] = AWAITING logging.info(f"Request sent for: {identifier}") # Wait until result is received. - max_tries = 50 - while max_tries > 0 and awaiting[identifier] == AWAITING: + MAX_TRIES = 10 + while MAX_TRIES > 0 and awaiting[identifier] == AWAITING: sleep(0.2) - max_tries -= 1 + MAX_TRIES -= 1 logging.debug(f"Waiting for request result: {identifier}") logging.debug(f"Current awaiting[identifier]: {awaiting[identifier]}") ipd.display(ipd.HTML(html)) diff --git a/stormvogel/show.py b/stormvogel/show.py index 5a7d0a1..e6d657c 100644 --- a/stormvogel/show.py +++ b/stormvogel/show.py @@ -34,10 +34,7 @@ def show( """ if layout is None: layout = stormvogel.layout.DEFAULT() - do_init_server = False - if show_editor or stormvogel.communication_server.enable_server: - do_init_server = True - + do_init_server = show_editor and stormvogel.communication_server.enable_server do_display = not show_editor vis = stormvogel.visualization.Visualization( model=model, From d2b6de8014baa4d56ee4a1d6a6a0354cb2f9969a Mon Sep 17 00:00:00 2001 From: YouGuessedMyName Date: Sat, 12 Oct 2024 17:27:14 +0200 Subject: [PATCH 2/4] Test --- docs/getting_started/lol.html | 1 + docs/getting_started/study.ipynb | 12 ++++++++++-- stormvogel/visjs.py | 32 ++++++++++++++++++-------------- 3 files changed, 29 insertions(+), 16 deletions(-) create mode 100644 docs/getting_started/lol.html diff --git a/docs/getting_started/lol.html b/docs/getting_started/lol.html new file mode 100644 index 0000000..8fe9ede --- /dev/null +++ b/docs/getting_started/lol.html @@ -0,0 +1 @@ +HELLO HTML diff --git a/docs/getting_started/study.ipynb b/docs/getting_started/study.ipynb index db48f12..af7ca02 100644 --- a/docs/getting_started/study.ipynb +++ b/docs/getting_started/study.ipynb @@ -154,14 +154,14 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 8, "id": "0df1511e-565d-45d0-93a8-adafbfaaaefa", "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "842f7d395ae045efa313f91bda29eef0", + "model_id": "bc6d176108fb414bad62d341a984d211", "version_major": 2, "version_minor": 0 }, @@ -176,6 +176,14 @@ "source": [ "vis = show(mdp, show_editor=False, layout=Layout(\"layouts/pinkgreen.json\"))" ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "caa359bf-4263-41f7-9222-f28d8325d218", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/stormvogel/visjs.py b/stormvogel/visjs.py index e71d56e..9bb794b 100644 --- a/stormvogel/visjs.py +++ b/stormvogel/visjs.py @@ -2,7 +2,6 @@ import IPython.display as ipd import ipywidgets as widgets -import html import stormvogel.displayable import stormvogel.html_templates import stormvogel.communication_server @@ -155,25 +154,30 @@ def generate_html(self) -> str: ).replace("__SIZES__", sizes) return html - def generate_iframe(self) -> str: + def generate_iframe(self) -> ipd.IFrame: """Generate an iframe for the network, using the html.""" - return f""" - """ + return ipd.IFrame( + src="lol.html", + width=self.width + self.EXTRA_PIXELS, + height=self.height + self.EXTRA_PIXELS, + ) + # return f""" + # """ def show(self) -> None: """Display the network on the output that was specified at initialization, otherwise simply display it.""" iframe = self.generate_iframe() with self.output: # Display the iframe within the Output. ipd.clear_output() - ipd.display(ipd.HTML(iframe)) + ipd.display(iframe) self.maybe_display_output() with self.debug_output: logging.info("Called Network.show") @@ -183,7 +187,7 @@ def reload(self) -> None: iframe = self.generate_iframe() with self.output: ipd.clear_output() - ipd.display(ipd.HTML(iframe)) + ipd.display(iframe) with self.debug_output: logging.info("Called Network.reload") From a2c750da151583979aba8f1f25994fee4c8b476b Mon Sep 17 00:00:00 2001 From: YouGuessedMyName Date: Sat, 12 Oct 2024 17:30:36 +0200 Subject: [PATCH 3/4] Revert "Test" This reverts commit d2b6de8014baa4d56ee4a1d6a6a0354cb2f9969a. --- docs/getting_started/lol.html | 1 - docs/getting_started/study.ipynb | 12 ++---------- stormvogel/visjs.py | 32 ++++++++++++++------------------ 3 files changed, 16 insertions(+), 29 deletions(-) delete mode 100644 docs/getting_started/lol.html diff --git a/docs/getting_started/lol.html b/docs/getting_started/lol.html deleted file mode 100644 index 8fe9ede..0000000 --- a/docs/getting_started/lol.html +++ /dev/null @@ -1 +0,0 @@ -HELLO HTML diff --git a/docs/getting_started/study.ipynb b/docs/getting_started/study.ipynb index af7ca02..db48f12 100644 --- a/docs/getting_started/study.ipynb +++ b/docs/getting_started/study.ipynb @@ -154,14 +154,14 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 10, "id": "0df1511e-565d-45d0-93a8-adafbfaaaefa", "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "bc6d176108fb414bad62d341a984d211", + "model_id": "842f7d395ae045efa313f91bda29eef0", "version_major": 2, "version_minor": 0 }, @@ -176,14 +176,6 @@ "source": [ "vis = show(mdp, show_editor=False, layout=Layout(\"layouts/pinkgreen.json\"))" ] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "caa359bf-4263-41f7-9222-f28d8325d218", - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { diff --git a/stormvogel/visjs.py b/stormvogel/visjs.py index 9bb794b..e71d56e 100644 --- a/stormvogel/visjs.py +++ b/stormvogel/visjs.py @@ -2,6 +2,7 @@ import IPython.display as ipd import ipywidgets as widgets +import html import stormvogel.displayable import stormvogel.html_templates import stormvogel.communication_server @@ -154,30 +155,25 @@ def generate_html(self) -> str: ).replace("__SIZES__", sizes) return html - def generate_iframe(self) -> ipd.IFrame: + def generate_iframe(self) -> str: """Generate an iframe for the network, using the html.""" - return ipd.IFrame( - src="lol.html", - width=self.width + self.EXTRA_PIXELS, - height=self.height + self.EXTRA_PIXELS, - ) - # return f""" - # """ + return f""" + """ def show(self) -> None: """Display the network on the output that was specified at initialization, otherwise simply display it.""" iframe = self.generate_iframe() with self.output: # Display the iframe within the Output. ipd.clear_output() - ipd.display(iframe) + ipd.display(ipd.HTML(iframe)) self.maybe_display_output() with self.debug_output: logging.info("Called Network.show") @@ -187,7 +183,7 @@ def reload(self) -> None: iframe = self.generate_iframe() with self.output: ipd.clear_output() - ipd.display(iframe) + ipd.display(ipd.HTML(iframe)) with self.debug_output: logging.info("Called Network.reload") From 42e6a05471e904f6b517df00786e25c5ab36f192 Mon Sep 17 00:00:00 2001 From: YouGuessedMyName Date: Sun, 13 Oct 2024 11:15:35 +0200 Subject: [PATCH 4/4] Hopefully fix docs --- docs/getting_started/naive_value_iteration.ipynb | 10 +++++++++- docs/getting_started/prism.ipynb | 4 ++-- stormvogel/visjs.py | 4 ++-- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/docs/getting_started/naive_value_iteration.ipynb b/docs/getting_started/naive_value_iteration.ipynb index c6e1a83..5e5143e 100644 --- a/docs/getting_started/naive_value_iteration.ipynb +++ b/docs/getting_started/naive_value_iteration.ipynb @@ -18,7 +18,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "192e4f4d760748e0a4edd3dc3702616d", + "model_id": "3f6d01aafc5e4afea55975ebcf61050d", "version_major": 2, "version_minor": 0 }, @@ -162,6 +162,14 @@ "metadata": {}, "outputs": [], "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "12b57306-780c-4a40-898a-f3a95f7ff9eb", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/docs/getting_started/prism.ipynb b/docs/getting_started/prism.ipynb index 5b16cf5..fdf879a 100644 --- a/docs/getting_started/prism.ipynb +++ b/docs/getting_started/prism.ipynb @@ -293,7 +293,7 @@ "source": [ "stormvogel_model = mapping.stormpy_to_stormvogel(nand_model)\n", "\n", - "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)" + "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result, show_editor=False)" ] }, { @@ -993,7 +993,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.11.2" }, "widgets": { "application/vnd.jupyter.widget-state+json": { diff --git a/stormvogel/visjs.py b/stormvogel/visjs.py index e71d56e..99a5d01 100644 --- a/stormvogel/visjs.py +++ b/stormvogel/visjs.py @@ -173,7 +173,7 @@ def show(self) -> None: iframe = self.generate_iframe() with self.output: # Display the iframe within the Output. ipd.clear_output() - ipd.display(ipd.HTML(iframe)) + ipd.display(widgets.HTML(iframe)) self.maybe_display_output() with self.debug_output: logging.info("Called Network.show") @@ -183,7 +183,7 @@ def reload(self) -> None: iframe = self.generate_iframe() with self.output: ipd.clear_output() - ipd.display(ipd.HTML(iframe)) + ipd.display(widgets.HTML(iframe)) with self.debug_output: logging.info("Called Network.reload")