Add CSP step after MC (if flag)

mc_openapi/__init__.py

-__version__ = '2.5.1'
+__version__ = '2.5.2'

mc_openapi/__main__.py

@@ -32,6 +32,17 @@ parser.add_argument("-m", "--max-tries", dest="tries", type=int, default=8, help
 
 args = parser.parse_args()
 
+def print_csp_results(results):
+    for csp_k, csp_v in results.items():
+                # Format items in minreq
+        if csp_k == 'minreq':
+            for row in csp_v:
+                for index, col in enumerate(row):
+                    if index > 0 and isinstance(col, list):
+                        row[index] = "\n".join(col)
+
+        print(tabulate(csp_v, headers='firstrow', tablefmt='fancy_grid'))
+
 if not args.doml and not args.synth:
     dictConfig({
         'version': 1,
@@ -92,15 +103,7 @@ else:
         # Check CSP Compatibility
         if args.csp:
             csp = verify_csp_compatibility(dmc)
-            for csp_k, csp_v in csp.items():
-                # Format items in minreq
-                if csp_k == 'minreq':
-                    for row in csp_v:
-                        for index, col in enumerate(row):
-                            if index > 0 and isinstance(col, list):
-                                row[index] = "\n".join(col)
-
-                print(tabulate(csp_v, headers='firstrow', tablefmt='fancy_grid'))
+            print_csp_results(csp)
         else:
             res = verify_model(dmc, domlr_src, args.threads, args.consistency, args.skip_builtin)
 
@@ -111,6 +114,12 @@ else:
                 print(res['result'])
                 print("[ERRORS]")
                 print("\033[91m{}\033[00m".format(res['description']))
+            
+            csp_res = res.get('csp')
+            if csp_res:
+                print("[CSP COMPATIBILITY RESULTS]")
+                print_csp_results(csp_res)
+
 
 
     else: # Synthesis

mc_openapi/doml_mc/domlr_parser/transformer.py

@@ -32,7 +32,9 @@ class DOMLRTransformer(Transformer):
     # start
     def start(self, args) -> tuple[list[Requirement], dict[str, str]]:
         if not isinstance(args[0], dict): # there aren't flags
-            args = [{}, args[0]]
+            return args[0], {}
+        elif len(args) == 1 and isinstance(args[0], dict): # There are just the flags
+            return [], args[0]
         return args[1], args[0]
     
     def flags(self, args) -> dict:

mc_openapi/doml_mc/main.py

@@ -78,10 +78,6 @@ def verify_model(
     # Log all requirements to check
     logging.debug("Checking following requirements: " + ", ".join([k.assert_name for k in req_store.get_all_requirements()]))
 
-    # Check CSP
-    if flags.get('_csp', False):
-        logging.warning("The CSP compatibility check is not yet implemented via DOMLR")
-
     # Check satisfiability
     results = dmc.check_requirements(
         req_store,
@@ -96,6 +92,10 @@ def verify_model(
 
     logging.info(res)
 
+    # Check CSP
+    if flags.get('_csp', False):
+        res['csp'] = verify_csp_compatibility(dmc)
+
     return res
 
 def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int):

mc_openapi/handlers.py

@@ -43,6 +43,7 @@ def mc(body, version, isHtml = False):
         res['result'] = res['result'].name
         
         if isHtml:
+            res |= res.get('csp', {})
             return render_template('mc.html.jinja', **res).replace('\n', '')
         else:
             return res

mc_openapi/templates/mc.html.jinja

@@ -48,6 +48,88 @@
         </ul>
         {% endif %}
     {% endif %}
+    
+    {% if csp %}
+        <h1>CSP Compatibility Report</h1>
+        {% if keypairs %}
+        <h2>Keypairs</h2>
+            <table>
+            {% for row in keypairs %}
+            {% set outer_loop = loop %}
+                <tr>
+                {% for column in row %}
+                {% if outer_loop.first or loop.first %}
+                    <th>{{ column }}</th>
+                {% else %}
+                    <td>{{ column }}</td>
+                {% endif %}
+                {% endfor %}
+                </tr>
+            {% endfor %}
+            </table>
+        {% endif %}
+
+        {% if os %}
+        <h2>OS</h2>
+            <table>
+            {% for row in os %}
+            {% set outer_loop = loop %}
+                <tr>
+                {% for column in row %}
+                {% if outer_loop.first or loop.first %}
+                    <th>{{ column }}</th>
+                {% else %}
+                    <td>{{ column }}</td>
+                {% endif %}
+                {% endfor %}
+                </tr>
+            {% endfor %}
+            </table>
+        {% endif %}
 
+        {% if arch %}
+            <h2>Architectures</h2>
+            <table>
+            {% for row in arch %}
+            {% set outer_loop = loop %}
+                <tr>
+                {% for column in row %}
+                {% if outer_loop.first or loop.first %}
+                    <th>{{ column }}</th>
+                {% else %}
+                    <td>{{ column }}</td>
+                {% endif %}
+                {% endfor %}
+                </tr>
+            {% endfor %}
+            </table>
+        {% endif %}
+
+        {% if minreq %}
+            <h2>Minimum Requirements</h2>
+            <table>
+            {% for row in minreq %}
+            {% set outer_loop = loop %}
+                <tr>
+                {% for column in row %}
+                {% if outer_loop.first or loop.first %}
+                    <th>{{ column }}</th>
+                {% else %}
+                <td>
+                    <ul>
+                        {% for item in column %}
+                        <li>
+                            {{ item }}
+                        </li>
+                        {% endfor %}
+                    </ul>
+                </td>
+                {% endif %}
+                {% endfor %}
+                </tr>
+            {% endfor %}
+            </table>
+        {% endif %}
+    {% endif %}
 </body>
 </html>
\ No newline at end of file

mc_openapi/templates/style.css

@@ -6,7 +6,7 @@
 /* spacing */
 
 table {
-    table-layout: fixed;
+    table-layout: auto;
     width: 100%;
     border-collapse: collapse;
     border: 1px solid black;
@@ -17,6 +17,7 @@ td {
     padding: 0.5em;
     border: 1px solid black;
     text-align: left;
+    min-width: max-content;
 }
 
 th {
@@ -31,6 +32,7 @@ ul {
     padding: 0;
     margin: 0;
     list-style: none;
+    max-width: 100vw;
 }
 
 .req-errs {