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

migrate to fastapi, improve HTML output

parent a3b0ff42
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 467 additions and 255 deletions
mc_openapi/assets/templates/base.html 0 → 100644
+ 20
− 0
View file @ 821d597a
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>DOML Model Checker</title>
<link href="{{ url_for('static', path='/bulma.min.css') }}" rel="stylesheet">
</head>
<body>
<section class="section">
<div class="container">
{% block content %}
{% endblock %}
</div>
</section>
</body>
</html>
\ No newline at end of file
mc_openapi/assets/templates/csp.html 0 → 100644
+ 5
− 0
View file @ 821d597a
{% extends "base.html" %}
{% block content %}
{% include "csp_content.html" %}
{% endblock content %}
\ No newline at end of file
mc_openapi/templates/mc.html.jinja → mc_openapi/assets/templates/csp_content.html
+ 98
− 0
View file @ 821d597a
<!DOCTYPE html> <h1 class="title">CSP Compatibility Results</h1>
<html lang="en"> {# FIX IMPORTS FOR MC #}
<head> {% if csp %}
<title>DOML Model Checker Report</title> {% set keypairs = csp.keypairs %}
<meta charset="utf8"> {% set os = csp.os %}
<style type="text/css"> {% set arch = csp.arch %}
{% include "style.css" %} {% set minreq = csp.minreq %}
</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 %} {% endif %}
{% if csp %} <div class="box">
<h1>CSP Compatibility Report</h1>
{% if keypairs %} {% if keypairs %}
<h2>Keypairs</h2> <h2 class="title is-4">Keypairs</h2>
<table> <div class="table-container">
<table class="table is-bordered is-striped is-hoverable">
{% for row in keypairs %} {% for row in keypairs %}
{% set outer_loop = loop %} {% set outer_loop = loop %}
<tr> <tr>
...@@ -67,11 +25,13 @@ ...@@ -67,11 +25,13 @@
</tr> </tr>
{% endfor %} {% endfor %}
</table> </table>
</div>
{% endif %} {% endif %}
{% if os %} {% if os %}
<h2>OS</h2> <h2 class="title is-4">OS</h2>
<table> <div class="table-container">
<table class="table is-bordered is-striped is-hoverable">
{% for row in os %} {% for row in os %}
{% set outer_loop = loop %} {% set outer_loop = loop %}
<tr> <tr>
...@@ -85,11 +45,13 @@ ...@@ -85,11 +45,13 @@
</tr> </tr>
{% endfor %} {% endfor %}
</table> </table>
</div>
{% endif %} {% endif %}
{% if arch %} {% if arch %}
<h2>Architectures</h2> <h2 class="title is-4">Architectures</h2>
<table> <div class="table-container">
<table class="table is-bordered is-striped is-hoverable">
{% for row in arch %} {% for row in arch %}
{% set outer_loop = loop %} {% set outer_loop = loop %}
<tr> <tr>
...@@ -103,11 +65,13 @@ ...@@ -103,11 +65,13 @@
</tr> </tr>
{% endfor %} {% endfor %}
</table> </table>
</div>
{% endif %} {% endif %}
{% if minreq %} {% if minreq %}
<h2>Minimum Requirements</h2> <h2 class="title is-4">Minimum Requirements</h2>
<table> <div class="table-container">
<table class="table is-bordered is-striped is-hoverable">
{% for row in minreq %} {% for row in minreq %}
{% set outer_loop = loop %} {% set outer_loop = loop %}
<tr> <tr>
...@@ -129,7 +93,6 @@ ...@@ -129,7 +93,6 @@
</tr> </tr>
{% endfor %} {% endfor %}
</table> </table>
</div>
</div>
{% endif %} {% endif %}
\ No newline at end of file
{% endif %}
</body>
</html>
\ No newline at end of file
mc_openapi/assets/templates/home.html 0 → 100644
+ 92
− 0
View file @ 821d597a
{% extends "base.html" %}
{% block content %}
<div class="box">
<h1 class="title">DOML Model Checker</h1>
<p>Upload a DOMLX file (in PIACERE IDE, <i>Right click > PIACERE > Generate DOMLX</i>) to either validate it with
the
model checker or the CSP compatibility tool.</p>
<br>
<div class="columns">
<div class="column">
<h2 class="subtitle">Model Checker</h2>
<div class="file is-boxed">
<label class="file-label">
<input class="file-input" type="file" name="resume" id="domlx-mc">
<span class="file-cta">
<span class="file-label">
Choose a file to validate
</span>
</span>
</label>
</div>
</div>
<div class="column">
<h2 class="subtitle">CSP Compatibility</h2>
<div class="file is-boxed">
<label class="file-label">
<input class="file-input" type="file" name="resume" id="domlx-csp">
<span class="file-cta">
<span class="file-label">
Choose a file to validate
</span>
</span>
</label>
</div>
</div>
</div>
<progress id="loading" class="is-hidden progress is-small is-primary" max="100">Loading...</progress>
<div id="error" class="notification is-danger is-hidden">
There was an issue with the file you uploaded. Is it a DOMLX file?
<br>
DOML files are not supported!
</div>
</div>
<script>
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)
const loadingBar = document.querySelector("#loading")
const errorBox = document.querySelector("#error")
async function readFile(event, url) {
const file = event.target.files[0]
if (file) {
loadingBar.classList.remove("is-hidden")
const res = await fetch(url, {
method: 'POST',
headers: {
"Content-Type": "application/xml",
},
redirect: "follow",
body: await file.text()
})
if (res.status === 200) {
newHtml = await res.text()
// Fix escaped quotes for tags
// Unescape emojis
// See: https://stackoverflow.com/questions/51640509/
newHtml = newHtml.replace(/\\u[\dA-F]{4}/gi, function (match) {
return String.fromCharCode(parseInt(match.replace(/\\u/g, ''), 16));
})
// Remove trailing and heading "
document.write(newHtml)
} else {
loadingBar.classList.add("is-hidden")
errorBox.classList.remove("is-hidden")
}
}
}
async function readFileCSP(event) {
readFile(event, '/csp_html')
}
async function readFileMC(event) {
readFile(event, '/modelcheck_html')
}
</script>
{% endblock content %}
\ No newline at end of file
mc_openapi/assets/templates/mc.html 0 → 100644
+ 116
− 0
View file @ 821d597a
{% extends "base.html" %}
{% block content %}
<h1 class="title">DOML Model Checker Results</h1>
<div class="box">
<h2 class="title is-4">Result:
{% if result == "sat" %}
<span class="tag is-success is-medium">Satisfied</span>
{% else %}
<span class="tag is-danger is-medium">Unsatisfied</span>
{% endif %}
</h2>
<div class="control">
<div class="tags has-addons">
<span class="tag is-dark">DOML Version</span>
<span class="tag is-info">{{doml_version}}</span>
</div>
</div>
{% if result != "sat" %}
{% if all_reqs %}
<label class="checkbox my-4">
<input type="checkbox" id="show-sat-reqs">
Show satisfied requirements
</label>
<ul class="">
{% for req in all_reqs %}
{% if req.result == "unsat" %}
<li class="message is-danger">
<div class="message-header">
<p>
Unsatisfied
</p>
<p>
<span class="tag is-family-monospace is-danger is-light">
{{req.id}}
</span>
<span class="tag is-danger is-light">{{req.type}}</span>
</p>
</div>
<div class="message-body">
<h2 class="title is-6 my-2">Description</h2>
<p>{{req.description}}</p>
<h2 class="title is-6 my-2">Error message:</h2>
<p>{{req.message}}</p>
</div>
</li>
{% else %}
<li class="message is-success sat-req is-hidden">
<div class="message-header">
<p>
Satisfied
</p>
<p>
<span class="tag is-family-monospace is-success is-light">
{{req.id}}
</span>
<span class="tag is-success is-light">{{req.type}}</span>
</p>
</div>
<div class="message-body">
<h2 class="title is-6 my-2">Description</h2>
<p>{{req.description}}</p>
</div>
</li>
{% endif %}
{% endfor %}
</ul>
{% endif %}
{% if user %}
<h3 class="title is-5">User Requirements</h3>
<ul class="">
{% for req in user %}
<li class="">
<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 %}
<article class="message is-warning">
<div class="message-header">
<p>Timeout!</p>
</div>
<div class="message-body">
There's been a timeout during the validation, so some requirements couldn't be verified.<br>
This is not the expected behaviour unless you are using custom requirements or/and very large DOML
models.<br>
Please report the issue if possible!
</div>
</article>
{% endif %}
{% endif %}
<script>
const checkbox = document.querySelector("#show-sat-reqs")
const satReqs = document.querySelectorAll(".sat-req")
checkbox.addEventListener("click", () => {
satReqs.forEach(el => el.classList.toggle('is-hidden'))
})
</script>
</div>
{% if csp %}
{% include "csp_content.html" %}
{% endif %}
{% endblock content %}
\ No newline at end of file
mc_openapi/doml_mc/exceptions.py 0 → 100644
+ 23
− 0
View file @ 821d597a
from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion
class BadDOMLException(Exception):
def __init__(self, message: str, *args: object) -> None:
super().__init__(*args)
self.errors = message or "The submitted DOML contains some kind of error."
class UnsupportedDOMLVersionException(Exception):
def __init__(self, message: str, *args: object) -> None:
super().__init__(*args)
self.errors = message or "The DOML version is not supported."
class MissingInfrastructureLayerException(Exception):
def __init__(self, message: str, *args: object) -> None:
super().__init__(*args)
self.errors = message or "Abstract infrastructure layer is missing from DOML."
class NoActiveConcreteLayerException(Exception):
def __init__(self, message: str, *args: object) -> None:
super().__init__(*args)
self.errors = message or "No active concrete infrastructure layer has been specified in DOML."
mc_openapi/doml_mc/imc.py
+ 4
− 1
View file @ 821d597a
...@@ -165,10 +165,13 @@ class IntermediateModelChecker: ...@@ -165,10 +165,13 @@ class IntermediateModelChecker:
res = self.solver.check() res = self.solver.check()
req_type, req_err_desc_fn = req.error_description req_type, req_err_desc_fn = req.error_description
req_is_sat = MCResult.from_z3result(res, flipped=req.flipped) req_is_sat = MCResult.from_z3result(res, flipped=req.flipped)
req_id = req.assert_name
results.append(( results.append((
req_is_sat, req_is_sat,
req_type, req_type,
req_err_desc_fn(self.solver, self.smt_sorts, self.intermediate_model) if req_is_sat else "" req_err_desc_fn(self.solver, self.smt_sorts, self.intermediate_model) if req_is_sat else "",
req_id,
req.description
# if res == sat else "" # not needed since we're try/catching model() errors # if res == sat else "" # not needed since we're try/catching model() errors
# in each requirement now # in each requirement now
)) ))
......
mc_openapi/doml_mc/intermediate_model/metamodel.py
+ 1
− 1
View file @ 821d597a
...@@ -171,7 +171,7 @@ def parse_inverse_associations(doc: dict) -> list[tuple[str, str]]: ...@@ -171,7 +171,7 @@ def parse_inverse_associations(doc: dict) -> list[tuple[str, str]]:
def init_metamodels(): def init_metamodels():
global MetaModelDocs, MetaModels, InverseAssociations global MetaModelDocs, MetaModels, InverseAssociations
for ver in DOMLVersion: for ver in DOMLVersion:
source = ilres.files(assets).joinpath(f"doml_meta_{ver.value}.yaml") source = ilres.files(assets).joinpath(f"metamodels/doml_meta_{ver.value}.yaml")
mmdoc = yaml.load(source.read_text() , yaml.Loader) mmdoc = yaml.load(source.read_text() , yaml.Loader)
MetaModelDocs[ver] = mmdoc MetaModelDocs[ver] = mmdoc
......
mc_openapi/doml_mc/main.py
+ 2
− 1
View file @ 821d597a
...@@ -89,8 +89,9 @@ def verify_model( ...@@ -89,8 +89,9 @@ def verify_model(
res = results.summarize() res = results.summarize()
res['doml_version'] = dmc.doml_version.name res['doml_version'] = dmc.doml_version.name
res['result'] = res['result'].name
logging.info(res) # logging.info(res)
# Check CSP # Check CSP
if flags.get('_csp', False): if flags.get('_csp', False):
......
mc_openapi/doml_mc/mc_result.py
+ 21
− 13
View file @ 821d597a
...@@ -34,27 +34,23 @@ class MCResults: ...@@ -34,27 +34,23 @@ class MCResults:
DONTKNOW_MSG = "Timed out: unable to check some requirements." DONTKNOW_MSG = "Timed out: unable to check some requirements."
SATISFIED_MSG = "All requirements are satisfied." SATISFIED_MSG = "All requirements are satisfied."
def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str]]): def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str, str, str]]):
"""It receives a list of tuples (result, type, error message, id)"""
self.results = results self.results = results
def summarize(self) -> dict[str, any]: 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)
if some_unsat: if some_unsat:
builtin_err_msgs = [ builtin_err_msgs = [
msg for res, type, msg in self.results if res == MCResult.unsat and type == "BUILTIN"] (id, msg) for res, type, msg, id, _ in self.results if res == MCResult.unsat and type == "BUILTIN"]
user_err_msgs = [ user_err_msgs = [
msg for res, type, msg in self.results if res == MCResult.unsat and type == "USER"] (id, msg) for res, type, msg, id, _ in self.results if res == MCResult.unsat and type == "USER"]
# Print to text (instead of HTML) # Print to text (instead of HTML)
builtin_err_msg = "\n".join(builtin_err_msgs) builtin_err_msg = "\n".join([f"[{id}] {msg}" for id, msg in builtin_err_msgs])
user_err_msg = "" user_err_msg = "\n".join([f"[{id}] {msg}" for id, msg in user_err_msgs])
for req_desc, err, notes in user_err_msgs:
user_err_msg += req_desc + '\n'
user_err_msg += err + '\n'
user_err_msg += "\n\t".join(notes)
err_msg = "" err_msg = ""
if builtin_err_msgs: if builtin_err_msgs:
...@@ -64,12 +60,24 @@ class MCResults: ...@@ -64,12 +60,24 @@ class MCResults:
if some_dontknow: if some_dontknow:
err_msg += '\n' + MCResults.DONTKNOW_MSG err_msg += '\n' + MCResults.DONTKNOW_MSG
all_reqs = [
{
"id": id,
"type": type,
"message": msg,
"result": res.name,
"description": desc
}
for res, type, msg, id, desc in self.results
]
return { return {
'result': MCResult.unsat, 'result': MCResult.unsat,
'builtin': builtin_err_msgs, 'builtin': builtin_err_msgs,
'user': user_err_msgs, 'user': user_err_msgs,
'dontknow': some_dontknow, 'dontknow': some_dontknow,
'description': err_msg 'description': err_msg,
'all_reqs': all_reqs
} }
elif some_dontknow: elif some_dontknow:
return {'result': MCResult.dontknow, 'description': MCResults.DONTKNOW_MSG } return {'result': MCResult.dontknow, 'description': MCResults.DONTKNOW_MSG }
......
mc_openapi/doml_mc/xmi_parser/doml_model.py
+ 7
− 6
View file @ 821d597a
...@@ -9,6 +9,7 @@ from pyecore.ecore import EObject ...@@ -9,6 +9,7 @@ from pyecore.ecore import EObject
from pyecore.resources import ResourceSet from pyecore.resources import ResourceSet
from mc_openapi import assets from mc_openapi import assets
from mc_openapi.doml_mc.exceptions import BadDOMLException, MissingInfrastructureLayerException, NoActiveConcreteLayerException, UnsupportedDOMLVersionException
from ..intermediate_model.doml_element import ( from ..intermediate_model.doml_element import (
IntermediateModel, reciprocate_inverse_associations) IntermediateModel, reciprocate_inverse_associations)
...@@ -23,7 +24,7 @@ def init_doml_rsets(): # noqa: E302 ...@@ -23,7 +24,7 @@ def init_doml_rsets(): # noqa: E302
global doml_rsets global doml_rsets
for ver in DOMLVersion: for ver in DOMLVersion:
rset = ResourceSet() rset = ResourceSet()
source = ilres.files(assets).joinpath(f"doml_{ver.value}.ecore") source = ilres.files(assets).joinpath(f"metamodels/doml_{ver.value}.ecore")
resource = rset.get_resource(BytesURI( resource = rset.get_resource(BytesURI(
"doml", bytes=source.read_bytes() "doml", bytes=source.read_bytes()
)) ))
...@@ -76,7 +77,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T ...@@ -76,7 +77,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T
except: except:
MSG_ERR_INVALID_DOML_VERSION = f"DOML requires version \"{model_version}\", but could not parse it with that version. Is the version valid?" MSG_ERR_INVALID_DOML_VERSION = f"DOML requires version \"{model_version}\", but could not parse it with that version. Is the version valid?"
logging.error(MSG_ERR_INVALID_DOML_VERSION) logging.error(MSG_ERR_INVALID_DOML_VERSION)
raise RuntimeError(MSG_ERR_INVALID_DOML_VERSION) raise UnsupportedDOMLVersionException(MSG_ERR_INVALID_DOML_VERSION)
except: except:
pass pass
# DOML version is not specified, proceed as usual # DOML version is not specified, proceed as usual
...@@ -86,7 +87,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T ...@@ -86,7 +87,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T
if len(doml_versions) == 0: if len(doml_versions) == 0:
MSG_ERR_NO_DOML_VERSIONS = "No other compatible DOML versions found!" MSG_ERR_NO_DOML_VERSIONS = "No other compatible DOML versions found!"
logging.error(MSG_ERR_NO_DOML_VERSIONS) logging.error(MSG_ERR_NO_DOML_VERSIONS)
raise RuntimeError(MSG_ERR_NO_DOML_VERSIONS) raise UnsupportedDOMLVersionException(MSG_ERR_NO_DOML_VERSIONS)
else: else:
return get_model(raw_model, doml_version) return get_model(raw_model, doml_version)
...@@ -95,7 +96,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T ...@@ -95,7 +96,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T
try: try:
model = parse_xmi_model(raw_model, doml_version) model = parse_xmi_model(raw_model, doml_version)
except: except:
raise RuntimeError("Parsing of DOML failed. Perhaps you are using the wrong DOML version or IDE?") raise BadDOMLException("Parsing of DOML failed. Perhaps you are using the wrong DOML version or IDE?")
logging.info(f"Model '{model.name}' parsed as DOML {doml_version.value}") logging.info(f"Model '{model.name}' parsed as DOML {doml_version.value}")
...@@ -105,13 +106,13 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T ...@@ -105,13 +106,13 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T
if model.infrastructure: if model.infrastructure:
elp.parse_elayer(model.infrastructure) elp.parse_elayer(model.infrastructure)
else: else:
raise RuntimeError("Abstract infrastructure layer is missing from DOML.") raise MissingInfrastructureLayerException()
if model.activeConfiguration: if model.activeConfiguration:
elp.parse_elayer(model.activeConfiguration) elp.parse_elayer(model.activeConfiguration)
if model.activeInfrastructure: if model.activeInfrastructure:
im = elp.parse_elayer(model.activeInfrastructure) im = elp.parse_elayer(model.activeInfrastructure)
else: else:
raise RuntimeError("No active concrete infrastructure layer has been specified in DOML.") raise NoActiveConcreteLayerException()
reciprocate_inverse_associations(im, InverseAssociations[doml_version]) reciprocate_inverse_associations(im, InverseAssociations[doml_version])
......
mc_openapi/fastapi.py 0 → 100644
+ 76
− 0
View file @ 821d597a
import logging
import os
import traceback
from fastapi import FastAPI, HTTPException, Request
from fastapi.responses import HTMLResponse
from fastapi.staticfiles import StaticFiles
from fastapi.templating import Jinja2Templates
from importlib.resources import files
import mc_openapi.assets as ASSETS
from mc_openapi.doml_mc.exceptions import *
from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion
from mc_openapi.doml_mc import init_model, verify_csp_compatibility, verify_model
from mc_openapi.doml_mc.mc import ModelChecker
assets = files(ASSETS)
static_path = assets / "static"
templates_path = assets / "templates"
app = FastAPI()
app.mount("/static", StaticFiles(directory=static_path), name="static")
templates = Jinja2Templates(directory=templates_path)
@app.get("/", response_class=HTMLResponse)
async def root(request: Request):
return templates.TemplateResponse("home.html", {"request": request})
def handleDOMLX(doml_xmi: bytes, callback) -> dict:
doml_version_str: str = None
doml_version: DOMLVersion = None
try:
# First try to infer DOML version from ENV, then query params
doml_version_str = os.environ.get("DOML_VERSION")
if doml_version_str:
doml_version = DOMLVersion.get(doml_version_str)
logging.info(f"Forcing DOML {doml_version.value}")
dmc = init_model(doml_xmi, doml_version)
return callback(dmc)
except (
BadDOMLException,
UnsupportedDOMLVersionException,
MissingInfrastructureLayerException,
NoActiveConcreteLayerException
) as e:
raise HTTPException(status_code=400, detail=e.errors)
except RuntimeError as e:
raise HTTPException(status_code=500, detail="An error has occurred.\n" + traceback.format_exc())
except Exception as e:
raise HTTPException(status_code=400, detail="An error has occurred.\n" + traceback.format_exc())
@app.post("/modelcheck")
async def mc(request: Request):
doml_xmi = await request.body()
return handleDOMLX(doml_xmi, verify_model)
@app.post("/csp")
async def csp(request: Request):
doml_xmi = await request.body()
return handleDOMLX(doml_xmi, verify_csp_compatibility)
@app.post("/modelcheck_html")
async def mc_html(request: Request):
doml_xmi = await request.body()
res = handleDOMLX(doml_xmi, verify_model)
return templates.TemplateResponse("mc.html", {"request": request, **res})
@app.post("/csp_html")
async def csp_html(request: Request):
doml_xmi = await request.body()
res = handleDOMLX(doml_xmi, verify_csp_compatibility)
return templates.TemplateResponse("csp.html", {"request": request, **res})
mc_openapi/templates/csp.html.jinja deleted 100644 → 0
+ 0
− 93
View file @ a3b0ff42
<!DOCTYPE html>
<html lang="en">
<head>
<title>CSP Compatibility Report</title>
<meta charset="utf8">
<style type="text/css">
{% include "style.css" %}
</style>
</head>
<body>
<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 %}
</body>
</html>
\ No newline at end of file
mc_openapi/templates/home.html deleted 100644 → 0
+ 0
− 60
View file @ a3b0ff42
<!DOCTYPE html>
<html lang="en">
<head>
<title>DOML Model Checker - Dashboard</title>
<meta charset="utf-8">
</head>
<body>
<h1>DOML Model Checker - Dashboard</h1>
<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_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, url) {
const file = event.target.files[0]
if (file) {
const res = await fetch(url, {
method: 'POST',
headers: {
"Content-Type": "application/xml",
},
redirect: "follow",
body: await file.text()
})
if (res.status === 200) {
newHtml = await res.text()
// Fix escaped quotes for tags
newHtml = newHtml.replaceAll("\\\"", "\"")
// Unescape emojis
// See: https://stackoverflow.com/questions/51640509/
newHtml = newHtml.replace(/\\u[\dA-F]{4}/gi, function(match) {
return String.fromCharCode(parseInt(match.replace(/\\u/g, ''), 16));
})
// Remove trailing and heading "
newHtml = newHtml.substr(1, newHtml.length - 3)
document.write(newHtml)
}
}
}
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
mc_openapi/templates/style.css deleted 100644 → 0
+ 0
− 77
View file @ a3b0ff42
* {
color: black;
font-family: system-ui, -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
}
/* spacing */
table {
table-layout: auto;
width: 100%;
border-collapse: collapse;
border: 1px solid black;
}
th,
td {
padding: 0.5em;
border: 1px solid black;
text-align: left;
min-width: max-content;
}
th {
background-color: #e7e7e7;
}
td {
vertical-align: top;
}
ul {
padding: 0;
margin: 0;
list-style: none;
max-width: 100vw;
}
.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;
}
li:last-child {
margin-bottom: 0;
}
.unsat {
color: red;
}
.sat {
color: green;
}
.dontknow {
color: orange;
}
\ No newline at end of file
requirements.txt
+ 1
− 2
View file @ 821d597a
tabulate tabulate
connexion fastapi
connexion[swagger-ui]
joblib joblib
z3-solver==4.11.* # Else it deadlocks the MC somehow z3-solver==4.11.* # Else it deadlocks the MC somehow
networkx networkx
......
tests/test_modelchecker.py
+ 1
− 1
View file @ 821d597a
...@@ -28,7 +28,7 @@ def test_domlx_models_by_version(subtests): ...@@ -28,7 +28,7 @@ def test_domlx_models_by_version(subtests):
if assert_result: if assert_result:
with subtests.test(msg=f"{doml_ver}/{domlx.name}", i=i): with subtests.test(msg=f"{doml_ver}/{domlx.name}", i=i):
res = run(domlx_file, assert_ver) res = run(domlx_file, assert_ver)
assert assert_result == res['result'].name assert assert_result == res['result']
assert assert_ver.name == res['doml_version'] assert assert_ver.name == res['doml_version']
OUTPUT = { OUTPUT = {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment