{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Modelverse Interfacing with external service (LoLA)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this notebook, we will show how to use LoLA as an external service for Petri Net reachability analysis.\n",
"LoLA will also return the path indicating how to reach the offending state, which we will also visualize as a model."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Initialization"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"First we initialize the Modelverse as usual by importing the wrapper and logging in as some user (in our case the \"admin\" user)."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import sys\n",
"sys.path.append(\"../wrappers/\")\n",
"from modelverse import *\n",
"init()\n",
"login(None, None)\n",
"\n",
"from IPython.display import SVG, display\n",
"\n",
"def view(model_name):\n",
" svg = SVG()\n",
" svg.data = show(model_name)\n",
" display(svg)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Adding metamodels"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add the PetriNets metamodel and show it."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"model_add(\"~/formalisms/PetriNets\", \"formalisms/SimpleClassDiagrams\", \"\"\"\n",
" SimpleAttribute Natural {}\n",
" SimpleAttribute String {}\n",
"\n",
" Class Place {\n",
" name = \"Place\"\n",
" tokens : Natural\n",
" name : String\n",
" }\n",
" Class Transition {\n",
" name = \"Transition\"\n",
" name : String\n",
" }\n",
" Association P2T (Place, Transition) {\n",
" name = \"P2T\"\n",
" weight : Natural\n",
" }\n",
" Association T2P (Transition, Place) {\n",
" name = \"T2P\"\n",
" weight : Natural\n",
" }\n",
" \"\"\")\n",
"view(\"~/formalisms/PetriNets\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add the Query metamodel and show it."
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"model_add(\"~/formalisms/Query\", \"formalisms/SimpleClassDiagrams\", \"\"\"\n",
" include \"primitives.alh\"\n",
" include \"object_operations.alh\"\n",
" include \"modelling.alh\"\n",
"\n",
" SimpleAttribute String {\n",
" name = \"String\"\n",
" }\n",
" SimpleAttribute Natural {\n",
" name = \"Natural\"\n",
" }\n",
"\n",
" Class Place {\n",
" name = \"Place\"\n",
" name : String\n",
" tokens : Natural\n",
" lower_cardinality = 1\n",
" upper_cardinality = 1\n",
" }\n",
" \"\"\")\n",
"view(\"~/formalisms/Query\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add the PetriNets execution path formalism and show it."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"model_add(\"~/formalisms/PNPath\", \"formalisms/SimpleClassDiagrams\", \"\"\"\n",
" SimpleAttribute String {\n",
" name = \"String\"\n",
" }\n",
" \n",
" Class Entry {\n",
" name = \"Entry\"\n",
" name : String\n",
" }\n",
" \n",
" Class First : Entry {\n",
" name = \"First\"\n",
" lower_cardinality = 1\n",
" upper_cardinality = 1\n",
" }\n",
" \n",
" Association Next (Entry, Entry){\n",
" source_upper_cardinality = 1\n",
" target_upper_cardinality = 1\n",
" }\n",
" \"\"\")\n",
"view(\"~/formalisms/PNPath\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add the reachability analysis code, relying on the LoLA service.\n",
"This code basically only has to serialize the PetriNets and Query model in LoLA format, and then forwards it.\n",
"Upon receiving a response from the service, the reachable path is serialized to its own model, which can be used however the user wants."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
"transformation_add_AL({\"PN\": \"~/formalisms/PetriNets\", \"Query\": \"~/formalisms/Query\"}, {\"Path\": \"~/formalisms/PNPath\"}, \"~/models/analyze_lola\", \"\"\"\n",
"include \"primitives.alh\"\n",
"include \"modelling.alh\"\n",
"include \"object_operations.alh\"\n",
"include \"services.alh\"\n",
"\n",
"Boolean function lola_format(model : Element):\n",
" Element all_places\n",
" String place\n",
" String name\n",
" Integer tokens\n",
" String transition\n",
" Element all_transitions\n",
" Element associations\n",
" Element association\n",
" String weight\n",
" String lola_net\n",
" String query\n",
" String place_output\n",
" String marking_output\n",
" String transition_output\n",
" String outp\n",
"\n",
" all_places = allInstances(model, \"PN/Place\")\n",
" place_output = \"PLACE \"\n",
" marking_output = \"MARKING \"\n",
" while (set_len(all_places) > 0):\n",
" place = set_pop(all_places)\n",
" name = read_attribute(model, place, \"name\")\n",
" tokens = read_attribute(model, place, \"tokens\")\n",
"\n",
" place_output = string_join(place_output, name)\n",
"\n",
" if tokens > 0:\n",
" if marking_output != \"MARKING \":\n",
" marking_output = string_join(marking_output, \", \")\n",
" marking_output = string_join(marking_output, name)\n",
" marking_output = string_join(marking_output, \": \")\n",
" marking_output = string_join(marking_output, cast_string(tokens))\n",
" \n",
" if list_len(all_places) == 0:\n",
" place_output = string_join(place_output, \";\")\n",
" marking_output = string_join(marking_output, \";\")\n",
" else:\n",
" place_output = string_join(place_output, \", \")\n",
"\n",
" lola_net = string_join(place_output, marking_output)\n",
"\n",
" all_transitions = allInstances(model, \"PN/Transition\")\n",
" transition_output = \"\"\n",
" while (set_len(all_transitions) > 0):\n",
" transition = set_pop(all_transitions)\n",
" name = read_attribute(model, transition, \"name\")\n",
"\n",
" transition_output = string_join(transition_output, \" TRANSITION \")\n",
" transition_output = string_join(transition_output, name)\n",
" transition_output = string_join(transition_output, \" CONSUME \")\n",
"\n",
" associations = allIncomingAssociationInstances(model, transition, \"PN/P2T\")\n",
" while (set_len(associations) > 0):\n",
" association = set_pop(associations)\n",
" place = readAssociationSource(model, association)\n",
" weight = read_attribute(model, association, \"weight\")\n",
" if cast_integer(weight) > 0:\n",
" transition_output = string_join(transition_output, read_attribute(model, place, \"name\"))\n",
" transition_output = string_join(transition_output, \": \")\n",
" transition_output = string_join(transition_output, weight)\n",
"\n",
" if list_len(associations) == 0:\n",
" transition_output = string_join(transition_output, \";\")\n",
" else:\n",
" transition_output = string_join(transition_output, \", \")\n",
"\n",
" transition_output = string_join(transition_output, \" PRODUCE \")\n",
"\n",
" associations = allOutgoingAssociationInstances(model, transition, \"PN/T2P\")\n",
" while (set_len(associations) > 0):\n",
" association = set_pop(associations)\n",
" place = readAssociationDestination(model, association)\n",
" weight = read_attribute(model, association, \"weight\")\n",
" if cast_integer(weight) > 0:\n",
" transition_output = string_join(transition_output, read_attribute(model, place, \"name\"))\n",
" transition_output = string_join(transition_output, \": \")\n",
" transition_output = string_join(transition_output, weight)\n",
"\n",
" if list_len(associations) == 0:\n",
" transition_output = string_join(transition_output, \";\")\n",
" else:\n",
" transition_output = string_join(transition_output, \", \")\n",
"\n",
" lola_net = string_join(lola_net, transition_output)\n",
"\n",
" all_places = allInstances(model, \"Query/Place\")\n",
" if set_len(all_places) > 0:\n",
" place = set_pop(all_places)\n",
" name = read_attribute(model, place, \"name\")\n",
" tokens = read_attribute(model, place, \"tokens\")\n",
" query = string_join(name, ' = ')\n",
" query = string_join(query, cast_string(tokens))\n",
"\n",
" outp = string_join(\"{\\\\\"petrinet\\\\\":\\\\\"\", lola_net)\n",
" outp = string_join(outp, \"\\\\\" , \\\\\"query\\\\\":\\\\\"\")\n",
" outp = string_join(outp, query)\n",
" outp = string_join(outp, \"\\\\\"}\")\n",
" \n",
" String port\n",
" port = comm_connect(\"lola\")\n",
" comm_set(port, outp)\n",
"\n",
" String result\n",
" String path\n",
" result = comm_get(port)\n",
" path = comm_get(port)\n",
" \n",
" Element path_elements\n",
" String first\n",
" String elem\n",
" String prev\n",
" path_elements = string_split(path, \",\")\n",
" if (list_len(path_elements) > 0):\n",
" first = instantiate_node(model, \"Path/First\", \"\")\n",
" prev = first\n",
" instantiate_attribute(model, first, \"name\", list_pop(path_elements, 0))\n",
" while (list_len(path_elements) > 0):\n",
" elem = instantiate_node(model, \"Path/Entry\", \"\")\n",
" instantiate_attribute(model, elem, \"name\", list_pop(path_elements, 0))\n",
" instantiate_link(model, \"Path/Next\", \"\", prev, elem)\n",
" prev = elem\n",
" \n",
" comm_close(port)\n",
"\n",
" return cast_boolean(result)!\n",
" \"\"\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Add models under test"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add a simple Petri Nets model to test with."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"model_add(\"~/models/PN\", \"~/formalisms/PetriNets\", \"\"\"\n",
" Place critical_section_1 {\n",
" tokens = 1\n",
" name = \"critical_section_1\"\n",
" }\n",
" Place critical_section_2 {\n",
" tokens = 0\n",
" name = \"critical_section_2\"\n",
" }\n",
" Place lock_available {\n",
" tokens = 1\n",
" name = \"lock_available\"\n",
" }\n",
"\n",
" Transition release_section_1 {\n",
" name = \"release_section_1\"\n",
" }\n",
" Transition release_section_2 {\n",
" name = \"release_section_2\"\n",
" }\n",
" Transition acquire_section_1 {\n",
" name = \"acquire_section_1\"\n",
" }\n",
" Transition acquire_section_2 {\n",
" name = \"acquire_section_2\"\n",
" }\n",
"\n",
" P2T (critical_section_1, release_section_1) {\n",
" weight = 1\n",
" }\n",
"\n",
" P2T (critical_section_2, release_section_2) {\n",
" weight = 1\n",
" }\n",
"\n",
" P2T (lock_available, acquire_section_1) {\n",
" weight = 1\n",
" }\n",
"\n",
" P2T (lock_available, acquire_section_2) {\n",
" weight = 1\n",
" }\n",
"\n",
" T2P (release_section_1, lock_available) {\n",
" weight = 1\n",
" }\n",
"\n",
" T2P (release_section_2, lock_available) {\n",
" weight = 1\n",
" }\n",
"\n",
" T2P (acquire_section_1, critical_section_1) {\n",
" weight = 1\n",
" }\n",
"\n",
" T2P (acquire_section_2, critical_section_2) {\n",
" weight = 1\n",
" }\n",
"\n",
" Place check {\n",
" tokens = 0\n",
" name = \"ERROR\"\n",
" }\n",
" Transition error {\n",
" name = \"both_enabled\"\n",
" }\n",
" P2T (critical_section_1, error) {\n",
" weight = 1\n",
" }\n",
" P2T (critical_section_2, error) {\n",
" weight = 1\n",
" }\n",
" T2P (error, check) {\n",
" weight = 1\n",
" }\n",
" \"\"\")\n",
"view(\"~/models/PN\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Add a simple Query model to check whether it is reachable or not, and subsequently show it."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"model_add(\"~/models/Query\", \"~/formalisms/Query\", \"\"\"\n",
" Place error {\n",
" name = \"ERROR\"\n",
" tokens = 1\n",
" }\n",
" \"\"\")\n",
"view(\"~/models/Query\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Execution"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, we actually invoke the activity, thereby visualizing the error path if applicable."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"transformation_execute_AL(\"~/models/analyze_lola\", {\"PN\": \"~/models/PN\", \"Query\": \"~/models/Query\"}, {\"Path\": \"~/models/Path\"})\n",
"view(\"~/models/Path\")"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
}
},
"nbformat": 4,
"nbformat_minor": 2
}