Add safety-liveness classification

client/src/LtlApp.js

@@ -197,6 +197,9 @@ const styles = theme => ({
     paddingBottom: 10
   },
   stutterdiv: {},
+  livenessdiv: {
+    paddingBottom: 10
+  },
   wordtable: {
     width: "auto"
   },
@@ -865,6 +868,34 @@ class LtlStudy extends React.Component {
             </Typography>
           )}
         </div>
+        <div className={this.props.classes.livenessdiv}>
+          <Typography variant="body2" color="primary">
+            Safety-Liveness classification
+          </Typography>
+          {res["safety_liveness"] === "safety" && (
+            <Typography>
+              This formula represents <b>a safety property</b>.
+            </Typography>
+          )}
+          {res["safety_liveness"] === "liveness" && (
+            <Typography>
+              This formula represents <b>a liveness property</b>.
+            </Typography>
+          )}
+          {res["safety_liveness"] === "both" && (
+            <Typography>
+              This formula represents both <b>a safety and a
+              liveness property</b>.
+            </Typography>
+          )}
+          {res["safety_liveness"] === "none" && (
+            <Typography>
+              This formula is neither a safety nor a
+              liveness property.  However it necessarily is the
+              {' '}<b>intersection</b> of a liveness and a safety property.
+            </Typography>
+          )}
+        </div>
         <div className={this.props.classes.satisfiabilitydiv}>
           <Typography variant="body2" color="primary">
             Satisfiability

server/spotapi.py

@@ -220,7 +220,8 @@ mp_class_to_english = {
 #   mp_hierarchy_svg: '<svg...'
 #   acc_word: 'word',     (an example of accepting 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')
+#   safety_liveness: 'safety'  (or 'liveness', or 'both', or 'none')
 # }
 @app.route('/api/study/<path:ltlformula>')
 @cachecontrol()
@@ -294,6 +295,17 @@ def study(ltlformula, method='GET'):
         else:
             result['rej_word'] = None;
 
+    if spot.is_liveness_automaton(pos):
+        if mp_class in ('S', 'B'):
+            result['safety_liveness'] = 'both'
+        else:
+            result['safety_liveness'] = 'liveness'
+    else:
+        if mp_class in ('S', 'B'):
+            result['safety_liveness'] = 'safety'
+        else:
+            result['safety_liveness'] = 'none'
+
     return jsonify(result)
 
 # Input parameters