Franck Pommereau / tlw

Go to a project
Toggle navigation Toggle navigation pinning
Franck Pommereau
e65603ba 0 parents

initial import

Inline Side-by-side
Showing 5 changed files with 339 additions and 0 deletions
# The MIT License (MIT)
Copyright (C) 2023 <franck.pommereau@univ-evry.fr>
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
# The Temporal Logic Wizard
The TLW is a dynamic web page that allow to interactively build complex temporal logic formulas from a list of patterns.
For instance, instead of writing `EF(X & EF(Y))`, users may select the pattern presented as "_`Y` is reachable and is possibly preceded at some time by `X`_" and then fill what they expect to be `X` and `Y`.
Of course, patterns may be arbitrarily nested.
So far, only CTL is supported, other temporal logics may be added in the future.
The syntax for temporal logic formulas is that of [pytl](https://github.com/fpom/pytl) as used in the [ecco](https://github.com/fpom/pytl) toolkit.
## Installation
The TLW consists of three files:
* `wiz.css` the CSS style sheet
* `wiz.py` the PyScript to animate the wizard (the Python interpreter is loaded at runtime from [PyScript homepage](http://pyscript.net))
* `wiz.html` the HTML page to be displayed to end-users
These three files should be copied on some web server, `wiz.html` may be renamed to something else.
Renaming the other files will require to edit `wiz.html` in order to have them correctly loaded.
## Licence
The Temporal Logic Wizard is (C) 2023 Franck Pommereau <franck.pommereau@univ-evry.fr> and released under the terms of the MIT Licence (see `LICENCE.md`).
.wiz {
margin: 10px;
width: 100%;
}
.wiz-wizard {
display: block;
margin-bottom: 10px;
padding: 10px;
}
.wiz-output {
display: flex;
}
.wiz-output textarea {
flex-grow: 1;
margin-right: 5px;
}
.wiz-pattern {
flex-grow: 1;
display: block;
margin: 0px;
margin-bottom: 5px;
padding-left: 5px;
padding-right: 0px;
padding-bottom: 5px;
padding-top: 5px;
border-left: 4px solid lightgray;
}
.wiz-select {
display: flex;
}
.wiz-select label {
margin-right: 10px;
flex-grow: 0;
}
.wiz-select select {
flex-grow: 1;
}
.wiz-args {
display: flex;
flex-direction: column;
align-items: stretch;
}
.wiz-arg {
display: flex;
margin-top: 5px;
margin-bottom: 5px;
margin-left: 10px;
margin-right: 0px;
padding-left: 5px;
}
.wiz-arg-name {
flex-grow: 0;
margin-right: 10px;
}
.wiz-arg-value {
display: flex;
flex-grow: 1;
}
.wiz-arg-value label {
flex-grow: 0;
}
.wiz-arg-value input {
flex-grow: 1;
}
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1"/>
<title>The Temporal Logic Wizard</title>
<link rel="stylesheet" href="https://pyscript.net/latest/pyscript.css"/>
<link rel="stylesheet" href="./wiz.css"/>
<script defer src="https://pyscript.net/latest/pyscript.js"></script>
</head>
<body>
<py-script src="./wiz.py"></py-script>
<div id="wiz"></div>
<button type="button" py-click="WizUI()">New formula</button>
<py-script>WizUI()</py-script>
</body>
</html>
from pyodide.ffi import create_proxy
from js import document as DOC
from functools import partial
from typing import assert_never
def vars_pattern(X: str):
return " & ".join(X.split())
patterns = {
"vars": {
"desc": "variables in X are True",
"tpl": vars_pattern,
"args": [{"name" : "X",
"type": "text",
"desc": "space-separated list"}]
},
"form": {
"desc": "formula X holds",
"tpl": "{X}",
"args": [{"name": "X",
"type": "text",
"desc": "CTL formula"}]
},
"and": {
"desc": "X and Y hold",
"tpl": "({X}) & ({Y})",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"or": {
"desc": "X or Y hold",
"tpl": "({X}) | ({Y})",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"not": {
"desc": "X does not hold",
"tpl": "~({X})",
"args": [{"name": "X", "type": "pattern"}]
},
"reach-may": {
"desc": "X may be reached",
"tpl": "EF({X})",
"args": [{"name": "X", "type": "pattern"}]
},
"reach-must": {
"desc": "X must be reached",
"tpl": "AF({X})",
"args": [{"name": "X", "type": "pattern"}]
},
"inv-may-persist": {
"desc": "X may persist forever",
"tpl": "EG({X})",
"args": [{"name": "X", "type": "pattern"}]
},
"inv-must-persist": {
"desc": "X must persist forever",
"tpl": "AG({X})",
"args": [{"name": "X", "type": "pattern"}]
},
"inv-may-reach": {
"desc": "X may remain forever reachable",
"tpl": "EG(EF({X}))",
"args": [{"name": "X", "type": "pattern"}]
},
"inv-must-reach": {
"desc": "X must remain forever reachable",
"tpl": "AG(EF({X}))",
"args": [{"name": "X", "type": "pattern"}]
},
"inv-infinite-reach": {
"desc": "X is necessarily reached infinitely often",
"tpl": "AG(AF({X}))",
"args": [{"name": "X", "type": "pattern"}]
},
"reach-inv-may": {
"desc": "is is possible to reach a state from which X may persist forever",
"tpl": "EF(EG({X}))",
"args": [{"name": "X", "type": "pattern"}]
},
"reach-inv-must": {
"desc": "is is possible to reach a state from which X must persist forever",
"tpl": "EF(AG({X}))",
"args": [{"name": "X", "type": "pattern"}]
},
"then-may": {
"desc": "if X is reached, then it is possibly followed by Y",
"tpl": "AF(({X}) => EF({Y}))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"then-must": {
"desc": "if X is reached, then it is necessarily followed by Y",
"tpl": "AF(({X}) => EF({Y}))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"seq-may-sometimes": {
"desc": "Y is reachable and is possibly preceded at some time by X",
"tpl": "EF(({X}) & EF({Y}))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"seq-may-always": {
"desc": "Y is reachable and is possibly preceded all the time by X",
"tpl": "E(({X}) U ({Y}))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"seq-must-sometimes": {
"desc": "Y is reachable and is necessarily preceded at some time by X",
"tpl": "EF({X}) & (~E((~({X})) U ({Y})))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
},
"seq-must-always": {
"desc": "Y is reachable and is necessarily preceded all the time by X",
"tpl": "EF({X}) & AG((~({X})) => AG(~({Y})))",
"args": [{"name": "X", "type": "pattern"},
{"name": "Y", "type": "pattern"}]
}
}
class HTML:
def __call__(self, tag, *content, **attrs):
elt = DOC.createElement(tag)
for key, val in attrs.items():
elt.setAttribute(key, val)
for child in content:
if isinstance(child, str):
elt.innerHTML = elt.innerHTML + child
else:
elt.appendChild(child, append=True)
return elt
def __getattr__(self, tag):
return partial(self.__call__, tag)
H = HTML()
WIZ = DOC.querySelector(f"#wiz")
class WizUI:
def __init__(self):
div = H.div((form := H.div(CLASS="wiz-form")),
H.div((out := H.textarea(name="output", readonly=True)),
(button := H.button("Copy")),
CLASS="wiz-output"),
CLASS="wiz-wizard")
self.child = PatternUI(self, form)
self.output = out
WIZ.appendChild(div, append=True)
button.addEventListener("click", create_proxy(self.on_copy))
def update(self):
self.output.value = self.child.formula()
self.output.setSelectionRange(0, 0);
def on_copy(self, *_):
self.output.select();
self.output.setSelectionRange(0, 99999);
DOC.execCommand("copy");
class PatternUI:
def __init__(self, wiz, container):
self.wiz = wiz
pat = H.div(H.div(H.label("Pattern:", FOR="pattern"),
(select := H.select(*(H.option(f"{spec['desc']} [{name}]",
value=name)
for name, spec in patterns.items()),
name="pattern")),
CLASS="wiz-select"),
(args := H.div(CLASS="wiz-args")),
CLASS="wiz-pattern")
self.select, self.args = select, args
container.appendChild(pat)
self.select.addEventListener("change", create_proxy(self.on_select))
self.on_select()
def on_select(self, *args):
val = str(self.select.value)
self.mk(val)
if args:
self.wiz.update()
def mk(self, name):
self.children = {}
spec = self.pattern = patterns[name]
self.args.innerHTML = ""
for arg in spec["args"]:
if arg["type"] == "text":
elt = H.div((inp := H.input(TYPE="text", placeholder=arg["desc"])),
CLASS="wiz-arg-value")
self.children[arg["name"]] = inp
elt.addEventListener("input", create_proxy(self.on_update))
elif arg["type"] == "pattern":
elt = H.div(CLASS="wiz-arg-value")
self.children[arg["name"]] = PatternUI(self.wiz, elt)
else:
assert_never(arg)
div = H.div(H.div(H.label(f"{arg['name']}:"), CLASS="wiz-arg-name"),
elt,
CLASS="wiz-arg")
self.args.appendChild(div, append=True)
def on_update(self, *_):
self.wiz.update()
def formula(self):
tpl = self.pattern["tpl"]
args = {}
for key, val in self.children.items():
if isinstance(val, PatternUI):
args[key] = val.formula()
else:
args[key] = val.value
if isinstance(tpl, str):
return tpl.format(**args)
else:
return tpl(**args)