jltl2ba.LTLFragments: Determine syntactic LTL fragment (safety, guarantee, persistence, obligation) for a given SimpleLTL formula

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12061 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/jltl2ba/LTLFragments.java

@@ -0,0 +1,330 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package jltl2ba;
+
+/**
+ * Helper to determine syntactic fragments of LTL formulas.
+ * <br>
+ * Each object stores information about membership in the
+ * "safety", "guarantee/co-safety", "obligation", "recurrence" and "persistence"
+ * fragments of LTL.
+ */
+public class LTLFragments
+{
+	private boolean syntacticSafety;
+	private boolean syntacticGuarantee;
+	private boolean syntacticObligation;
+	private boolean syntacticRecurrence;
+	private boolean syntacticPersistence;
+
+	/**
+	 * Constructor for basic formula (true, false, atomic proposition),
+	 * contained in all fragments.
+	 */
+	private LTLFragments()
+	{
+		syntacticSafety = true;
+		syntacticGuarantee = true;
+		syntacticObligation = true;
+		syntacticRecurrence = true;
+		syntacticPersistence = true;
+	}
+
+	/** Copy constructor */
+	private LTLFragments(LTLFragments other)
+	{
+		syntacticSafety = other.syntacticSafety;
+		syntacticGuarantee = other.syntacticGuarantee;
+		syntacticObligation = other.syntacticObligation;
+		syntacticRecurrence = other.syntacticRecurrence;
+		syntacticPersistence = other.syntacticPersistence;
+	}
+
+	/** Do we belong to the syntactic safety fragment? */
+	public boolean isSyntacticSafety()
+	{
+		return syntacticSafety;
+	}
+
+	/** Do we belong to the syntactic guarantee (co-safety) fragment? */
+	public boolean isSyntacticGuarantee()
+	{
+		return syntacticGuarantee;
+	}
+
+	/** Do we belong to the syntactic obligation fragment? */
+	public boolean isSyntacticObligation()
+	{
+		return syntacticObligation;
+	}
+
+	/** Do we belong to the syntactic recurrence fragment? */
+	public boolean isSyntacticRecurrence()
+	{
+		return syntacticRecurrence;
+	}
+
+	/** Do we belong to the syntactic persistence fragment? */
+	public boolean isSyntacticPersistence()
+	{
+		return syntacticPersistence;
+	}
+
+	@Override
+	public String toString()
+	{
+		String s = "[";
+		boolean first = true;
+
+		if (isSyntacticSafety()) {
+			if (!first) s+=",";
+			first = false;
+			s+="syntactic safety";
+		}
+
+		if (isSyntacticGuarantee()) {
+			if (!first) s+=",";
+			first = false;
+			s+="syntactic guarantee";
+		}
+
+		if (isSyntacticObligation()) {
+			if (!first) s+=",";
+			first = false;
+			s+="syntactic obligation";
+		}
+
+		if (isSyntacticRecurrence()) {
+			if (!first) s+=",";
+			first = false;
+			s+="syntactic recurrence";
+		}
+
+		if (isSyntacticPersistence()) {
+			if (!first) s+=",";
+			first = false;
+			s+="syntactic persistence";
+		}
+
+		return s+"]";
+	}
+
+	/**
+	 * Apply the Boolean AND operator (i.e., corresponding to this & other),
+	 * returning the result.
+	 */
+	private LTLFragments and(LTLFragments other)
+	{
+		LTLFragments result = new LTLFragments(this);
+
+		result.syntacticSafety &= other.syntacticSafety;
+		result.syntacticGuarantee &= other.syntacticGuarantee;
+		result.syntacticObligation &= other.syntacticObligation;
+		result.syntacticRecurrence &= other.syntacticRecurrence;
+		result.syntacticPersistence &= other.syntacticPersistence;
+
+		return result;
+	}
+
+	/**
+	 * Apply the Boolean OR operator (i.e., corresponding to this | other),
+	 * returning the result.
+	 */
+	private LTLFragments or(LTLFragments other)
+	{
+		LTLFragments result = new LTLFragments(this);
+
+		result.syntacticSafety &= other.syntacticSafety;
+		result.syntacticGuarantee &= other.syntacticGuarantee;
+		result.syntacticObligation &= other.syntacticObligation;
+		result.syntacticRecurrence &= other.syntacticRecurrence;
+		result.syntacticPersistence &= other.syntacticPersistence;
+
+		return result;
+	}
+
+	/**
+	 * Apply the Boolean NOT operator (i.e., corresponding to !this),
+	 * returning the result.
+	 */
+	private LTLFragments not()
+	{
+		LTLFragments result = new LTLFragments();
+
+		// take opposites
+		result.syntacticSafety = this.syntacticGuarantee;
+		result.syntacticGuarantee = this.syntacticSafety;
+
+		// obligation stays the same
+		result.syntacticObligation = this.syntacticObligation;
+
+		// take opposites
+		result.syntacticRecurrence = this.syntacticPersistence;
+		result.syntacticPersistence = this.syntacticRecurrence;
+
+		return result;
+	}
+
+	/**
+	 * Apply the temporal "nextstep" operator (i.e., corresponding to X this),
+	 * returning the result.
+	 */
+	private LTLFragments nextstep()
+	{
+		return new LTLFragments(this);  // just a copy
+	}
+
+	/**
+	 * Apply the temporal "eventually" operator (i.e., corresponding to F this),
+	 * returning the result.
+	 */
+	private LTLFragments eventually()
+	{
+		LTLFragments result = new LTLFragments(this);  // copy
+
+		result.syntacticSafety = false;
+		// syntacticGuarantee inherited
+		result.syntacticObligation = syntacticGuarantee;
+		result.syntacticRecurrence = syntacticGuarantee;
+		// syntacticPersistence inherited
+
+		return result;
+	}
+
+	/**
+	 * Apply the temporal "always" operator (i.e., corresponding to G this),
+	 * returning the result.
+	 */
+	private LTLFragments always()
+	{
+		LTLFragments result = new LTLFragments(this);  // copy
+
+		// syntacticSafety inherited
+		result.syntacticGuarantee = false;
+		result.syntacticObligation = syntacticSafety;
+		// syntacticRecurrence inherited
+		result.syntacticPersistence = syntacticSafety;
+
+		return result;
+	}
+
+	/**
+	 * Apply the temporal "until" operator (i.e., corresponding to this U other),
+	 * returning the result.
+	 */
+	private LTLFragments until(LTLFragments other)
+	{
+		LTLFragments result = new LTLFragments();
+		
+		result.syntacticSafety = false;
+		result.syntacticGuarantee = this.syntacticGuarantee & other.syntacticGuarantee;
+		result.syntacticObligation = this.syntacticObligation & other.syntacticGuarantee;
+		result.syntacticRecurrence = this.syntacticRecurrence & other.syntacticGuarantee;
+		result.syntacticPersistence = this.syntacticPersistence & other.syntacticPersistence;
+
+		return result;
+	}
+
+	/**
+	 * Apply the temporal "release" operator (i.e., corresponding to this R other),
+	 * returning the result.
+	 */
+	private LTLFragments release(LTLFragments other)
+	{
+		LTLFragments result = new LTLFragments();
+
+		result.syntacticSafety = this.syntacticSafety & other.syntacticSafety;
+		result.syntacticGuarantee = false;
+		result.syntacticObligation = this.syntacticObligation & other.syntacticSafety;
+		result.syntacticRecurrence = this.syntacticRecurrence & other.syntacticRecurrence;
+		result.syntacticPersistence = this.syntacticPersistence & other.syntacticSafety;
+
+		return result;
+	}
+
+	/**
+	 * Apply the Boolean EQUIV operator (i.e., corresponding to this &lt;-&gt; other),
+	 * returning the result.
+	 */
+	private LTLFragments equiv(LTLFragments other)
+	{
+		LTLFragments left = and(other);
+		LTLFragments right = not().and(other.not());
+
+		return left.or(right);
+	}
+
+	/**
+	 * Apply the Boolean IMPLIES operator (i.e., corresponding to this -&gt; other),
+	 * returning the result.
+	 */
+	private LTLFragments implies(LTLFragments other)
+	{
+		LTLFragments result = not().or(other);
+		return result;
+	}
+
+	/**
+	 * Analyse a given LTL formula and return the syntactic LTL fragments it belongs to.
+	 * @param root the root of the LTL formula
+	 * @return the LTLFragments it belongs to
+	 */
+	public static LTLFragments analyse(SimpleLTL root)
+	{
+		switch (root.kind) {
+		case TRUE:
+		case FALSE:
+			return new LTLFragments(); // all true
+		case AP:
+			return new LTLFragments(); // all true
+		case NOT:
+			return analyse(root.left).not();
+
+		case AND:
+			return analyse(root.left).and(analyse(root.right));
+		case OR:
+			return analyse(root.left).or(analyse(root.right));
+
+		case FINALLY:
+			return analyse(root.left).eventually();
+		case GLOBALLY:
+			return analyse(root.left).always();
+		case NEXT:
+			return analyse(root.left).nextstep();
+		case UNTIL:
+			return analyse(root.left).until(analyse(root.right));
+		case RELEASE:
+			return analyse(root.left).release(analyse(root.right));
+
+		case EQUIV:
+			return analyse(root.left).equiv(analyse(root.right));
+		case IMPLIES:
+			return analyse(root.left).implies(analyse(root.right));
+		}
+		throw new UnsupportedOperationException();
+	}
+}