add Jinja2-based tapaal exporter

This commit is contained in:
Joeri Exelmans 2024-12-17 14:30:24 +01:00
parent 6aa5302e36
commit 26d8655147
4 changed files with 110 additions and 0 deletions

View file

@ -0,0 +1,6 @@
from uuid import UUID
def get_num_tokens(odapi, place: UUID):
pn_of = odapi.get_incoming(place, "pn_of")[0]
place_state = odapi.get_source(pn_of)
return odapi.get_slot_value(place_state, "numTokens")

View file

@ -0,0 +1,35 @@
from state.devstate import DevState
from bootstrap.scd import bootstrap_scd
from util import loader
from examples.petrinet.translational_semantics.tapaal.exporter import export_tapaal
if __name__ == "__main__":
import os
THIS_DIR = os.path.dirname(__file__)
# get file contents as string
def read_file(filename):
with open(THIS_DIR+'/'+filename) as file:
return file.read()
state = DevState()
scd_mmm = bootstrap_scd(state)
# Read models from their files
mm_cs = read_file('metamodels/mm_design.od')
mm_rt_cs = mm_cs + read_file('metamodels/mm_runtime.od')
# m_cs = read_file('models/m_example_simple.od')
# m_rt_initial_cs = m_cs + read_file('models/m_example_simple_rt_initial.od')
m_cs = read_file('models/m_example_mutex.od')
m_rt_initial_cs = m_cs + read_file('models/m_example_mutex_rt_initial.od')
# m_cs = read_file('models/m_example_inharc.od')
# m_rt_initial_cs = m_cs + read_file('models/m_example_inharc_rt_initial.od')
# Parse them
mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model")
mm_rt = loader.parse_and_check(state, mm_rt_cs, scd_mmm, "Petri-Net Runtime meta-model")
m = loader.parse_and_check(state, m_cs, mm, "Example model")
m_rt_initial = loader.parse_and_check(state, m_rt_initial_cs, mm_rt, "Example model initial state")
with open('exported.tapn', 'w') as f:
f.write(export_tapaal(state, m=m_rt_initial, mm=mm_rt))

View file

@ -0,0 +1,17 @@
import jinja2
import os
THIS_DIR = os.path.dirname(__file__)
from api.od import ODAPI
from examples.petrinet import helpers
from util.module_to_dict import module_to_dict
def export_tapaal(state, m, mm):
loader = jinja2.FileSystemLoader(searchpath=THIS_DIR)
environment = jinja2.Environment(loader=loader)
template = environment.get_template("tapaal.jinja2")
return template.render({
'odapi': ODAPI(state, m, mm),
**globals()['__builtins__'],
**module_to_dict(helpers),
})

View file

@ -0,0 +1,52 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<pnml xmlns="http://www.informatik.hu-berlin.de/top/pnml/ptNetb">
<net active="true" id="PN" type="P/T net">
{% for i, (place_name, place) in enumerate(odapi.get_all_instances("PNPlace")) %}
<place id="{{ place_name }}"
name="{{ place_name }}"
initialMarking="{{ get_num_tokens(odapi, place) }}"
invariant="&lt; inf"
displayName="true"
nameOffsetX="0"
nameOffsetY="0"
positionX="{{ i * 100 + 100 }}"
positionY="100"
/>
{% endfor %}
{% for i, (transition_name, transition) in enumerate(odapi.get_all_instances("PNTransition")) %}
<transition angle="0" displayName="true" id="{{ transition_name }}" infiniteServer="false" name="{{ transition_name }}" nameOffsetX="0" nameOffsetY="0" player="0" positionX="{{ i * 100 + 100 }}" positionY="300" priority="0" urgent="false"/>
{% endfor %}
{% for arc_name, arc in odapi.get_all_instances("arc") %}
<arc id="{{ arc_name }}"
inscription="{{ '[0,inf)' if odapi.get_type_name(odapi.get_source(arc)) == 'PNPlace' else '1' }}"
nameOffsetX="0"
nameOffsetY="0"
weight="1"
type="{{ 'timed' if odapi.get_type_name(odapi.get_source(arc)) == 'PNPlace' else 'normal' }}"
source="{{ odapi.get_name(odapi.get_source(arc)) }}"
target="{{ odapi.get_name(odapi.get_target(arc)) }}">
<arcpath arcPointType="false" id="0" xCoord="0" yCoord="0"/>
<arcpath arcPointType="false" id="1" xCoord="0" yCoord="0"/>
</arc>
{% endfor %}
{% for inh_arc_name, inh_arc in odapi.get_all_instances("inh_arc") %}
<arc id="{{ inh_arc_name }}"
inscription="[0,inf)"
nameOffsetX="0"
nameOffsetY="0"
type="tapnInhibitor"
weight="1"
source="{{ odapi.get_name(odapi.get_source(inh_arc)) }}"
target="{{ odapi.get_name(odapi.get_target(inh_arc)) }}">
<arcpath arcPointType="false" id="0" xCoord="0" yCoord="0"/>
<arcpath arcPointType="false" id="1" xCoord="0" yCoord="0"/>
</arc>
{% endfor %}
</net>
<feature isGame="false" isTimed="false"/>
</pnml>