Commit fa9e86df authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

add icon to randomize the formula + PSL>LTL diagnostics

parent 7af6c76a
Pipeline #3280 passed with stage
in 1 minute and 33 seconds
......@@ -8,6 +8,7 @@ import FormControlLabel from "@material-ui/core/FormControlLabel";
import FormLabel from "@material-ui/core/FormLabel";
import FormHelperText from "@material-ui/core/FormHelperText";
import IconButton from "@material-ui/core/IconButton";
import InputAdornment from "@material-ui/core/InputAdornment";
import List from "@material-ui/core/List";
import ListItem from "@material-ui/core/ListItem";
import ListItemText from "@material-ui/core/ListItemText";
......@@ -196,6 +197,14 @@ const styles = theme => ({
}
});
function DiceIcon(props) {
return (
<SvgIcon {...props}>
<path d="M5,3H19A2,2 0 0,1 21,5V19A2,2 0 0,1 19,21H5A2,2 0 0,1 3,19V5A2,2 0 0,1 5,3M7,5A2,2 0 0,0 5,7A2,2 0 0,0 7,9A2,2 0 0,0 9,7A2,2 0 0,0 7,5M17,15A2,2 0 0,0 15,17A2,2 0 0,0 17,19A2,2 0 0,0 19,17A2,2 0 0,0 17,15M17,5A2,2 0 0,0 15,7A2,2 0 0,0 17,9A2,2 0 0,0 19,7A2,2 0 0,0 17,5M12,10A2,2 0 0,0 10,12A2,2 0 0,0 12,14A2,2 0 0,0 14,12A2,2 0 0,0 12,10M7,15A2,2 0 0,0 5,17A2,2 0 0,0 7,19A2,2 0 0,0 9,17A2,2 0 0,0 7,15Z" />
</SvgIcon>
);
}
function NoteIcon(props) {
return (
<SvgIcon {...props}>
......@@ -309,6 +318,20 @@ class LtlInput extends React.Component {
if (e.key === "Enter") this.updateFormula();
};
randomizeFormula = () => {
let url = new URL(api_endpoint() + "random");
console.log(this.props.expert);
if (this.props.expert)
// turn on PSL generation
url.searchParams.append("p", 1);
fetch(url)
.then(handleErrors)
.then(fmt => {
this.setState({ tmpformula: fmt, formula: fmt });
this.props.setFormula(fmt);
});
};
render() {
return (
<div className={this.props.classes.ltlInput}>
......@@ -316,12 +339,28 @@ class LtlInput extends React.Component {
error={Boolean(this.props.formulaerr)}
className={this.props.className}
fullWidth
defaultValue={this.props.defaultValue}
value={this.state.tmpformula}
label={this.props.label}
autoFocus={this.props.autoFocus}
onChange={this.handleChange}
onKeyPress={this.handleKey}
onBlur={this.updateFormula}
InputProps={{
endAdornment: (
<Tooltip
disableFocusListener={true}
title="Overwrite input with a random formula."
placement="right"
enterDelay={750}
>
<InputAdornment position="end">
<IconButton onClick={this.randomizeFormula}>
<DiceIcon color="primary" />
</IconButton>
</InputAdornment>
</Tooltip>
)
}}
/>
<FormHelperText className={this.props.classes.helperText}>
{this.state.tmpformula !== this.state.formula && (
......@@ -686,6 +725,8 @@ class LtlRewrite extends React.Component {
this.setState({ result: <Typography>{res["formula"]}</Typography> });
else if ("svg" in res)
this.setState({ result: <SVGInline svg={res["svg"]} /> });
else if ("error" in res)
this.setState({ result: <Typography>{res["error"]}</Typography> });
else this.setState({ result: null });
})
.catch(error => {
......@@ -1448,6 +1489,7 @@ class LtlCompare extends React.Component {
classes={this.props.classes}
className={this.props.classes.textField2}
label="Second formula"
expert={this.props.expert}
defaultValue={this.props.formula2}
setFormula={this.props.handleChangeFormula2}
formulalbt={this.state.formula2lbt}
......@@ -1650,6 +1692,7 @@ class LtlApp extends React.Component {
: this.props.classes.textField
}
label={this.state.action === 2 ? "First formula" : "Input formula"}
expert={this.state.expert}
autoFocus
setFormula={this.handleChangeFormula}
formulalbt={this.state.formulalbt}
......@@ -1689,6 +1732,7 @@ class LtlApp extends React.Component {
formula2={this.state.formula2}
handleChangeFormula2={this.handleChangeFormula2}
handleAnyParseError={this.handleAnyParseError}
expert={this.props.expert}
/>
)}
{this.state.action === 3 && (
......
......@@ -8,6 +8,7 @@ from platform import python_version
import subprocess
import re
import os
from time import time
app = Flask(__name__)
CORS(app)
......@@ -16,6 +17,19 @@ os.environ['SPOT_DOTEXTRA'] = 'size="6,6" edge[arrowhead=vee, arrowsize=.7]'
import spot
from spot.aux import str_to_svg
from functools import wraps
def cachecontrol(max_age=3600):
def decorate_f(f):
@wraps(f)
def wrapped_f(*args, **kwargs):
response = f(*args, **kwargs)
if ((type(response) is Flask.response_class) and
(response.status_code == 200)):
response.cache_control.max_age = max_age
return response
return wrapped_f
return decorate_f
def parse_ltl(input, res, errkey='parse_error', synkey='prefix_syntax'):
env = spot.default_environment.instance()
......@@ -39,6 +53,7 @@ def parse_ltl(input, res, errkey='parse_error', synkey='prefix_syntax'):
# Return a Json list of triplets [[tool,version,url],...].
@app.route('/api/versions')
@cachecontrol()
def versions():
dot = subprocess.Popen(['dot', '-V'],
stdout=subprocess.PIPE,
......@@ -56,6 +71,21 @@ def versions():
("GraphViz", dot_version, "https://graphviz.gitlab.io/"),
])
@app.route('/api/random')
# no cache control for this one!
def random(method='GET'):
p = request.args.get('p', None)
gen = spot.randltl(3, tree_size=(5,25),
output=('psl' if p else 'ltl'),
seed=int(time()))
# Try 10 time to avoid true or false
for i in range(1, 10):
f = next(gen)
if not (f.is_tt() or f.is_ff()):
break;
return jsonify(str(f))
# Rewrite a formula.
#
# URL parameters:
......@@ -80,6 +110,7 @@ def versions():
# on success: { formula: "text" } or { svg: "text" }
# on syntax error: { parse_error: "text" }
@app.route('/api/rewrite/<path:ltlformula>')
@cachecontrol()
def rewrite(ltlformula, method='GET'):
res = {}
......@@ -128,6 +159,10 @@ def rewrite(ltlformula, method='GET'):
s = dotsrc.str().encode('utf-8')
return jsonify({'svg': str_to_svg(s)})
if not f.is_ltl_formula() and syntax in "li":
res['error'] = "The selected syntax only supports LTL formulas."
return jsonify(res)
s = None
if syntax == 'l':
s = spot.str_lbt_ltl(f)
......@@ -163,6 +198,7 @@ mp_class_to_english = {
# stutter_invariant: False (or True, or 'no X')
# }
@app.route('/api/study/<path:ltlformula>')
@cachecontrol()
def study(ltlformula, method='GET'):
result = {}
......@@ -276,6 +312,7 @@ def study(ltlformula, method='GET'):
# note: {'text'} (optional)
# }
@app.route('/api/translate/<path:ltlformula>')
@cachecontrol()
def translate(ltlformula, method='GET'):
res = {}
......@@ -514,6 +551,7 @@ def svg_compare(w1, w2, w3, w4):
return svg_compare_list[idx]
@app.route('/api/compare/<path:ltlformula>')
@cachecontrol()
def compare(ltlformula, method='GET'):
result = {}
......@@ -553,25 +591,7 @@ def compare(ltlformula, method='GET'):
return jsonify(result)
@app.after_request
def add_header(response):
if response.status_code == 200:
response.cache_control.max_age = 3600
return response
if __name__ == '__main__':
app.run(debug=True, use_reloader=True, use_debugger=False)
# import os
# import sys
#
# # 3600s = 1h
# sys.stdout.write("""Cache-Control: max-age=3600
# Content-Type: application/json
#
# """)
#
# from http.server import CGIHTTPRequestHandler, HTTPServer
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment