Skip to content

Commit

Permalink
remove unnecessary notebook cell
Browse files Browse the repository at this point in the history
  • Loading branch information
@PimLeerkes
PimLeerkes committed Dec 14, 2024
1 parent 8d0c93d commit 4412aa5
Showing 1 changed file with 61 additions and 77 deletions.
138 changes: 61 additions & 77 deletions docs/getting_started/mdp.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
{
"data": {
"text/plain": [
"<stormpy.storage.storage.PrismProgram at 0x7fae4020e670>"
"<stormpy.storage.storage.PrismProgram at 0x7f131c10ab30>"
]
},
"execution_count": 2,
Expand Down Expand Up @@ -167,7 +167,7 @@
},
{
"cell_type": "code",
"execution_count": 16,
"execution_count": 5,
"metadata": {},
"outputs": [
{
Expand Down Expand Up @@ -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: [<stormpy.core.Property object at 0x7fae397a04f0>]",
"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: [<stormpy.core.Property object at 0x7fae397a04f0>]"
]
"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": [
"<script>fetch('http://127.0.0.1:8889/nfbwTPnqVm/MESSAGE/' + 'test message')</script>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<script>fetch('http://127.0.0.1:8889/nfbwTPnqVm/MESSAGE/' + 'test message')</script>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"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",
Expand All @@ -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
},
Expand All @@ -349,7 +361,7 @@
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "ec5f0ce2baf24964b07078b37cf7e46f",
"model_id": "0bb6d1006f5c4805906414ae77c05328",
"version_major": 2,
"version_minor": 0
},
Expand All @@ -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,
Expand All @@ -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": {
Expand All @@ -417,7 +401,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.5"
"version": "3.12.7"
}
},
"nbformat": 4,
Expand Down

0 comments on commit 4412aa5

Please sign in to comment.