WIP: updating parser

mc_openapi/__main__.py

@@ -3,8 +3,8 @@ import argparse
 
 from mc_openapi.app_config import app
 from mc_openapi.doml_mc import DOMLVersion
-from mc_openapi.doml_mc.dsl_parser.exceptions import RequirementException
-from mc_openapi.doml_mc.dsl_parser.parser import Parser
+from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementException
+from mc_openapi.doml_mc.domlr_parser.parser import Parser
 from mc_openapi.doml_mc.imc import RequirementStore
 from mc_openapi.doml_mc.intermediate_model.metamodel import MetaModelDocs
 from mc_openapi.doml_mc.mc import ModelChecker

mc_openapi/doml_mc/dsl_parser/exceptions.yaml → mc_openapi/doml_mc/domlr_parser/exceptions.yaml

@@ -38,6 +38,6 @@ TOKENS:
   FORALL: a 'forall' quantifier.
 
   CLASS_PREFIX: a 'class' followed by a class name
-  ERR_DESC_SYMBOL: a '---' (three hyphens) to separate the logic expression from the error message.
+  ERR_DESC_SYMBOL: a 'error:' to separate the logic expression from the error message.
 HINTS:
   DOT: If you're trying to use a class, did you put 'class' before the class name?
\ No newline at end of file

mc_openapi/doml_mc/dsl_parser/grammar.lark → mc_openapi/doml_mc/domlr_parser/grammar.lark

 requirements    : requirement (requirement)*
 
-requirement     : FLIP_EXPR req_name expression ERR_DESC_SYMBOL error_desc
+requirement     : FLIP_EXPR req_name expression "error:" error_desc
 
 req_name        : ESCAPED_STRING
 error_desc      : ESCAPED_STRING
@@ -23,10 +23,12 @@ error_desc      : ESCAPED_STRING
                 | "(" expression ")"
                 | property
 
-?property       : CONST "has" RELATIONSHIP (CONST|value)        -> relationship_expr
+?property       : CONST "has" RELATIONSHIP (CONST|attr_rhs)     -> relationship_expr
                 | const_or_class "is" const_or_class            -> equality
                 | const_or_class "is not" const_or_class        -> inequality
-                | value COMPARISON_OP value                     -> comparison
+
+?attr_rhs       : COMPARISON_OP value                           -> attribute_value
+                | COMPARISON_OP CONST RELATIONSHIP              -> rhs_const_attribute
 
 bound_consts    : [CONST ("," CONST)*]
 
@@ -36,7 +38,6 @@ const_or_class  : "class" CLASS
 value           : ESCAPED_STRING
                 | NUMBER
                 | BOOL
-                | VALUE
 
 FLIP_EXPR       : "+"
                 | "-"
@@ -45,22 +46,16 @@ COMPARISON_OP   : ">" | ">="
                 | "<" | "<="
                 | "==" | "!="
 
-BOOL            : "!True"
-                | "!False"
+BOOL            : ":true"
+                | ":false"
 
 // regex: /[a-zA-Z]+_[a-zA-Z]+::[a-zA-Z]+/
-//RELATIONSHIP: (LCASE_LETTER) ("_"|"::"|LETTER|DIGIT)*
 RELATIONSHIP: /[^\W\d_]+\.[^\W\d_]+\.([^\W\d]|_)+/
 
-//CLASS: (LCASE_LETTER) ("_"|LETTER|DIGIT)*
 CLASS: /[^\W\d_]+\.[^\W\d_]+/
 
 // Const must start with lowercase letter
 CONST: (LCASE_LETTER) ("_"|LETTER|DIGIT)*
-// Value must start with uppercase letter
-VALUE: (UCASE_LETTER) ("_"|LETTER|DIGIT)*
-
-ERR_DESC_SYMBOL: "---"
 
 // Comment: python/sh style
 COMMENT: /#[^\n]*/

mc_openapi/doml_mc/dsl_parser/parser.py → mc_openapi/doml_mc/domlr_parser/parser.py

@@ -4,8 +4,8 @@ from typing import Callable
 
 import yaml
 from lark import Lark, Transformer, UnexpectedCharacters
