diff --git a/mc_openapi/__init__.py b/mc_openapi/__init__.py
index b8c5494802195e2851d08a7509f33ee3f154e2e6..3bfa1a62a6d9bafec40c6b60339bb5b3985924f2 100644
--- a/mc_openapi/__init__.py
+++ b/mc_openapi/__init__.py
@@ -1 +1 @@
-__version__ = '2.5.1'
+__version__ = '2.5.2'
diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py
index 086e2c43dc06b3e5ab49315b2debc52c8d82b3d7..1504eed4f4fabf8581bf8d71d8ea658c274a44e2 100644
--- a/mc_openapi/__main__.py
+++ b/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
diff --git a/mc_openapi/doml_mc/domlr_parser/transformer.py b/mc_openapi/doml_mc/domlr_parser/transformer.py
index 76aed5f2ae2309af385d00e13d632fbef13ec099..624d6003a3a675297e91e2b73bec601385b8f851 100644
--- a/mc_openapi/doml_mc/domlr_parser/transformer.py
+++ b/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:
diff --git a/mc_openapi/doml_mc/main.py b/mc_openapi/doml_mc/main.py
index 1a9caa2105f74084ccef858f17e9a2b7627c2041..407ba8477a753f939aca56c59d1d9ec1d9b3b122 100644
--- a/mc_openapi/doml_mc/main.py
+++ b/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):
diff --git a/mc_openapi/handlers.py b/mc_openapi/handlers.py
index 6776797933dc6cbe661df1d1891791772aa22123..bda0ad13bb3060d31933daaeb47951b8db5d6814 100644
--- a/mc_openapi/handlers.py
+++ b/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
diff --git a/mc_openapi/templates/mc.html.jinja b/mc_openapi/templates/mc.html.jinja
index 37d760b987268320e31f516ceabfc56ad2003e64..9c2ff24f686f2344e9db869fd969c588a4397454 100644
--- a/mc_openapi/templates/mc.html.jinja
+++ b/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
diff --git a/mc_openapi/templates/style.css b/mc_openapi/templates/style.css
index dafd919a81ad9fd07cd110e561c0be93e27a312f..16ef91e090c20ff7757433eea5bdc78e453d3866 100644
--- a/mc_openapi/templates/style.css
+++ b/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 {