Skip to content

Commit

Permalink
move some code in layout_editor.py around
Browse files Browse the repository at this point in the history
  • Loading branch information
@YouGuessedMyName
YouGuessedMyName committed Feb 22, 2025
1 parent 4e2aa63 commit 300ff31
Show file tree
Hide file tree
Showing 7 changed files with 316 additions and 159 deletions.
12 changes: 6 additions & 6 deletions docs/introduction/1-Introduction.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 1,
"id": "df22ee92-d159-46de-913b-bf22e1022386",
"metadata": {},
"outputs": [
Expand All @@ -27,7 +27,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modeluyiYtdQVSk\"\n",
" id=\"modelstLyyXzOUw\"\n",
" width=\"675\"\n",
" height=\"395\"\n",
" frameborder=\"0\"\n",
Expand Down Expand Up @@ -378,15 +378,15 @@
],
"source": [
"import stormvogel.show, stormvogel.examples.car, stormvogel.show\n",
"vis = stormvogel.show.show(stormvogel.examples.car.car, layout=stormvogel.layout.CAR(), show_editor=False)"
"vis = stormvogel.show.show(stormvogel.examples.car.car, layout=stormvogel.layout.CAR())"
]
},
{
"cell_type": "markdown",
"id": "97ee7880-9bf6-4f6b-add6-fd1db5db8c34",
"metadata": {},
"source": [
"Over the last decades, many tools to automate model checking have been developed at various institutions.\n",
"Over the last decades, many tools to automate model checking have been developed at various institutions, but the most succesful ones are PRISM and Storm.\n",
"\n",
"### What is Storm, Stormpy and Stormvogel?\n",
"* [Storm](https://www.stormchecker.org/) is a model checker developed at RWTH Aachen University using C/C++. It is currently considered one of the best model checking tools. It is designed in a low-level way that allows users a great level of control over the internal representation of the models. This meams that Storm is very efficient, but also difficult to use.\n",
Expand Down Expand Up @@ -414,7 +414,7 @@
},
{
"cell_type": "code",
"execution_count": 4,
"execution_count": 2,
"id": "9c7665b1-0d99-49e8-bd28-a9742bfb36cc",
"metadata": {},
"outputs": [
Expand All @@ -423,7 +423,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modelPFsJIpbyZc\"\n",
" id=\"modelZaPjlZjtxa\"\n",
" width=\"223\"\n",
" height=\"233\"\n",
" frameborder=\"0\"\n",
Expand Down
148 changes: 78 additions & 70 deletions docs/introduction/2-1-Building-dtmcs.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 6,
"id": "c6542cf2-8445-429c-bdf8-531d36868d94",
"metadata": {},
"outputs": [
Expand All @@ -25,7 +25,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modelnrTNrtiHLH\"\n",
" id=\"modeluYiTYLNqGb\"\n",
" width=\"401\"\n",
" height=\"394\"\n",
" frameborder=\"0\"\n",
Expand All @@ -52,13 +52,13 @@
" &lt;div id=&quot;mynetwork&quot;&gt;&lt;/div&gt;\n",
" &lt;script type=&quot;text/javascript&quot;&gt;\n",
" \n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: 0 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 114, y: 78 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 7, y: -140 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 127, y: -64 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -112, y: -82 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -14, y: 141 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -130, y: 56 },\n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: -3 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 3, y: -146 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 128, y: -67 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 120, y: 77 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -6, y: 135 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -124, y: 70 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -124, y: -73 },\n",
"]);\n",
" var edges = new vis.DataSet([{ from: 0, to: 1, label: &quot;1/6&quot; },\n",
"{ from: 0, to: 2, label: &quot;1/6&quot; },\n",
Expand Down Expand Up @@ -189,31 +189,31 @@
" &quot;positions&quot;: {\n",
" &quot;0&quot;: {\n",
" &quot;x&quot;: 0,\n",
" &quot;y&quot;: 0\n",
" &quot;y&quot;: -3\n",
" },\n",
" &quot;1&quot;: {\n",
" &quot;x&quot;: 114,\n",
" &quot;y&quot;: 78\n",
" &quot;x&quot;: 3,\n",
" &quot;y&quot;: -146\n",
" },\n",
" &quot;2&quot;: {\n",
" &quot;x&quot;: 7,\n",
" &quot;y&quot;: -140\n",
" &quot;x&quot;: 128,\n",
" &quot;y&quot;: -67\n",
" },\n",
" &quot;3&quot;: {\n",
" &quot;x&quot;: 127,\n",
" &quot;y&quot;: -64\n",
" &quot;x&quot;: 120,\n",
" &quot;y&quot;: 77\n",
" },\n",
" &quot;4&quot;: {\n",
" &quot;x&quot;: -112,\n",
" &quot;y&quot;: -82\n",
" &quot;x&quot;: -6,\n",
" &quot;y&quot;: 135\n",
" },\n",
" &quot;5&quot;: {\n",
" &quot;x&quot;: -14,\n",
" &quot;y&quot;: 141\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: 70\n",
" },\n",
" &quot;6&quot;: {\n",
" &quot;x&quot;: -130,\n",
" &quot;y&quot;: 56\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: -73\n",
" }\n",
" },\n",
" &quot;width&quot;: 381,\n",
Expand Down Expand Up @@ -320,7 +320,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 7,
"id": "abed08f9-9381-4cf1-97b6-582f8a7a7cfb",
"metadata": {},
"outputs": [
Expand All @@ -329,7 +329,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modelvZYhojjYnr\"\n",
" id=\"modelWcaxddDIXx\"\n",
" width=\"401\"\n",
" height=\"394\"\n",
" frameborder=\"0\"\n",
Expand All @@ -356,13 +356,13 @@
" &lt;div id=&quot;mynetwork&quot;&gt;&lt;/div&gt;\n",
" &lt;script type=&quot;text/javascript&quot;&gt;\n",
" \n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: 0 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 114, y: 78 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 7, y: -140 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 127, y: -64 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -112, y: -82 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -14, y: 141 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -130, y: 56 },\n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: -3 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 3, y: -146 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 128, y: -67 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 120, y: 77 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -6, y: 135 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -124, y: 70 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -124, y: -73 },\n",
"]);\n",
" var edges = new vis.DataSet([{ from: 0, to: 1, label: &quot;1/6&quot; },\n",
"{ from: 0, to: 2, label: &quot;1/6&quot; },\n",
Expand Down Expand Up @@ -493,31 +493,31 @@
" &quot;positions&quot;: {\n",
" &quot;0&quot;: {\n",
" &quot;x&quot;: 0,\n",
" &quot;y&quot;: 0\n",
" &quot;y&quot;: -3\n",
" },\n",
" &quot;1&quot;: {\n",
" &quot;x&quot;: 114,\n",
" &quot;y&quot;: 78\n",
" &quot;x&quot;: 3,\n",
" &quot;y&quot;: -146\n",
" },\n",
" &quot;2&quot;: {\n",
" &quot;x&quot;: 7,\n",
" &quot;y&quot;: -140\n",
" &quot;x&quot;: 128,\n",
" &quot;y&quot;: -67\n",
" },\n",
" &quot;3&quot;: {\n",
" &quot;x&quot;: 127,\n",
" &quot;y&quot;: -64\n",
" &quot;x&quot;: 120,\n",
" &quot;y&quot;: 77\n",
" },\n",
" &quot;4&quot;: {\n",
" &quot;x&quot;: -112,\n",
" &quot;y&quot;: -82\n",
" &quot;x&quot;: -6,\n",
" &quot;y&quot;: 135\n",
" },\n",
" &quot;5&quot;: {\n",
" &quot;x&quot;: -14,\n",
" &quot;y&quot;: 141\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: 70\n",
" },\n",
" &quot;6&quot;: {\n",
" &quot;x&quot;: -130,\n",
" &quot;y&quot;: 56\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: -73\n",
" }\n",
" },\n",
" &quot;width&quot;: 381,\n",
Expand Down Expand Up @@ -632,22 +632,22 @@
"id": "c87b4b02-ef13-459a-9a99-bcdd1c6d18a7",
"metadata": {},
"source": [
"Finally, we can also construct our die model in PRISM. The concepts here are similar to the pgc API."
"Finally, we can also construct our die model in PRISM. The concepts here are similar to the pgc API. **This requires stormpy**."
]
},
{
"cell_type": "code",
"execution_count": 3,
"execution_count": 10,
"id": "bf89ca26-43a6-4929-9da4-b17f7771289a",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"<stormpy.storage.storage.PrismProgram at 0x762ab27fb070>"
"<stormpy.storage.storage.PrismProgram at 0x72cd50122ff0>"
]
},
"execution_count": 3,
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
Expand Down Expand Up @@ -681,9 +681,17 @@
"label \"rolled6\" = s=6;"
]
},
{
"cell_type": "markdown",
"id": "e161373f-5334-4a89-bfb7-adf65ac4aa25",
"metadata": {},
"source": [
"Under the hood, stormpy parses the prism model which is then converted to a stormpy model and a stormvogel model."
]
},
{
"cell_type": "code",
"execution_count": 4,
"execution_count": 11,
"id": "cca0c59b-ec0b-4a3b-92a4-5a4c793512e5",
"metadata": {},
"outputs": [
Expand All @@ -692,7 +700,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modeljHoEWwdnCC\"\n",
" id=\"modelkVckhoosKI\"\n",
" width=\"401\"\n",
" height=\"394\"\n",
" frameborder=\"0\"\n",
Expand All @@ -719,13 +727,13 @@
" &lt;div id=&quot;mynetwork&quot;&gt;&lt;/div&gt;\n",
" &lt;script type=&quot;text/javascript&quot;&gt;\n",
" \n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: 0 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 114, y: 78 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 7, y: -140 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 127, y: -64 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -112, y: -82 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -14, y: 141 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -130, y: 56 },\n",
" var nodes = new vis.DataSet([{ id: 0, label: `init`, group: &quot;states&quot;, x: 0, y: -3 },\n",
"{ id: 1, label: `rolled1`, group: &quot;states&quot;, x: 3, y: -146 },\n",
"{ id: 2, label: `rolled2`, group: &quot;states&quot;, x: 128, y: -67 },\n",
"{ id: 3, label: `rolled3`, group: &quot;states&quot;, x: 120, y: 77 },\n",
"{ id: 4, label: `rolled4`, group: &quot;states&quot;, x: -6, y: 135 },\n",
"{ id: 5, label: `rolled5`, group: &quot;states&quot;, x: -124, y: 70 },\n",
"{ id: 6, label: `rolled6`, group: &quot;states&quot;, x: -124, y: -73 },\n",
"]);\n",
" var edges = new vis.DataSet([{ from: 0, to: 1, label: &quot;1/6&quot; },\n",
"{ from: 0, to: 2, label: &quot;1/6&quot; },\n",
Expand Down Expand Up @@ -856,31 +864,31 @@
" &quot;positions&quot;: {\n",
" &quot;0&quot;: {\n",
" &quot;x&quot;: 0,\n",
" &quot;y&quot;: 0\n",
" &quot;y&quot;: -3\n",
" },\n",
" &quot;1&quot;: {\n",
" &quot;x&quot;: 114,\n",
" &quot;y&quot;: 78\n",
" &quot;x&quot;: 3,\n",
" &quot;y&quot;: -146\n",
" },\n",
" &quot;2&quot;: {\n",
" &quot;x&quot;: 7,\n",
" &quot;y&quot;: -140\n",
" &quot;x&quot;: 128,\n",
" &quot;y&quot;: -67\n",
" },\n",
" &quot;3&quot;: {\n",
" &quot;x&quot;: 127,\n",
" &quot;y&quot;: -64\n",
" &quot;x&quot;: 120,\n",
" &quot;y&quot;: 77\n",
" },\n",
" &quot;4&quot;: {\n",
" &quot;x&quot;: -112,\n",
" &quot;y&quot;: -82\n",
" &quot;x&quot;: -6,\n",
" &quot;y&quot;: 135\n",
" },\n",
" &quot;5&quot;: {\n",
" &quot;x&quot;: -14,\n",
" &quot;y&quot;: 141\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: 70\n",
" },\n",
" &quot;6&quot;: {\n",
" &quot;x&quot;: -130,\n",
" &quot;y&quot;: 56\n",
" &quot;x&quot;: -124,\n",
" &quot;y&quot;: -73\n",
" }\n",
" },\n",
" &quot;width&quot;: 381,\n",
Expand Down
Loading

0 comments on commit 300ff31

Please sign in to comment.