From 39c2dadc387142a095bb9df7166809ef266d7f9b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 19 Jul 2017 12:31:52 +0000 Subject: [PATCH] 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 | 330 ++++++++++++++++++++++++++++ 1 file changed, 330 insertions(+) create mode 100644 prism/src/jltl2ba/LTLFragments.java diff --git a/prism/src/jltl2ba/LTLFragments.java b/prism/src/jltl2ba/LTLFragments.java new file mode 100644 index 00000000..5413eb20 --- /dev/null +++ b/prism/src/jltl2ba/LTLFragments.java @@ -0,0 +1,330 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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. + *
+ * 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 <-> 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 -> 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(); + } +}