Commit 61824f9b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

state if a non SSI formula can be simplified to an SSI formula

parent ce984be8
Pipeline #9074 passed with stage
in 1 minute and 55 seconds
...@@ -1005,6 +1005,8 @@ class LtlStudy extends React.Component { ...@@ -1005,6 +1005,8 @@ class LtlStudy extends React.Component {
<Typography> <Typography>
This formula is <b>stutter-invariant</b> even if it might not look This formula is <b>stutter-invariant</b> even if it might not look
so syntactically. so syntactically.
{"stutter_invariant_eq" in res &&
(<><br/>Furthermore, it can be simplified to the following <i>syntactically sutter-invariant</i> formula:<br/><Ltl f={res["stutter_invariant_eq"]}/></>)}
</Typography> </Typography>
)} )}
{res["stutter_invariant"] === false && ( {res["stutter_invariant"] === false && (
......
...@@ -216,13 +216,19 @@ mp_class_to_english = { ...@@ -216,13 +216,19 @@ mp_class_to_english = {
# #
# on success: # on success:
# { mp_class: 'name', # { mp_class: 'name',
# pathological: True, (absent if not pathological) # pathological: true, (absent if not pathological)
# mp_hierarchy_svg: '<svg...' # mp_hierarchy_svg: '<svg...'
# acc_word: 'word', (an example of accepting word, or null) # acc_word: 'word', (an example of accepting word, or null)
# rej_word: 'word', (an example of rejecting word, or null) # rej_word: 'word', (an example of rejecting word, or null)
# stutter_invariant: False, (or True, or 'no X') # stutter_invariant: false, (or true, or 'no X')
# stutter_invariant_eq: formula, (* see below)
# safety_liveness: 'safety' (or 'liveness', or 'both', or 'none') # safety_liveness: 'safety' (or 'liveness', or 'both', or 'none')
# } # }
#
# stutter_invariant_eq is only given if stutter_invariant=true (not 'no X'),
# and simplifying the input ltlformula gives a syntactically stutter-invariant
# formula.
@app.route('/api/study/<path:ltlformula>') @app.route('/api/study/<path:ltlformula>')
@cachecontrol() @cachecontrol()
def study(ltlformula, method='GET'): def study(ltlformula, method='GET'):
...@@ -259,6 +265,11 @@ def study(ltlformula, method='GET'): ...@@ -259,6 +265,11 @@ def study(ltlformula, method='GET'):
ssi = f.is_syntactic_stutter_invariant() ssi = f.is_syntactic_stutter_invariant()
pos = spot.translate(f, 'med') pos = spot.translate(f, 'med')
# f was simplified by translate.
if (ssi is False and f.is_syntactic_stutter_invariant()):
result['stutter_invariant_eq'] = str(f)
neg = spot.translate(spot.formula_Not(f), 'med') neg = spot.translate(spot.formula_Not(f), 'med')
if ssi: if ssi:
......
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