"""Parser
This file provides all uppaal parsers required to create an executable uppaal model.
This file can be imported as a module and contains the following classes:
* UppaalParser: Interface for all uppaal parsers.
* SystemParser: Uppaal parser for parsing an uppaal system.
* AutomatonParser: Uppaal parser for parsing an uppaal automaton.
* LocationParser: Uppaal parser for parsing an uppaal location.
* TransitionParser: Uppaal parser for parsing an uppaal transition.
"""
from __future__ import annotations
import logging
import re
from abc import ABC, abstractmethod
from typing import Dict, List, Tuple
from bs4 import Tag
from uppaal2jetracer.declarations.declarations_tree_visitor import DeclarationsTreeVisitor
from uppaal2jetracer.parser.declarationparser.declaration_parser import DeclarationParser, \
SingleStatementParser
from uppaal2jetracer.controller.executor import Executor
from uppaal2jetracer.declarations.declarations_ast import Node, ID, FileAST
from uppaal2jetracer.uppaalmodel.elements import Invariant, Transition, Guard, Update, \
Synchronization
from uppaal2jetracer.uppaalmodel.frame import Frame
from uppaal2jetracer.uppaalmodel.system import Automaton, Location, System, UppaalElement
logger = logging.getLogger("parser")
dp: DeclarationParser = DeclarationParser(lex_optimize = False,
yacc_optimize = False,
yacc_debug = False)
ssp: SingleStatementParser = SingleStatementParser(lex_optimize = False,
yacc_optimize = False,
yacc_debug = False)
[docs]
class UppaalParser(ABC):
"""
Abstract base class for all parsers that convert an XMl file to UPPAAL model objects.
"""
_AUTOMATON_KEY = "template"
_FRAME_KEY = "declaration"
_GUARD_KEY = "guard"
_ID_KEY = "id"
_INITIAL_KEY = "init"
_INVARIANT_KEY = "invariant"
_REFERENCE_KEY = "ref"
_LOCATION_KEY = "location"
_NAME_KEY = "name"
_PARAMETER_KEY = "parameter"
_SOURCE_KEY = "source"
_SYNC_KEY = "synchronisation"
_SYSTEM_KEY = "system"
_TARGET_KEY = "target"
_TRANSITION_KEY = "transition"
_UPDATE_KEY = "assignment"
_COMMENT_KEY = "//"
_ASSIGNMENT_KEY = "="
_OPEN_BRACKET_KEY = "("
_CALL_BY_REF_KEY = "&"
_ENUMERATION_KEY = ","
_CLOSE_BRACKET_KEY = ")"
_LINE_END_KEY = ";"
_LINE_SEPERATOR = "\n"
_AUTOMATON_DECL_REGEX = (r"^ *[A-z_]([A-z0-9_])* *="
r" *[A-z_]([A-z0-9_])*\( *(([A-z_]([A-z0-9_])*, *)*"
r"[A-z_]([A-z0-9_])*)?\) *;")
_IDENTIFIER_REGEX = r"^ *[A-z_]([A-z0-9_])* *= *"
[docs]
@staticmethod
@abstractmethod
def parse(t: Tag) -> UppaalElement:
"""
Parses an XML tag to UPPAAL element.
:param t: XML tag to parse.
:type t: Tag
:return: List of UPPAAL elements.
:rtype: List[UppaalElement]
"""
@staticmethod
def _remove_line_comment(text: str) -> str:
return text.split(UppaalParser._COMMENT_KEY)[0].strip()
@staticmethod
def _remove_all_comments(text: str) -> str:
trimmed_text = ""
for line in text.splitlines():
trimmed_text += line.split(UppaalParser._COMMENT_KEY)[0] + UppaalParser._LINE_SEPERATOR
return trimmed_text.removesuffix(UppaalParser._LINE_SEPERATOR)
[docs]
class SystemParser(UppaalParser):
"""
An UPPAAL parser that parses UPPAAL systems.
"""
[docs]
@staticmethod
def parse(t: Tag) -> System:
"""
Parse an XML tag to UPPAAL system.
:param t: XML tag to parse.
:type t: Tag
:return: UPPAAL system.
:rtype: [System]
"""
if t.find(UppaalParser._FRAME_KEY) is None:
raise XMLParseError("No global declaration found.")
global_frame: Frame = SystemParser._create_frame(t.find(UppaalParser._FRAME_KEY))
logger.info("Parsed global frame.")
# Get automata names.
templates: Dict[str, Tag] = {}
for automaton_tag in t.find_all(UppaalParser._AUTOMATON_KEY):
if automaton_tag.find(UppaalParser._NAME_KEY) is None:
raise XMLParseError("Automaton has no name.")
name = automaton_tag.find(UppaalParser._NAME_KEY).text
templates.update({name: automaton_tag})
# Create and parse system frame.
system_frame: Frame = Frame(global_frame)
executor: Executor = Executor(system_frame)
automata: List[Automaton] = []
declared_automata: Dict[str, Automaton] = {}
if t.find(UppaalParser._SYSTEM_KEY) is None:
raise XMLParseError("No system declaration found.")
lines: List[str] = t.find(UppaalParser._SYSTEM_KEY).text.splitlines()
for line in lines:
line = UppaalParser._remove_line_comment(line)
if re.match(UppaalParser._AUTOMATON_DECL_REGEX, line):
# Parse automaton call.
identifier: str = line.split(UppaalParser._ASSIGNMENT_KEY)[0].strip()
line = re.sub(UppaalParser._IDENTIFIER_REGEX, "", line)
automaton_call: Tuple[str, List[FileAST]] = SystemParser._create_automaton_call(
line.strip()
)
automaton_tag = templates.get(automaton_call[0], None)
if automaton_tag is None:
raise XMLParseError(f"No automaton with name '{automaton_call[0]}' "
f"defined.")
declared_automata.update(
{identifier: AutomatonParser.parse(
automaton_tag, global_frame, system_frame, automaton_call[1]
)}
)
elif line.startswith(UppaalParser._SYSTEM_KEY):
# Create declared automata.
line = (line.removeprefix(UppaalParser._SYSTEM_KEY).replace(" ", "")
.removesuffix(UppaalParser._LINE_END_KEY))
system_automata: List[str] = line.split(UppaalParser._ENUMERATION_KEY)
for system_automaton in system_automata:
automata.append(declared_automata.get(system_automaton.strip(), None))
break
else:
line_node = dp.parse(line)
logger.debug("Parsed declaration: %s", line_node.accept(DeclarationsTreeVisitor()))
line_node.accept(executor)
return System(global_frame, system_frame, automata)
@staticmethod
def _create_frame(t: Tag) -> Frame:
declaration: Node = dp.parse(UppaalParser._remove_all_comments(t.text))
logger.debug("Parsed declaration: %s", declaration.accept(DeclarationsTreeVisitor()))
new_frame: Frame = Frame()
executor: Executor = Executor(new_frame)
declaration.accept(executor)
return new_frame
@staticmethod
def _create_automaton_call(text: str) -> Tuple[str, List[FileAST]]:
text = UppaalParser._remove_line_comment(text)
split_name_params: List[str] = text.replace(" ", "").replace(
UppaalParser._LINE_END_KEY,
"").split(UppaalParser._OPEN_BRACKET_KEY)
# Get parameters.
params: List[FileAST] = []
for param in (split_name_params[1].replace(UppaalParser._CLOSE_BRACKET_KEY, "")
.split(UppaalParser._ENUMERATION_KEY)):
if param:
param_node: FileAST = ssp.parse(param.strip())
logger.debug("Parsed declaration: %s",
param_node.accept(DeclarationsTreeVisitor()))
params.append(param_node)
return split_name_params[0], params
@staticmethod
def _create_automaton(t: Tag) -> Automaton:
return AutomatonParser.parse(t)
[docs]
class AutomatonParser(UppaalParser):
"""
An UPPAAL parser that parses UPPAAL automata.
"""
[docs]
@staticmethod
def parse(t: Tag, global_frame: Frame = None, system_frame: Frame = None,
params: List[FileAST] = None) -> Automaton:
"""
Parse an XML tag to UPPAAL automata.
:param t: XML tag to parse.
:type t: Tag
:param global_frame: Global frame.
:type global_frame: Frame
:param system_frame: System frame.
:type system_frame: Frame
:param params: Parameters to parse.
:type params: List[str]
:return: List of UPPAAL automata.
:rtype: List[Automaton]
"""
name: str = t.find(UppaalParser._NAME_KEY).text
if name is None:
raise XMLParseError("Automaton has no name.")
logger.debug("Parsed automaton name '%s'.", name)
automaton_frame: Frame = AutomatonParser._create_frame(
global_frame,
system_frame,
t.find(UppaalParser._PARAMETER_KEY),
params,
t.find(UppaalParser._FRAME_KEY)
)
logger.info("Parsed automaton frame.")
locations: Dict[str, Location] = {}
for location_tag in t.find_all(UppaalParser._LOCATION_KEY):
new_location: Location = AutomatonParser._create_location(location_tag)
locations.update({new_location.identifier: new_location})
logger.info("Parsed location '%s'.", new_location.identifier)
initial_location: Location = locations.get(
t.find(UppaalParser._INITIAL_KEY).get(UppaalParser._REFERENCE_KEY)
)
if initial_location is None:
raise XMLParseError(f"Automaton '{name}' has no initial location.")
logger.debug(
"Parsed initial location '%s'.",
t.find(UppaalParser._INITIAL_KEY).get(UppaalParser._REFERENCE_KEY)
)
transitions: List[Transition] = []
for transition_tag in t.find_all(UppaalParser._TRANSITION_KEY):
new_transition: Transition = AutomatonParser._create_transition(transition_tag)
source_location = locations.get(
transition_tag.find(UppaalParser._SOURCE_KEY).get(UppaalParser._REFERENCE_KEY)
)
if source_location is None:
raise XMLParseError("Transition has no source location.")
new_transition.source = source_location
source_location.add_transition(new_transition)
logger.debug("Set source of transition to '%s'.", new_transition.source.identifier)
target_location = locations.get(
transition_tag.find(UppaalParser._TARGET_KEY).get(UppaalParser._REFERENCE_KEY), None
)
if target_location is None:
raise XMLParseError("Transition has no target location.")
new_transition.target = target_location
logger.debug("Set target of transition to '%s'.", new_transition.target.identifier)
transitions.append(new_transition)
logger.info("Parsed transition.")
return Automaton(name, automaton_frame, list(locations.values()), initial_location)
@staticmethod
def _create_frame(global_frame: Frame, system_frame: Frame, param_tag: Tag,
params: List[FileAST], frame_tag: Tag) -> Frame:
new_frame: Frame = Frame(system_frame)
executor: Executor = Executor(new_frame)
if param_tag is not None:
for i, param in enumerate(param_tag.text.split(UppaalParser._ENUMERATION_KEY)):
call_by_reference = UppaalParser._CALL_BY_REF_KEY in param
param = param.replace(UppaalParser._CALL_BY_REF_KEY, "")
name = param.strip().split(" ").pop()
declaration: Node = dp.parse(param.strip() + UppaalParser._LINE_END_KEY)
logger.debug("Parsed declaration: %s",
declaration.accept(DeclarationsTreeVisitor()))
declaration.accept(executor)
if call_by_reference:
ref: ID = params[i].ext[0]
new_frame.add_binding(name, new_frame.get_variable(ref.name))
else:
new_frame.get_variable(name).value = params[i].accept(executor)
new_frame.parent = global_frame
if frame_tag is not None:
declaration: Node = dp.parse(UppaalParser._remove_all_comments(frame_tag.text))
logger.debug("Parsed declaration: %s", declaration.accept(DeclarationsTreeVisitor()))
declaration.accept(executor)
return new_frame
@staticmethod
def _create_location(t: Tag) -> Location:
return LocationParser.parse(t)
@staticmethod
def _create_transition(t: Tag) -> Transition:
return TransitionParser.parse(t)
[docs]
class LocationParser(UppaalParser):
"""
An UPPAAL parser that parses UPPAAL locations.
"""
[docs]
@staticmethod
def parse(t: Tag) -> Location:
"""
Parse an XML tag to UPPAAL locations.
:param t: XML tag to parse.
:type t: Tag
:return: List of UPPAAL locations.
:rtype: List[Location]
"""
identifier: str = t.get(UppaalParser._ID_KEY)
if identifier is None:
raise XMLParseError("Location has no identifier.")
logger.debug("Parsed location identifier '%s'.", identifier)
name_tag: Tag = t.find(UppaalParser._NAME_KEY)
name = None
if name_tag is not None:
name = t.find(UppaalParser._NAME_KEY).text
logger.debug("Parsed location identifier '%s'.", name)
invariant_tag: Tag = t.find(kind = UppaalParser._INVARIANT_KEY)
invariant = None
if invariant_tag is not None:
invariant = LocationParser._create_invariant(invariant_tag)
logger.debug("Parsed invariant '%s'.", invariant_tag.text)
else:
logger.debug("Location '%s' has no invariant.", identifier)
return Location(identifier, name, invariant)
@staticmethod
def _create_invariant(t: Tag) -> Invariant:
decision: Node = ssp.parse(t.text)
logger.debug("Parsed declaration: %s", decision.accept(DeclarationsTreeVisitor()))
return Invariant(decision)
[docs]
class TransitionParser(UppaalParser):
"""
An UPPAAL parser that parses UPPAAL transitions.
"""
_RECEIVING_KEY = "?"
_SENDING_KEY = "!"
[docs]
@staticmethod
def parse(t: Tag) -> Transition:
"""
Parse an XML tag to UPPAAL transitions.
:param t: XML tag to parse.
:type t: Tag
:return: List of UPPAAL automata.
:rtype: List[Transition]
"""
guard_tag: Tag = t.find(kind = UppaalParser._GUARD_KEY)
guard = None
if guard_tag is not None:
guard = TransitionParser._create_guard(guard_tag)
logger.debug("Parsed guard '%s'.", guard_tag.text)
else:
logger.debug("Transition has no guard.")
update_tag: Tag = t.find(kind = UppaalParser._UPDATE_KEY)
update = None
if update_tag is not None:
update = TransitionParser._create_update(update_tag)
logger.debug("Parsed update '%s'.", update_tag.text)
else:
logger.debug("Transition has no update.")
sync_tag: Tag = t.find(kind = UppaalParser._SYNC_KEY)
sync = None
if sync_tag is not None:
sync = TransitionParser._create_synchronization(sync_tag)
logger.debug("Parsed synchronization '%s'.", sync_tag.text)
else:
logger.debug("Transition has no synchronization.")
return Transition(guard, update, sync)
@staticmethod
def _create_guard(t: Tag) -> Guard:
guard: Node = ssp.parse(t.text)
logger.debug("Parsed declaration: %s", guard.accept(DeclarationsTreeVisitor()))
return Guard(guard)
@staticmethod
def _create_update(t: Tag) -> Update:
updates: List[Node] = []
for text in t.text.split(UppaalParser._ENUMERATION_KEY):
text = text.strip()
updates.append(ssp.parse(text))
logger.debug("Parsed declaration: %s", updates[-1].accept(DeclarationsTreeVisitor()))
return Update(updates)
@staticmethod
def _create_synchronization(t: Tag) -> Synchronization:
text: str = t.text
sending: bool = TransitionParser._SENDING_KEY in text
text = text.replace(TransitionParser._RECEIVING_KEY, "")
text = text.replace(TransitionParser._SENDING_KEY, "")
text = text.strip()
sync: Node = ssp.parse(text)
logger.debug("Parsed declaration: %s", sync.accept(DeclarationsTreeVisitor()))
return Synchronization(sending, sync)
[docs]
class XMLParseError(Exception):
"""
An error class for XML parsing.
"""
def __init__(self, message: str):
super().__init__("Error: " + message)
logger.error(message)