diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index c7c3ec9..0690df0 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -18,7 +18,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -167,7 +167,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -266,40 +266,64 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 15, "metadata": { "scrolled": true }, "outputs": [ { - "ename": "TypeError", - "evalue": "parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mTypeError\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[10], line 4\u001b[0m\n\u001b[1;32m 1\u001b[0m stormvogel_model \u001b[38;5;241m=\u001b[39m mapping\u001b[38;5;241m.\u001b[39mstormpy_to_stormvogel(leader_model)\n\u001b[1;32m 3\u001b[0m \u001b[38;5;66;03m#a stormvogel result can also be obtained directly:\u001b[39;00m\n\u001b[0;32m----> 4\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m \u001b[43mmodel_checking\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mmodel_checking\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstormvogel_model\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mprop\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m)\u001b[49m\n\u001b[1;32m 6\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m result\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", - "File \u001b[0;32m~/repositories/stormvogel/.venv/lib/python3.12/site-packages/stormvogel/model_checking.py:18\u001b[0m, in \u001b[0;36mmodel_checking\u001b[0;34m(model, prop, scheduler)\u001b[0m\n\u001b[1;32m 9\u001b[0m \u001b[38;5;250m\u001b[39m\u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 10\u001b[0m \u001b[38;5;124;03mFunction to provide a model checking functionality in stormvogel that uses the stormpy model checker behind the scenes.\u001b[39;00m\n\u001b[1;32m 11\u001b[0m \u001b[38;5;124;03mTakes a stormvogel model and a property string as input. Additionally it can be specified wheter the result should contain a scheduler or not.\u001b[39;00m\n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 14\u001b[0m \u001b[38;5;124;03mfollowed by converting the model checker result to a stormvogel result. This function just performs this procedure automatically.\u001b[39;00m\n\u001b[1;32m 15\u001b[0m \u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 17\u001b[0m stormpy_model \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mmapping\u001b[38;5;241m.\u001b[39mstormvogel_to_stormpy(model)\n\u001b[0;32m---> 18\u001b[0m parsed_prop \u001b[38;5;241m=\u001b[39m \u001b[43mstormpy\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mparse_properties_without_context\u001b[49m\u001b[43m(\u001b[49m\u001b[43mprop\u001b[49m\u001b[43m)\u001b[49m \n\u001b[1;32m 19\u001b[0m stormpy_result \u001b[38;5;241m=\u001b[39m stormpy\u001b[38;5;241m.\u001b[39mmodel_checking(stormpy_model, parsed_prop, extract_scheduler\u001b[38;5;241m=\u001b[39mscheduler)\n\u001b[1;32m 20\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mresult\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", - "\u001b[0;31mTypeError\u001b[0m: parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []" - ] + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "423136e0bf054647a4c0a03d7445cfa8", + "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": "443fe89c24aa451bb549ece263673661", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], - "source": [ - "stormvogel_model = mapping.stormpy_to_stormvogel(leader_model)\n", - "\n", - "#a stormvogel result can also be obtained directly:\n", - "#stormvogel_result = model_checking.model_checking(stormvogel_model, prop[0], True)\n", - "\n", - "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "scrolled": true - }, - "outputs": [], "source": [ "import stormvogel.layout\n", "\n", @@ -308,34 +332,22 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 16, "metadata": {}, - "outputs": [ - { - "ename": "NameError", - "evalue": "name 'stormvogel_result' is not defined", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[11], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m induced_dtmc \u001b[38;5;241m=\u001b[39m \u001b[43mstormvogel_result\u001b[49m\u001b[38;5;241m.\u001b[39mgenerate_induced_dtmc()\n", - "\u001b[0;31mNameError\u001b[0m: name 'stormvogel_result' is not defined" - ] - } - ], + "outputs": [], "source": [ "induced_dtmc = stormvogel_result.generate_induced_dtmc()" ] }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "a44b9b958747405b84ab6467441ca86a", + "model_id": "a56ece4593504c95b575e61387666219", "version_major": 2, "version_minor": 0 }, @@ -349,7 +361,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "ec5f0ce2baf24964b07078b37cf7e46f", + "model_id": "0bb6d1006f5c4805906414ae77c05328", "version_major": 2, "version_minor": 0 }, @@ -365,34 +377,6 @@ "vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE())" ] }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, { "cell_type": "code", "execution_count": null, @@ -403,9 +387,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": "Python 3 (ipykernel)", "language": "python", - "name": "stormvogel-env" + "name": "python3" }, "language_info": { "codemirror_mode": { @@ -417,7 +401,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.5" + "version": "3.12.7" } }, "nbformat": 4,