-from mc_openapi.doml_mc.dsl_parser.exceptions import RequirementBadSyntaxException
-from mc_openapi.doml_mc.dsl_parser.utils import (RefHandler, StringValuesCache,
+from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementBadSyntaxException
+from mc_openapi.doml_mc.domlr_parser.utils import (RefHandler, StringValuesCache,
                                                  VarStore)
 from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
 from mc_openapi.doml_mc.imc import (Requirement, RequirementStore, SMTEncoding,
@@ -16,6 +16,7 @@ from z3 import And, Exists, ExprRef, ForAll, Implies, Not, Or, Solver, Xor, simp
 
 class ParserData:
     def __init__(self) -> None:
+        # TODO: Replace with files api?
         grammar_path = os.path.join(os.path.dirname(__file__), "grammar.lark")
         exceptions_path = os.path.join(os.path.dirname(__file__), "exceptions.yaml")
         with open(grammar_path, "r") as grammar:
@@ -30,19 +31,25 @@ class Parser:
         self.parser = Lark(grammar, start="requirements")
 
     def parse(self, input: str):
+        """Parse the input string containing the DOMLR requirements and
+           returns a tuple with:
+           - RequirementStore with the parsed requirements inside
+           - A list of strings to be added to the string constant EnumSort
+        """
         try:
             self.tree = self.parser.parse(input)
 
             const_store = VarStore()
             user_values_cache = StringValuesCache()
 
-            transformer = DSLTransformer(const_store, user_values_cache)
+            transformer = DOMLRTransformer(const_store, user_values_cache)
 
             return RequirementStore(transformer.transform(self.tree)), user_values_cache.get_list()
         except UnexpectedCharacters as e:
             ctx = e.get_context(input)
             msg = _get_error_desc_for_unexpected_characters(e, input)
 
+            # TODO: Replace before production
             print(msg)
 
             exit()
@@ -50,7 +57,7 @@ class Parser:
             # print()
             # raise RequirementBadSyntaxException(e.line, e.column, msg)       
 
-class DSLTransformer(Transformer):
+class DOMLRTransformer(Transformer):
     # These callbacks will be called when a rule with the same name
     # is matched. It starts from the leaves.
     def __init__(self, 
@@ -73,7 +80,7 @@ class DSLTransformer(Transformer):
         flip_expr: bool = args[0].value == "-"
         name: str = args[1]
         expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[2]
-        errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[4]
+        errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[3]
         index = self.const_store.get_index_and_push()
         return Requirement(
             expr,
@@ -90,6 +97,8 @@ class DSLTransformer(Transformer):
     def req_name(self, args) -> str:
         return str(args[0].value.replace('"', ''))
 
+    # Requirement requirement expression
+
     def bound_consts(self, args):
         const_names = list(map(lambda arg: arg.value, args))
         for name in const_names:
@@ -119,6 +128,7 @@ class DSLTransformer(Transformer):
         return lambda enc, sorts: ForAll(args[0](enc, sorts), args[1](enc, sorts))
 
     def relationship_expr(self, args):
+        print(args)
         rel_name = args[1].value
 
         def _gen_rel_expr(enc: SMTEncoding, sorts: SMTSorts):
@@ -148,6 +158,25 @@ class DSLTransformer(Transformer):
         
         return _gen_rel_expr
 
+    def attribute_value(self, args):
+        """Parse rhs of expression containing:
+           <, <=, >, >=, ==, != can be followed by a NUMBER
+           ==, != can be followed by a BOOL or STRING
+           should generate attr(e1, rel, attr_data_sort(VALUE)) for ==, !=
+           or attr(e1, rel, val) and get_int(val) >= NUMBER
+
+        """
+        print(args)
+        return args
+
+    def rhs_const_attribute(self, args):
+        """Parse rhs of expression
+           ==, != followed by CONST RELATIONSHIP
+           should generate attr(e1, rel, val) and attr(e2, rel, val) and e1 COMP_OP e2
+        """
+        print(args)
+        return args
+
     def _get_equality_sides(self, arg1, arg2):
         # We track use of const in const_or_class
         if arg1.type == "CONST" and arg2.type == "CONST":
@@ -181,35 +210,35 @@ class DSLTransformer(Transformer):
             self.const_store.use(args[0].value)
         return args[0]
     
-    def comparison(self, args):
-        def _gen_comparison(enc: SMTEncoding, sorts: SMTSorts):
-            a = args[0](enc, sorts)
-            b = args[2](enc, sorts)
-            op = args[1].value
-
-            # To extract the `int` contained in the attr_data_sort,
-            # we need to call its `get_int` method on the `DatatypeRef`
-            get_int = sorts.attr_data_sort.get_int
-
-            # TODO: Find a way to check if we're actually comparing Integers?
-
-            a = get_int(a)
-            b = get_int(b)
-
-            if op == ">":
-                return a > b
-            if op == ">=":
-                return a >= b
-            if op == "<":
-                return a < b
-            if op == "<=":
-                return a <= b
-            if op == "==":
-                return a == b
-            if op == "!=":
-                return a != b
-
-        return _gen_comparison
+    # def comparison(self, args):
+    #     def _gen_comparison(enc: SMTEncoding, sorts: SMTSorts):
+    #         a = args[0](enc, sorts)
+    #         b = args[2](enc, sorts)
+    #         op = args[1].value
+
+    #         # To extract the `int` contained in the attr_data_sort,
+    #         # we need to call its `get_int` method on the `DatatypeRef`
+    #         get_int = sorts.attr_data_sort.get_int
+
+    #         # TODO: Find a way to check if we're actually comparing Integers?
+
+    #         a = get_int(a)
+    #         b = get_int(b)
+
+    #         if op == ">":
+    #             return a > b
+    #         if op == ">=":
+    #             return a >= b
+    #         if op == "<":
+    #             return a < b
+    #         if op == "<=":
+    #             return a <= b
+    #         if op == "==":
+    #             return a == b
+    #         if op == "!=":
+    #             return a != b
+
+    #     return _gen_comparison
 
     def value(self, args):        
         type = args[0].type

mc_openapi/doml_mc/dsl_parser/utils.py → mc_openapi/doml_mc/domlr_parser/utils.py

 from difflib import get_close_matches
 
-from mc_openapi.doml_mc.dsl_parser.exceptions import \
+from mc_openapi.doml_mc.domlr_parser.exceptions import \
     RequirementMissingKeyException
 from mc_openapi.doml_mc.imc import SMTEncoding, SMTSorts
 from z3 import Const, DatatypeRef, ExprRef, FuncDeclRef, SortRef, Ints

mc_openapi/doml_mc/intermediate_model/metamodel.py

@@ -52,6 +52,7 @@ class DOMLAssociation:
 MetaModel = dict[str, DOMLClass]
 InverseAssociation = list[tuple[str, str]]
 
+MetaModelDocs: dict[DOMLVersion, dict] = {}
 MetaModels: dict[DOMLVersion, MetaModel] = {}
 InverseAssociations: dict[DOMLVersion, InverseAssociation] = {}
 
@@ -151,9 +152,12 @@ def parse_inverse_associations(doc: dict) -> list[tuple[str, str]]:
 
 
 def init_metamodels():
-    global MetaModels, InverseAssociations
+    global MetaModelDocs, MetaModels, InverseAssociations
     for ver in DOMLVersion:
-        mmdoc = yaml.load(ilres.read_text(assets, f"doml_meta_{ver.value}.yaml"), yaml.Loader)
+        source = ilres.files(assets).joinpath(f"doml_meta_{ver.value}.yaml")
+        
+        mmdoc = yaml.load(source.read_text()  , yaml.Loader)
+        MetaModelDocs[ver] = mmdoc
         MetaModels[ver] = parse_metamodel(mmdoc)
         InverseAssociations[ver] = parse_inverse_associations(mmdoc)
 

mc_openapi/doml_mc/mc.py

@@ -9,8 +9,7 @@ from .consistency_reqs import (get_association_multiplicity_reqs,
                                get_attribute_multiplicity_reqs,
                                get_attribute_type_reqs,
                                get_inverse_association_reqs)
-from .dsl_parser.parser import Parser
-from .imc import IntermediateModelChecker, Requirement, RequirementStore
+from .imc import IntermediateModelChecker, RequirementStore
 from .intermediate_model.metamodel import (DOMLVersion, InverseAssociations,
                                            MetaModels)
 from .mc_result import MCResult, MCResults

mc_openapi/doml_mc/synthesis_old/__init__.py

+import warnings
+warnings.warn("the synthesis module is deprecated", DeprecationWarning,
+              stacklevel=2)
\ No newline at end of file

mc_openapi/doml_mc/synthesis/xmi_gen.py → mc_openapi/doml_mc/synthesis_old/xmi_gen.py

@@ -6,7 +6,7 @@ from pyecore.ecore import EClass, EObject
 from mc_openapi.doml_mc.intermediate_model.doml_element import \
     IntermediateModel
 from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion
-from mc_openapi.doml_mc.synthesis.synthesis import AssocAndElems
+from mc_openapi.doml_mc.synthesis_old.synthesis import AssocAndElems
 from mc_openapi.doml_mc.xmi_parser.doml_model import get_rset
 
 import secrets

mc_openapi/doml_mc/xmi_parser/doml_model.py

@@ -21,8 +21,9 @@ def init_doml_rsets():  # noqa: E302
     global doml_rsets
     for ver in DOMLVersion:
         rset = ResourceSet()
+        source = ilres.files(assets).joinpath(f"doml_{ver.value}.ecore")
         resource = rset.get_resource(BytesURI(
-            "doml", bytes=ilres.read_binary(assets, f"doml_{ver.value}.ecore")
+            "doml", bytes=source.read_bytes()
         ))
         doml_metamodel = resource.contents[0]
 

tests/domlr/example_multiple_reqs.domlr

@@ -2,27 +2,33 @@
     vm is class infrastructure.VirtualMachine
     and
     not exists iface (
-        vm has infrastructure.ComputingNode->ifaces iface
+        vm has infrastructure.ComputingNode.ifaces iface
     )
-    ---
-    "VM {vm} must have iface {iface}"
+
+    error: "VM {vm} must have iface {iface}"
 
 +   "VM must have iface"
     forall vm (
         vm is class infrastructure.VirtualMachine
         implies
         exists iface (
-            vm has infrastructure.ComputingNode->ifaces iface
+            vm has infrastructure.ComputingNode.ifaces iface
         )
     )
-    ---
-    "VM {vm} must have iface {iface}"
+
+    error: "VM {vm} must have iface {iface}"
+
+# -   "Iface must be unique"
+#     ni1 has infrastructure.NetworkInterface.endPoint Value
+#     and
+#     ni1 is not ni2
+#     and
+#     ni2 has infrastructure.NetworkInterface.endPoint Value
 
 -   "Iface must be unique"
-    ni1 has infrastructure.NetworkInterface->endPoint Value
+    ni1 has infrastructure.NetworkInterface.endPoint == ni2 infrastructure.NetworkInterface.endPoint
     and
     ni1 is not ni2
-    and
-    ni2 has infrastructure.NetworkInterface->endPoint Value
-    ---
-    "Iface {ni1} and {ni2} must have different values"
+
+
+    error: "Iface {ni1} and {ni2} must have different values"

tests/domlr/example_single_req.domlr

@@ -13,7 +13,7 @@
     vm is class infrastructure.VirtualMachine
     and
     not exists iface (
-        vm has infrastructure.ComputingNode->ifaces iface
+        vm has infrastructure.ComputingNode.ifaces iface
     )
     ---
     "VM {vm} has no associated interface."

tests/domlr/example_single_req_bad_syntax.domlr

@@ -13,9 +13,9 @@
     vm is class infrastructure.VirtualMachine
     and
     not exists iface (
-        vm has infrastructure.ComputingNode->ifaces iface
+        vm has infrastructure.ComputingNode.ifaces iface
         and
-        vm has infrastructure.ComputingNode->ifaces X
+        vm has infrastructure.ComputingNode.ifaces X
     )
     ---
     "VM {vm} has no associated interface."