diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py
index 4aa03e45497fd6a1e4934b95d45c51d5dcfe8a57..9f8607ab5db3a02a87e56c0ecaba90f86c22e0f6 100644
--- a/mc_openapi/__main__.py
+++ b/mc_openapi/__main__.py
@@ -1,10 +1,18 @@
#!/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,20 +122,30 @@ else:
}
# Parse
- synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
- synth_user_reqs, user_reqs_strings = synth_domlr_parser.parse(user_reqs)
+ try:
+ synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
+ 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)
- print(user_reqs_strings)
-
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],
- strings=user_reqs_strings,
+ requirements=reqs,
+ strings=user_reqs_strings,
max_tries=args.tries
)
# Update state
diff --git a/mc_openapi/doml_mc/domlr_parser/parser.py b/mc_openapi/doml_mc/domlr_parser/parser.py
index fd4627790aaf73a535ea031072df328eaf054f6c..e193b24f6f3e3fe811c7c8648571fd9794428066 100644
--- a/mc_openapi/doml_mc/domlr_parser/parser.py
+++ b/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)
-
- # TODO: Replace before production
- print(msg)
-
- exit()
- # print()
- # print()
- # raise RequirementBadSyntaxException(e.line, e.column, msg)
+ raise RequirementBadSyntaxException(e.line, e.column, msg)
+
+
class DOMLRTransformer(Transformer):
# These callbacks will be called when a rule with the same name
diff --git a/mc_openapi/doml_mc/mc.py b/mc_openapi/doml_mc/mc.py
index a39a1ce57f231499925476160d583f9dd9ebd6af..f50936a58f8c5a4c17b5c85bec98d391a84ab2e6 100644
--- a/mc_openapi/doml_mc/mc.py
+++ b/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
diff --git a/requirements.txt b/requirements.txt
index ba2f5560b528dd052218d4e355393938ca022ece..b5475e5c8b9a4ef6d17a7ee2173db6e95a7ffa72 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,13 +1,19 @@
+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
diff --git a/tests/domlr/example_single_req.domlr b/tests/domlr/example_single_req.domlr
index 818548b68d1f57a134232358ccfbb991253a7524..759ace0a27ecd81605faa56eb21372eb16a9115e 100644
--- a/tests/domlr/example_single_req.domlr
+++ b/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."
diff --git a/tests/domlr/example_vm_has_sizedesc_cpu_count.domlr b/tests/domlr/example_vm_has_sizedesc_cpu_count.domlr
new file mode 100644
index 0000000000000000000000000000000000000000..c48e812e1f15ed1a38e473fb56baf6e970b38fab
--- /dev/null
+++ b/tests/domlr/example_vm_has_sizedesc_cpu_count.domlr
@@ -0,0 +1,9 @@
++ "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