Skip to content
Snippets Groups Projects
Commit 5792bb81 authored by Andrea Franchini's avatar Andrea Franchini
Browse files

add MC html output

parent 24c0199b
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 134 additions and 55 deletions
mc_openapi/__main__.py
+ 5
− 5
View file @ 5792bb81
...@@ -102,15 +102,15 @@ else: ...@@ -102,15 +102,15 @@ else:
print(tabulate(csp_v, headers='firstrow', tablefmt='fancy_grid')) print(tabulate(csp_v, headers='firstrow', tablefmt='fancy_grid'))
else: 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]") print("[RESULT]")
if result == MCResult.sat: if res['result'] == MCResult.sat:
print("sat") print(res['description'])
else: else:
print(result.name) print(res['result'])
print("[ERRORS]") print("[ERRORS]")
print("\033[91m{}\033[00m".format(msg)) print("\033[91m{}\033[00m".format(res['description']))
else: # Synthesis else: # Synthesis
......
mc_openapi/doml_mc/html_output.py deleted 100644 → 0
+ 0
− 16
View file @ 24c0199b
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
mc_openapi/doml_mc/main.py
+ 4
− 3
View file @ 5792bb81
...@@ -90,9 +90,11 @@ def verify_model( ...@@ -90,9 +90,11 @@ def verify_model(
disable_multithreading=(threads == 1) 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): 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.") 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): ...@@ -139,7 +141,6 @@ def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int):
reqs = user_req_store reqs = user_req_store
# TODO: Filter requirements according to flags
reqs += builtin_requirements reqs += builtin_requirements
state = DOMLS.solve( state = DOMLS.solve(
......
mc_openapi/doml_mc/mc_result.py
+ 11
− 8
View file @ 5792bb81
...@@ -37,7 +37,7 @@ class MCResults: ...@@ -37,7 +37,7 @@ class MCResults:
def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str]]): def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str]]):
self.results = results 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_unsat = any(res == MCResult.unsat for res, _, _ in self.results)
some_dontknow = any( some_dontknow = any(
res == MCResult.dontknow for res, _, _ in self.results) res == MCResult.dontknow for res, _, _ in self.results)
...@@ -61,17 +61,20 @@ class MCResults: ...@@ -61,17 +61,20 @@ class MCResults:
err_msg += '[Built-in]\n' + builtin_err_msg err_msg += '[Built-in]\n' + builtin_err_msg
if user_err_msgs: if user_err_msgs:
err_msg += '\n[User]\n' + user_err_msg err_msg += '\n[User]\n' + user_err_msg
if some_dontknow: if some_dontknow:
err_msg += '\n' + MCResults.DONTKNOW_MSG 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: elif some_dontknow:
logging.info(MCResults.DONTKNOW_MSG) return {'result': MCResult.dontknow, 'description': MCResults.DONTKNOW_MSG }
return MCResult.dontknow, MCResults.DONTKNOW_MSG
else: else:
logging.info(MCResults.SATISFIED_MSG) return {'result': MCResult.sat, 'description': MCResults.SATISFIED_MSG }
return MCResult.sat, MCResults.SATISFIED_MSG
def add_results(self, results: "MCResults"): def add_results(self, results: "MCResults"):
self.results.extend(results.results) self.results.extend(results.results)
mc_openapi/handlers.py
+ 7
− 16
View file @ 5792bb81
...@@ -3,7 +3,6 @@ import logging ...@@ -3,7 +3,6 @@ import logging
import os import os
from flask import render_template 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.intermediate_model.metamodel import DOMLVersion
from mc_openapi.doml_mc import verify_model, init_model, verify_csp_compatibility from mc_openapi.doml_mc import verify_model, init_model, verify_csp_compatibility
...@@ -38,22 +37,15 @@ def mc(body, version, isHtml = False): ...@@ -38,22 +37,15 @@ def mc(body, version, isHtml = False):
dmc = init_model(doml_xmi, doml_version) 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: if isHtml:
return html_template("DOML Model Checker - Results", "HELLO WORLD!") return render_template('mc.html.jinja', **res).replace('\n', '')
else: else:
if res == MCResult.sat: return res
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}'
}
except Exception as e: except Exception as e:
return make_error("The supplied DOMLX model is malformed or its DOML version is unsupported.", debug_msg=str(e)), 400 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): ...@@ -72,7 +64,6 @@ def csp(body, version=None):
dmc = init_model(doml_xmi, doml_version) dmc = init_model(doml_xmi, doml_version)
# TODO: Do something with the results
return verify_csp_compatibility(dmc) return verify_csp_compatibility(dmc)
......
mc_openapi/templates/home.html
+ 21
− 5
View file @ 5792bb81
...@@ -6,16 +6,25 @@ ...@@ -6,16 +6,25 @@
</head> </head>
<body> <body>
<h1>DOML Model Checker - Dashboard</h1> <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> <script>
const input = document.querySelector("#domlx") const input_csp = document.querySelector("#domlx-csp")
input.addEventListener('change', readFile, false) 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] const file = event.target.files[0]
if (file) { if (file) {
const res = await fetch('/csp_html', { const res = await fetch(url, {
method: 'POST', method: 'POST',
headers: { headers: {
"Content-Type": "application/xml", "Content-Type": "application/xml",
...@@ -39,6 +48,13 @@ ...@@ -39,6 +48,13 @@
} }
} }
async function readFileCSP(event) {
readFile(event, '/csp_html')
}
async function readFileMC(event) {
readFile(event, '/modelcheck_html')
}
</script> </script>
</body> </body>
</html> </html>
\ No newline at end of file
mc_openapi/templates/mc.html.jinja 0 → 100644
+ 53
− 0
View file @ 5792bb81
<!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
mc_openapi/templates/style.css
+ 32
− 1
View file @ 5792bb81
...@@ -33,6 +33,26 @@ ul { ...@@ -33,6 +33,26 @@ ul {
list-style: none; 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 { li {
word-wrap: anywhere; word-wrap: anywhere;
margin-bottom: 1em; margin-bottom: 1em;
...@@ -41,4 +61,15 @@ li { ...@@ -41,4 +61,15 @@ li {
li:last-child { li:last-child {
margin-bottom: 0; margin-bottom: 0;
} }
\ No newline at end of file .unsat {
color: red;
}
.sat {
color: green;
}
.dontknow {
color: orange;
}
\ No newline at end of file
tests/doml/v2.2/nginx_func_req2_unsat.domlx
+ 1
− 1
View file @ 5792bb81
...@@ -55,5 +55,5 @@ ...@@ -55,5 +55,5 @@
<configurations name="conf"> <configurations name="conf">
<deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/> <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/>
</configurations> </configurations>
<functionalRequirements name="req_ext" description="```&#xA;&#xA; + &quot;VM must have iface and iface is connected to network&quot;&#xA; &#x9;forall vm (&#xA; &#x9;&#x9;vm is class abstract.VirtualMachine&#xA; &#x9;implies&#xA; (&#xA; &#x9;vm has abstract.ComputingNode.ifaces iface&#xA; &#x9;and&#xA; &#x9;iface has abstract.NetworkInterface.belongsTo net&#xA; )&#xA; )&#xA; error: &quot;TEST ERROR&quot;&#xA; &#xA; ```"/> <functionalRequirements name="req_ext" description="```&#xA;&#xA; + &quot;VM must have iface and iface is connected to network&quot;&#xA; &#x9;forall vm (&#xA; &#x9;&#x9;vm is class abstract.VirtualMachine&#xA; &#x9;implies&#xA; (&#xA; &#x9;vm has abstract.ComputingNode.ifaces iface&#xA; &#x9;and&#xA; &#x9;iface has abstract.NetworkInterface.belongsTo net&#xA; )&#xA; )&#xA; error: &quot;TEST ERROR {vm}&quot;&#xA; &#xA; ```"/>
</commons:DOMLModel> </commons:DOMLModel>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment