Merge synthesis in CLI tool

mc_openapi/__main__.py

 #!/usr/bin/env python3
 import argparse
+import sys
+
+from doml_synthesis.data import init_data
+from doml_synthesis.requirements import builtin_requirements
+from doml_synthesis.results import check_synth_results, save_results
+from doml_synthesis.solver import solve
+from doml_synthesis.types import State
 
 from mc_openapi.app_config import app
 from mc_openapi.doml_mc import DOMLVersion
 from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementException
-from mc_openapi.doml_mc.domlr_parser.parser import DOMLRTransformer, Parser, SynthesisDOMLRTransformer
+from mc_openapi.doml_mc.domlr_parser.parser import (DOMLRTransformer, Parser,
+                                                    SynthesisDOMLRTransformer)
 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
@@ -23,7 +31,7 @@ parser.add_argument("-S", "--skip-common-checks", dest="skip_common", action='st
 parser.add_argument("-t", "--threads", dest="threads", type=int, default=2, help="number of threads used by the model checker")
 # Synthesis
 parser.add_argument("-s", "--synth", dest="synth", action='store_true', help="synthetize a new DOMLX file from requirements")
-parser.add_argument("-m", "--max-tries", dest="tries", type=int, default=10, help="max number of iteration while trying to solve the model with unbounded variables")
+parser.add_argument("-m", "--max-tries", dest="tries", type=int, default=8, help="max number of iteration while trying to solve the model with unbounded variables")
 
 args = parser.parse_args()
 
@@ -71,8 +79,9 @@ else:
             domlr_parser = Parser(DOMLRTransformer)
             user_req_store, user_req_str_consts = domlr_parser.parse(user_reqs)
         except Exception as e:
-            print(e)
-            raise RuntimeError("Failed to parse the DOMLR.")
+            print(e, file=sys.stderr)
+            print("Failed to parse the DOMLR.", file=sys.stderr)
+            exit(-1)
 
     if not args.synth:
         try:
@@ -97,12 +106,7 @@ else:
 
     else: # Synthesis
         printv("Running synthesis...")
-        # Lazy load libraries
-        from doml_synthesis.types import State
-        from doml_synthesis.data import init_data
-        from doml_synthesis.solver import solve
-        from doml_synthesis.requirements import builtin_requirements
-        from doml_synthesis.results import check_synth_results, save_results
+        
 
         # Required files:
         mm = MetaModelDocs[doml_ver]
@@ -118,19 +122,29 @@ else:
         }
 
         # Parse
+        try:
             synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
-        synth_user_reqs, user_reqs_strings = synth_domlr_parser.parse(user_reqs)
-
-        print(user_reqs_strings)
+            synth_user_reqs, user_reqs_strings = synth_domlr_parser.parse(user_reqs, for_synthesis=True)
+        except Exception as e:
+            print(e, file=sys.stderr)
+            print("Failed to parse the DOMLR.", file=sys.stderr)
+            exit(-1)
 
         state = State()
         # Parse MM and IM
-        state = init_data(state, doml=im, metamodel=mm)
-        # Solve
+        state = init_data(
+            state, 
+            doml=im, 
+            metamodel=mm, 
+        )
+
+        reqs = [synth_user_reqs]
+        if not args.skip_common:
+            reqs.append(builtin_requirements)
 
         state = solve(
             state, 
-            requirements=[builtin_requirements, synth_user_reqs], 
+            requirements=reqs, 
             strings=user_reqs_strings,
             max_tries=args.tries
         )

mc_openapi/doml_mc/domlr_parser/parser.py

@@ -3,7 +3,7 @@ import re
 from typing import Callable
 
 import yaml
-from lark import Lark, Transformer, UnexpectedCharacters
+from lark import Lark, Transformer, UnexpectedCharacters, UnexpectedEOF
 from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementBadSyntaxException
 from mc_openapi.doml_mc.domlr_parser.utils import (RefHandler, StringValuesCache, SynthesisRefHandler,
                                                  VarStore)
@@ -28,10 +28,10 @@ PARSER_DATA = ParserData()
 
 class Parser:
     def __init__(self, transformer, grammar: str = PARSER_DATA.grammar):
-        self.parser = Lark(grammar, start="requirements")
+        self.parser = Lark(grammar, start="requirements", parser="lalr")
         self.transformer = transformer
 
