Add initial support to new synthesis package

README.md

+[![Documentation Status](https://readthedocs.org/projects/piacere-model-checker/badge/?version=latest)](https://piacere-model-checker.readthedocs.io/en/latest/?badge=latest)
+
 # PIACERE Model Checker
 _______________________
-## **You can read the [docs here](https://andreafranchini.com/piacere-model-checker/) for more details.**
+## **You can read the [docs here](https://piacere-model-checker.readthedocs.io/en/latest/) for more details.**
 _______________________
 
 The DOML Model Checker is a component of the [PIACERE](https://www.piacere-project.eu/) framework
@@ -66,6 +68,8 @@ by adding `-p 127.0.0.1:8080:80/tcp` to the `docker run` command.
 The documentation has been written in [Sphinx](https://www.sphinx-doc.org/)
 and covers both usage through the PIACERE IDE and the REST APIs.
 
+Read it at [readthedocs.io](https://piacere-model-checker.readthedocs.io/en/latest/)
+
 Build the documentation with:
 ```sh
 cd docs

mc_openapi/__main__.py

@@ -6,12 +6,9 @@ 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.imc import RequirementStore
+from mc_openapi.doml_mc.intermediate_model.metamodel import MetaModelDocs
 from mc_openapi.doml_mc.mc import ModelChecker
 from mc_openapi.doml_mc.mc_result import MCResult
-from mc_openapi.doml_mc.synthesis.synthesis import Synthesis
-from mc_openapi.doml_mc.synthesis.synthesis_common_reqs import synthesis_default_req_store
-from mc_openapi.doml_mc.synthesis.xmi_gen import generate_xmi
-from mc_openapi.doml_mc.xmi_parser.doml_model import get_pyecore_model, serialize_pyecore_model
 
 parser = argparse.ArgumentParser()
 
@@ -77,51 +74,7 @@ else:
             print(e)
             raise RuntimeError("Failed to parse the DOMLR.")
 
-    if args.synth:
-        
-        try:
-            synth = Synthesis(dmc.metamodel, dmc.intermediate_model, verbose=args.verbose)
-
-            synth_req_store = RequirementStore()
-
-            synth_req_store += synthesis_default_req_store
-            synth_req_store += user_req_store
-
-            printv(f"synth_reqs : {len(synth_req_store)}")
-
-            solved_ctx = synth.check(
-                ub_elems_n=0,
-                ub_vals_n=0,
-                max_tries=args.tries, # default = 10
-                reqs=synth_req_store.get_all_requirements(), 
-                user_req_strings=user_req_str_consts)
-            solved_model = solved_ctx.solver.model()
-
-            # Print new found relationships
-            ub_elems_and_assoc = synth.get_ub_elems_and_assoc(solved_ctx, solved_model)
-            printv("\n".join([synth.pretty_ub_elems_assoc(assoc) for assoc in ub_elems_and_assoc]))
-            printv("-" * 120)
-            ub_vals_and_attr = synth.get_ub_vals_and_attr(solved_ctx, solved_model)
-            printv("\n".join([synth.pretty_ub_vals_attr(attr) for attr in ub_vals_and_attr]))
-
-            # find thinned results
-            assoc_to_implement = synth.thin_ub_elems_and_assoc(solved_ctx, ub_elems_and_assoc)
-            attrs_to_implement = synth.thin_ub_vals_and_attr(solved_ctx, ub_vals_and_attr)
-
-            # Print results
-            printv("\nPlease implement the following:\n")
-            printv("\n".join([synth.pretty_ub_elems_assoc(assoc) for assoc in assoc_to_implement]))
-            printv("\n".join([synth.pretty_ub_vals_attr(attr) for attr in attrs_to_implement]))
-
-            # Implement results
-            eobj = get_pyecore_model(doml_xmi, doml_ver)
-            eobj = generate_xmi(eobj, assoc_to_implement, dmc.intermediate_model, doml_ver)
-            serialize_pyecore_model(eobj)
-            
-        except Exception as e:
-            print(e)
-
-    else:
+    if not args.synth:
         try:
             # Check satisfiability
             results = dmc.check_requirements(
@@ -141,3 +94,37 @@ else:
                 print("\033[91m{}\033[00m".format(msg))
         except RequirementException as e:
             print(e.message)
+
+    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]
+        im = {
+            k: { 
+                'id': v.id_,
+                'name': v.user_friendly_name,
+                'class': v.class_,
+                'assocs': v.associations,
+                'attrs': v.attributes
+            }
+            for k, v in  dmc.intermediate_model.items()
+        }
+
+        # TODO: Fetch (user_reqs, user_reqs_strings)
+
+        state = State()
+        # Parse MM and IM
+        state = init_data(state, doml=im, metamodel=mm)
+        # Solve
+        state = solve(state, requirements=[builtin_requirements], strings=[], max_tries=args.tries)
+        # Update state
+        state = save_results(state)
+        # Print output
+        state = check_synth_results(state)
\ No newline at end of file