Source code for uppaal2jetracer.parser.parser

"""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: if declared_automata.get(system_automaton.strip(), None) is None: raise XMLParseError(f"Automaton '{system_automaton.strip()}' was not " f"declared.") 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) if len(automata) == 0: raise XMLParseError("No system creation found.") 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_tag: Tag = t.find(UppaalParser._NAME_KEY) if name_tag is None: raise XMLParseError("Automaton has no name.") name: str = name_tag.text.strip() 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_tag: Tag = t.find(UppaalParser._INITIAL_KEY) if initial_tag is None: raise XMLParseError(f"Automaton '{name}' has no initial tag.") initial_location: Location = locations.get( initial_tag.get(UppaalParser._REFERENCE_KEY), None ) 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) ) for transition_tag in t.find_all(UppaalParser._TRANSITION_KEY): new_transition: Transition = AutomatonParser._create_transition(transition_tag) source_tag: Tag = transition_tag.find(UppaalParser._SOURCE_KEY) if source_tag is None: raise XMLParseError("Transition has no source tag.") source_location: Location = locations.get( source_tag.get(UppaalParser._REFERENCE_KEY), None ) 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_tag: Tag = transition_tag.find(UppaalParser._TARGET_KEY) if target_tag is None: raise XMLParseError("Transition has no target tag.") target_location: Location = locations.get( target_tag.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) 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 None: if params is not None and len(params) != 0: raise XMLParseError("Too many parameters provided.") else: if len(params) != len(param_tag.text.split(UppaalParser._ENUMERATION_KEY)): raise XMLParseError("Wrong number of parameters provided.") 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__(message) logger.error(message)