diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py
index 3d4bf9315506f0bdf811effcb280862e419da1a3..086e2c43dc06b3e5ab49315b2debc52c8d82b3d7 100644
--- a/mc_openapi/__main__.py
+++ b/mc_openapi/__main__.py
@@ -102,15 +102,15 @@ else:
print(tabulate(csp_v, headers='firstrow', tablefmt='fancy_grid'))
else:
- result, msg = verify_model(dmc, domlr_src, args.threads, args.consistency, args.skip_builtin)
+ res = verify_model(dmc, domlr_src, args.threads, args.consistency, args.skip_builtin)
print("[RESULT]")
- if result == MCResult.sat:
- print("sat")
+ if res['result'] == MCResult.sat:
+ print(res['description'])
else:
- print(result.name)
+ print(res['result'])
print("[ERRORS]")
- print("\033[91m{}\033[00m".format(msg))
+ print("\033[91m{}\033[00m".format(res['description']))
else: # Synthesis
diff --git a/mc_openapi/doml_mc/html_output.py b/mc_openapi/doml_mc/html_output.py
deleted file mode 100644
index 09d215cd474ad9d04c1594d7243f5fbd1314a7c9..0000000000000000000000000000000000000000
--- a/mc_openapi/doml_mc/html_output.py
+++ /dev/null
@@ -1,16 +0,0 @@
-def html_template(
- title: str,
- content: str
-):
- return f"""<!doctype html>
-<html lang="en">
-<head>
- <meta charset="utf-8">
- <meta name="viewport" content="width=device-width, initial-scale=1">
- <title>{title}</title>
-</head>
-<body>
-{content}
-</body>
-</html>
-"""
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/main.py b/mc_openapi/doml_mc/main.py
index ac542d106cde4ed108defe1fa555027c2a15558f..dce6d80ec31812870fd6c2fa72ac05cbeed1238c 100644
--- a/mc_openapi/doml_mc/main.py
+++ b/mc_openapi/doml_mc/main.py
@@ -90,9 +90,11 @@ def verify_model(
disable_multithreading=(threads == 1)
)
- res, msg = results.summarize()
+ res = results.summarize()
- return res, msg
+ logging.info(res)
+
+ return res
def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int):
logging.warn("Synthesis is experimental and might not be up-to-date with the latest DOML.")
@@ -139,7 +141,6 @@ def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int):
reqs = user_req_store
- # TODO: Filter requirements according to flags
reqs += builtin_requirements
state = DOMLS.solve(
diff --git a/mc_openapi/doml_mc/mc_result.py b/mc_openapi/doml_mc/mc_result.py
index eb9e5bb7ac04d0fc58bd32365e66c42d6ac36eee..14bcd80f880df62a5d372b4643989f4d91a33009 100644
--- a/mc_openapi/doml_mc/mc_result.py
+++ b/mc_openapi/doml_mc/mc_result.py
@@ -37,7 +37,7 @@ class MCResults:
def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str]]):
self.results = results
- def summarize(self) -> tuple[MCResult, str]:
+ def summarize(self) -> dict[str, any]:
some_unsat = any(res == MCResult.unsat for res, _, _ in self.results)
some_dontknow = any(
res == MCResult.dontknow for res, _, _ in self.results)
@@ -61,17 +61,20 @@ class MCResults:
err_msg += '[Built-in]\n' + builtin_err_msg
if user_err_msgs:
err_msg += '\n[User]\n' + user_err_msg
-
if some_dontknow:
err_msg += '\n' + MCResults.DONTKNOW_MSG
- logging.info(err_msg)
- return MCResult.unsat, err_msg
+
+ return {
+ 'result': MCResult.unsat,
+ 'builtin': builtin_err_msgs,
+ 'user': user_err_msgs,
+ 'dontknow': some_dontknow,
+ 'description': err_msg
+ }
elif some_dontknow:
- logging.info(MCResults.DONTKNOW_MSG)
- return MCResult.dontknow, MCResults.DONTKNOW_MSG
+ return {'result': MCResult.dontknow, 'description': MCResults.DONTKNOW_MSG }
else:
- logging.info(MCResults.SATISFIED_MSG)
- return MCResult.sat, MCResults.SATISFIED_MSG
+ return {'result': MCResult.sat, 'description': MCResults.SATISFIED_MSG }
def add_results(self, results: "MCResults"):
self.results.extend(results.results)
diff --git a/mc_openapi/handlers.py b/mc_openapi/handlers.py
index 5308e80b2eaf2221b51d226647985448918d31af..6776797933dc6cbe661df1d1891791772aa22123 100644
--- a/mc_openapi/handlers.py
+++ b/mc_openapi/handlers.py
@@ -3,7 +3,6 @@ import logging
import os
from flask import render_template
-from mc_openapi.doml_mc.html_output import html_template
from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion
from mc_openapi.doml_mc import verify_model, init_model, verify_csp_compatibility
@@ -38,22 +37,15 @@ def mc(body, version, isHtml = False):
dmc = init_model(doml_xmi, doml_version)
- res, msg = verify_model(dmc)
-
+ res = verify_model(dmc)
+
+ res['doml_version'] = dmc.doml_version.value
+ res['result'] = res['result'].name
+
if isHtml:
- return html_template("DOML Model Checker - Results", "HELLO WORLD!")
+ return render_template('mc.html.jinja', **res).replace('\n', '')
else:
- if res == MCResult.sat:
- return {
- "result": "sat",
- "doml_version": dmc.doml_version.value
- }
- else:
- return {
- "result": res.name,
- "doml_version": dmc.doml_version.value,
- "description": f'[Using DOML {dmc.doml_version.value}]\n{msg}'
- }
+ return res
except Exception as e:
return make_error("The supplied DOMLX model is malformed or its DOML version is unsupported.", debug_msg=str(e)), 400
@@ -72,7 +64,6 @@ def csp(body, version=None):
dmc = init_model(doml_xmi, doml_version)
- # TODO: Do something with the results
return verify_csp_compatibility(dmc)
diff --git a/mc_openapi/templates/home.html b/mc_openapi/templates/home.html
index c71017d9ae33da28f92e61be9f978b0d2ab538d5..2a0e2acf030afcc804aea640eb53647fd65c4062 100644
--- a/mc_openapi/templates/home.html
+++ b/mc_openapi/templates/home.html
@@ -6,16 +6,25 @@
</head>
<body>
<h1>DOML Model Checker - Dashboard</h1>
- <input type="file" id="domlx" name="domlx" accept="text/xml,.domlx" />
+
+ <label for="domlx-csp">CSP Compatibility Check</label>
+ <input type="file" id="domlx-csp" name="domlx-csp" accept="text/xml,.domlx" />
+ <br/>
+ <br/>
+ <label for="domlx-mc">Model Check</label>
+ <input type="file" id="domlx-mc" name="domlx-mc" accept="text/xml,.domlx" />
<script>
- const input = document.querySelector("#domlx")
- input.addEventListener('change', readFile, false)
+ const input_csp = document.querySelector("#domlx-csp")
+ input_csp.addEventListener('change', readFileCSP, false)
+
+ const input_mc = document.querySelector("#domlx-mc")
+ input_mc.addEventListener('change', readFileMC, false)
- async function readFile(event) {
+ async function readFile(event, url) {
const file = event.target.files[0]
if (file) {
- const res = await fetch('/csp_html', {
+ const res = await fetch(url, {
method: 'POST',
headers: {
"Content-Type": "application/xml",
@@ -39,6 +48,13 @@
}
}
+ async function readFileCSP(event) {
+ readFile(event, '/csp_html')
+ }
+
+ async function readFileMC(event) {
+ readFile(event, '/modelcheck_html')
+ }
</script>
</body>
</html>
\ No newline at end of file
diff --git a/mc_openapi/templates/mc.html.jinja b/mc_openapi/templates/mc.html.jinja
new file mode 100644
index 0000000000000000000000000000000000000000..37d760b987268320e31f516ceabfc56ad2003e64
--- /dev/null
+++ b/mc_openapi/templates/mc.html.jinja
@@ -0,0 +1,53 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+ <title>DOML Model Checker Report</title>
+ <meta charset="utf8">
+ <style type="text/css">
+ {% include "style.css" %}
+ </style>
+</head>
+<body>
+ <h1>DOML Model Checker Report</h1>
+ <h2>Result:
+ {% if result == "sat" %}
+ <span class="sat">Satisfied</span>
+ {% else %}
+ <span class="unsat">Unsatisfied</span>
+ {% endif %}
+ </h2>
+ <p>DOML Version: {{doml_version}}</p>
+ {% if result != "sat" %}
+ {% if builtin %}
+
+ <h3>Built-in Requirements</h3>
+ <ul class="req-errs">
+ {% for req in builtin %}
+ <li class="req-err">{{req}}</li>
+ {% endfor %}
+ </ul>
+ {% endif %}
+ {% if user %}
+ <h3>User Requirements</h3>
+ <ul class="req-errs">
+ {% for req in user %}
+ <li class="req-err">
+ <h4>{{req[0]}}</h4>
+ <p>{{req[1]}}</p>
+ <ul class="notes">
+ {% for note in req[2] %}
+ <li>{{note}}</li>
+ {% endfor %}
+ </ul>
+ </li>
+ {% endfor %}
+ </ul>
+ {% endif %}
+ {% if dontknow %}
+ <p class="dontknow">There's been a timeout, so certain requirements couldn't be verified.</p>
+ </ul>
+ {% 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 9336cc2e4ebf42fe28f07e82dafa1ea864973111..dafd919a81ad9fd07cd110e561c0be93e27a312f 100644
--- a/mc_openapi/templates/style.css
+++ b/mc_openapi/templates/style.css
@@ -33,6 +33,26 @@ ul {
list-style: none;
}
+.req-errs {
+ display: block;
+}
+
+.req-err {
+ background-color: rgba(255, 0, 0, 0.2);
+ margin-bottom: 1em;
+ padding: 1em;
+ border-radius: 4px;
+}
+
+h4 {
+ margin: none;
+}
+
+.notes {
+ list-style: circle;
+ padding-left: 1.5em;
+}
+
li {
word-wrap: anywhere;
margin-bottom: 1em;
@@ -41,4 +61,15 @@ li {
li:last-child {
margin-bottom: 0;
}
-
\ No newline at end of file
+
+.unsat {
+ color: red;
+}
+
+.sat {
+ color: green;
+}
+
+.dontknow {
+ color: orange;
+}
\ No newline at end of file
diff --git a/tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_SoftwareComponents_deployed.doml b/tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_software_components_deployed.doml
similarity index 100%
rename from tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_SoftwareComponents_deployed.doml
rename to tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_software_components_deployed.doml
diff --git a/tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_SoftwareComponents_deployed.domlx b/tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_software_components_deployed.domlx
similarity index 100%
rename from tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_SoftwareComponents_deployed.domlx
rename to tests/doml/v2.0/nginx-openstack_v2.0_wrong_all_software_components_deployed.domlx
diff --git a/tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_iface.doml b/tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_has_iface.doml
similarity index 100%
rename from tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_iface.doml
rename to tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_has_iface.doml
diff --git a/tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_iface.domlx b/tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_has_iface.domlx
similarity index 100%
rename from tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_iface.domlx
rename to tests/doml/v2.0/nginx-openstack_v2.0_wrong_vm_has_iface.domlx
diff --git a/tests/doml/v2.2/nginx_func_req2_unsat.domlx b/tests/doml/v2.2/nginx_func_req2_unsat.domlx
index ab00f04895723cb0d57cd329588537d0c45a97ac..b05aa09b6d9ade8bc2a8a7c3a240c2296b6d76e4 100644
--- a/tests/doml/v2.2/nginx_func_req2_unsat.domlx
+++ b/tests/doml/v2.2/nginx_func_req2_unsat.domlx
@@ -55,5 +55,5 @@
<configurations name="conf">
<deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/>
</configurations>
- <functionalRequirements name="req_ext" description="```

 + "VM must have iface and iface is connected to network"
 	forall vm (
 		vm is class abstract.VirtualMachine
 	implies
 (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 )
 )
 error: "TEST ERROR"
 
 ```"/>
+ <functionalRequirements name="req_ext" description="```

 + "VM must have iface and iface is connected to network"
 	forall vm (
 		vm is class abstract.VirtualMachine
 	implies
 (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 )
 )
 error: "TEST ERROR {vm}"
 
 ```"/>
</commons:DOMLModel>