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

support multiple notes from the translation

parent 46625f77
...@@ -1010,7 +1010,7 @@ class LtlTranslate extends React.Component { ...@@ -1010,7 +1010,7 @@ class LtlTranslate extends React.Component {
{res["edges"] > 1 ? "s" : ""}. {res["edges"] > 1 ? "s" : ""}.
</Typography> </Typography>
)} )}
{"note" in res && <NoteText text={res["note"]} />} {"note" in res && res["note"].map((note) => <NoteText text={note} />)}
{"automaton_svg" in res && ( {"automaton_svg" in res && (
<SVGInline <SVGInline
className={this.props.classes.automaton_svg} className={this.props.classes.automaton_svg}
......
...@@ -70,6 +70,12 @@ def parse_ltl(input, res, errkey='parse_error', synkey='prefix_syntax'): ...@@ -70,6 +70,12 @@ def parse_ltl(input, res, errkey='parse_error', synkey='prefix_syntax'):
return None return None
return spot.formula(str(f)) return spot.formula(str(f))
def warn(res, msg):
if 'note' in res:
res['note'].append(msg)
else:
res['note'] = [msg]
# Return a Json list of triplets [[tool,version,url],...]. # Return a Json list of triplets [[tool,version,url],...].
@app.route('/api/versions') @app.route('/api/versions')
@cachecontrol() @cachecontrol()
...@@ -328,7 +334,7 @@ def study(ltlformula, method='GET'): ...@@ -328,7 +334,7 @@ def study(ltlformula, method='GET'):
# on syntax error: { parse_error: "text" } # on syntax error: { parse_error: "text" }
# on success: # on success:
# { automaton_svg: '<svg...' # { automaton_svg: '<svg...'
# note: {'text'} (optional) # note: ['text1','text2',...] (optional)
# } # }
@app.route('/api/translate/<path:ltlformula>') @app.route('/api/translate/<path:ltlformula>')
@cachecontrol() @cachecontrol()
...@@ -397,15 +403,15 @@ def translate(ltlformula, method='GET'): ...@@ -397,15 +403,15 @@ def translate(ltlformula, method='GET'):
aut = spot.translate(f, *args) aut = spot.translate(f, *args)
if arg_a == 'c' and not f.is_syntactic_persistence(): if arg_a == 'c' and not f.is_syntactic_persistence():
res['note'] = ("Co-Büchi automata can only represent persistence" warn(res, ("Co-Büchi automata can only represent persistence"
" properties. If your formula does not belong to this" " properties. If your formula does not belong to this"
" class, the automaton below will accept a superset of" " class, the automaton below will accept a superset of"
" the intended language.") " the intended language."))
if arg_a == 'm' and not f.is_syntactic_safety(): if arg_a == 'm' and not f.is_syntactic_safety():
res['note'] = ("Monitors can only represent safety properties. " warn(res, ("Monitors can only represent safety properties. "
"If your formula does not belong to this class, " "If your formula does not belong to this class, "
"the automaton below will accept a superset of " "the automaton below will accept a superset of "
"the intended language.") "the intended language."))
if arg_a == 'p': if arg_a == 'p':
accname = aut.acc().name() accname = aut.acc().name()
if not accname.startswith('parity'): if not accname.startswith('parity'):
...@@ -422,11 +428,11 @@ def translate(ltlformula, method='GET'): ...@@ -422,11 +428,11 @@ def translate(ltlformula, method='GET'):
msg += " and to 'parity {} {} 1'".format( msg += " and to 'parity {} {} 1'".format(
"min" if ipm else "max", "min" if ipm else "max",
"odd" if ipo else "even") "odd" if ipo else "even")
res['note'] = msg + '.' warn(res, msg + '.')
opt = "arf(Lato)C(#ffffaa)" opt = "arf(Lato)C(#ffffaa)"
opt += 'B' if arg_a in ('b', 'm', 'c') else 'b' opt += 'B' if arg_a in ('b', 'm', 'c') else 'b'
if arg_a == 'm': if arg_a == 'm' and aut.acc().is_t():
opt += 'A' opt += 'A'
match_arg_display_opts = { match_arg_display_opts = {
...@@ -446,10 +452,10 @@ def translate(ltlformula, method='GET'): ...@@ -446,10 +452,10 @@ def translate(ltlformula, method='GET'):
dodot = True dodot = True
if float(aut.num_edges())/aut.num_states() > 16: if float(aut.num_edges())/aut.num_states() > 16:
res['note'] = "Automaton not displayed because it has too many edges per state." warn(res, "Automaton not displayed because it has too many edges per state.")
dodot = False; dodot = False;
elif aut.num_states() > 30: elif aut.num_states() > 30:
res['note'] = "Only the first 30 states of the automaton are displayed." warn(res, "Only the first 30 states of the automaton are displayed.")
if dodot: if dodot:
dotsrc = spot.ostringstream() dotsrc = spot.ostringstream()
......
Supports Markdown
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