-    def parse(self, input: str):
+    def parse(self, input: str, for_synthesis: bool = False):
         """Parse the input string containing the DOMLR requirements and
            returns a tuple with:
            - RequirementStore with the parsed requirements inside
@@ -45,7 +45,7 @@ class Parser:
 
             transformer = self.transformer(const_store, user_values_cache)
 
-            if isinstance(self.transformer, DOMLRTransformer):
+            if not for_synthesis:
                 return (
                     RequirementStore(transformer.transform(self.tree)), 
                     user_values_cache.get_list()
@@ -63,17 +63,16 @@ class Parser:
 
                 return user_reqs, user_values_cache.get_list()
 
+        except UnexpectedEOF as e:
+            msg =  "Unexpected End of File:\n"
+            msg += "Did you forget the `error:` message at the end of a requirement?"
+            raise Exception(msg)
+
         except UnexpectedCharacters as e:
-            ctx = e.get_context(input)
             msg = _get_error_desc_for_unexpected_characters(e, input)
+            raise RequirementBadSyntaxException(e.line, e.column, msg)
        
-            # TODO: Replace before production
-            print(msg)
         
-            exit()
-            # print()
-            # print()
-            # raise RequirementBadSyntaxException(e.line, e.column, msg)       
 
 class DOMLRTransformer(Transformer):
     # These callbacks will be called when a rule with the same name

mc_openapi/doml_mc/mc.py

@@ -45,8 +45,6 @@ class ModelChecker:
                 + get_association_multiplicity_reqs(self.metamodel) \
                 + get_inverse_association_reqs(self.inv_assoc)
         
-        user_str_values = []
-
         if user_requirements:
             req_store += user_requirements
 

requirements.txt

+alabaster==0.7.13
 attrs==22.2.0
+Babel==2.11.0
+beautifulsoup4==4.11.1
 certifi==2022.12.7
 charset-normalizer==3.0.1
 click==8.1.3
 clickclick==20.10.2
 connexion==2.14.2
+docutils==0.19
 Flask==2.2.2
+furo==2022.12.7
 future-fstrings==1.2.0
 h11==0.14.0
 idna==3.4
+imagesize==1.4.1
 inflection==0.5.1
 iniconfig==2.0.0
 itsdangerous==2.1.2
@@ -20,15 +26,29 @@ MarkupSafe==2.1.2
 networkx==3.0
 ordered-set==4.1.0
 packaging==23.0
+piacere-doml-synthesis==2023.1.3
 pluggy==1.0.0
 pyecore==0.13.0
+Pygments==2.14.0
 pyrsistent==0.19.3
 pytest==7.2.1
+pytz==2022.7.1
 PyYAML==6.0
 requests==2.28.2
 RestrictedPython==6.0
+snowballstemmer==2.2.0
+soupsieve==2.3.2.post1
+Sphinx==6.1.3
+sphinx-basic-ng==1.0.0b1
+sphinxcontrib-applehelp==1.0.4
+sphinxcontrib-devhelp==1.0.2
+sphinxcontrib-htmlhelp==2.0.0
+sphinxcontrib-jsmath==1.0.1
+sphinxcontrib-qthelp==1.0.3
+sphinxcontrib-serializinghtml==1.1.5
 swagger-ui-bundle==0.0.9
+termcolor==2.2.0
 urllib3==1.26.14
 uvicorn==0.20.0
 Werkzeug==2.2.2
-z3-solver==4.12.1.0
+z3-solver==4.11.2.0

tests/domlr/example_single_req.domlr

@@ -15,5 +15,4 @@
     not exists iface (
         vm has infrastructure.ComputingNode.ifaces iface
     )
-    ---
-    "VM {vm} has no associated interface."
+    error: "VM {vm} has no associated interface."

tests/domlr/example_vm_has_sizedesc_cpu_count.domlr

++   "VM has size description and cpu_count >= 4"
+    forall vm (
+        vm is class infrastructure.VirtualMachine
+        implies
+            vm has infrastructure.VirtualMachine.sizeDescription == "EXAMPLE"
+            and
+            vm has infrastructure.ComputingNode.cpu_count >= 4
+    )
+    error: "Model is wrong..."
\ No newline at end of file