From 04d8fb8e9ce6db82542311c29eba4560b3d8c10a Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:41 +0200 Subject: [PATCH] imported patch rewardcounter-TemporalOperatorBounds.patch --- .../parser/ast/TemporalOperatorBounds.java | 291 ++++++++++++++++++ prism/src/parser/visitor/ASTTraverse.java | 12 + .../src/parser/visitor/ASTTraverseModify.java | 12 + 3 files changed, 315 insertions(+) create mode 100644 prism/src/parser/ast/TemporalOperatorBounds.java diff --git a/prism/src/parser/ast/TemporalOperatorBounds.java b/prism/src/parser/ast/TemporalOperatorBounds.java new file mode 100644 index 00000000..6ba29c8a --- /dev/null +++ b/prism/src/parser/ast/TemporalOperatorBounds.java @@ -0,0 +1,291 @@ +//============================================================================== +// +// Copyright (c) 2015- +// 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 parser.ast; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; + +import parser.visitor.ASTVisitor; +import prism.ModelType; +import prism.PrismLangException; + +/** + * A conjunction of bounds attached to a temporal operator. + *
+ * If there is only one bound, it can be a DEFAULT_BOUND, where the + * bound type is context dependent. + */ +public class TemporalOperatorBounds extends ASTElement { + /** The list (conjunction) of TemporalOperatorBound */ + public List bounds = new ArrayList(); + + /** Get the list of bounds */ + public List getBounds() + { + return bounds; + } + + /** Adds the specified bound. Can only be used to add non-default bounds! */ + public void addBound(TemporalOperatorBound bound) + { + if (bound.getBoundType() == TemporalOperatorBound.BoundType.DEFAULT_BOUND) { + throw new IllegalArgumentException("Can not add default bound!"); + } + bounds.add(bound); + } + + /** + * Sets the default bound as the only bound. It is an error if bound is not a default bound. + */ + public void setDefaultBound(TemporalOperatorBound bound) { + if (bound.getBoundType() != TemporalOperatorBound.BoundType.DEFAULT_BOUND) { + throw new IllegalArgumentException("Can not set non-default bound as default bound!"); + } + + bounds.clear(); + bounds.add(bound); + } + + /** Get the number of bounds */ + public int countBounds() {return bounds.size();} + + /** Get the number of bounds of type TIME_BOUND */ + public int countTimeBounds() {return countBoundsOfType(TemporalOperatorBound.BoundType.TIME_BOUND);} + + /** Get the number of bounds of type STEP_BOUND */ + public int countStepBounds() {return countBoundsOfType(TemporalOperatorBound.BoundType.STEP_BOUND);} + + /** Get the number of bounds of type REWARD_BOUND */ + public int countRewardBounds() {return countBoundsOfType(TemporalOperatorBound.BoundType.REWARD_BOUND);} + + /** + * Get the number of bounds that resolve to a time bound in a discrete-time model, + * i.e., TIME_BOUND, STEP_BOUND and DEFAULT_BOUND + */ + public int countTimeBoundsDiscrete() { + return countBoundsOfType(TemporalOperatorBound.BoundType.TIME_BOUND, + TemporalOperatorBound.BoundType.STEP_BOUND, + TemporalOperatorBound.BoundType.DEFAULT_BOUND); + } + + /** + * Get the number of bounds that resolve to a time bound in a continuous-time model, + * i.e., TIME_BOUND and DEFAULT_BOUND + */ + public int countTimeBoundsContinuous() { + return countBoundsOfType(TemporalOperatorBound.BoundType.TIME_BOUND, + TemporalOperatorBound.BoundType.DEFAULT_BOUND); + } + + /** Is the list of bounds non-empty? */ + public boolean hasBounds() {return !bounds.isEmpty();} + + /** Are there bounds of type TIME_BOUND */ + public boolean hasTimeBounds() {return countTimeBounds() > 0;} + + /** Are there bounds of type STEP_BOUND */ + public boolean hasStepBounds() {return countStepBounds() > 0;} + + /** Are there bounds of type REWARD_BOUND */ + public boolean hasRewardBounds() {return countRewardBounds() > 0;} + + /** Do we have a bound of type DEFAULT_BOUND? */ + public boolean hasDefaultBound() {return countBoundsOfType(TemporalOperatorBound.BoundType.DEFAULT_BOUND) > 0;} + + /** + * Returns the default bound, if it exists. Otherwise, {@code null} is returned. + */ + public TemporalOperatorBound getDefaultBound() + { + return getFirstOfBoundType(TemporalOperatorBound.BoundType.DEFAULT_BOUND); + } + + /** + * Returns the default bound or the single time bound. + * Returns {@code null} if there is none, + * throws exception if there are multiple time bounds. + */ + public TemporalOperatorBound getTimeBoundForContinuousTime() throws PrismLangException + { + if (hasDefaultBound()) {return getDefaultBound();} + if (countTimeBounds() > 1) { + throw new PrismLangException("Multiple time bounds, not supported!"); + } + return getFirstOfBoundType(TemporalOperatorBound.BoundType.TIME_BOUND); + } + + /** + * Returns the default bound, the single time bound or the single step bound. + * Returns {@code null} if there is none, throws exception if there are multiple bounds. + */ + public TemporalOperatorBound getStepBoundForDiscreteTime() throws PrismLangException + { + if (hasDefaultBound()) {return getDefaultBound();} + if (countTimeBounds() + countStepBounds() > 1) { + throw new PrismLangException("Multiple step/time bounds, not supported!"); + } + if (hasStepBounds()) { + return getFirstOfBoundType(TemporalOperatorBound.BoundType.STEP_BOUND); + } + return getFirstOfBoundType(TemporalOperatorBound.BoundType.TIME_BOUND); + } + + /** + * Return the step bounds in a discrete time setting, + * i.e., all STEP_BOUND, TIME_BOUND and DEFAULT_BOUND. + */ + public List getStepBoundsForDiscreteTime() throws PrismLangException + { + return getBoundsOfType(TemporalOperatorBound.BoundType.STEP_BOUND, + TemporalOperatorBound.BoundType.TIME_BOUND, + TemporalOperatorBound.BoundType.DEFAULT_BOUND); + } + + /** + * Return the time bounds in a continuous time setting, + * i.e., all TIME_BOUND and DEFAULT_BOUND. + */ + public List getStepBoundsForContinuousTime() throws PrismLangException + { + return getBoundsOfType(TemporalOperatorBound.BoundType.TIME_BOUND, + TemporalOperatorBound.BoundType.DEFAULT_BOUND); + } + + /** + * Returns the standard time/step bound for the given model type, + * either from default bound or specific time / step bound. + * Throws an exception if there are more than one step/time bounds. + * @param modelType the model type + */ + public TemporalOperatorBound getStandardBound(ModelType modelType) throws PrismLangException + { + if (modelType.continuousTime()) { + return getTimeBoundForContinuousTime(); + } else { + return getStepBoundForDiscreteTime(); + } + } + + /** + * Return the reward bounds. + */ + public List getRewardBounds() throws PrismLangException + { + return getBoundsOfType(TemporalOperatorBound.BoundType.REWARD_BOUND); + } + + @Override + public Object accept(ASTVisitor v) throws PrismLangException { + return v.visit(this); + } + + @Override + public String toString() { + if (hasDefaultBound()) { + return getDefaultBound().toString(); + } else { + // TODO(JK): Change format: String result = "^{"; + String result = "{"; + boolean first=true; + for (TemporalOperatorBound bound : getBounds()) { + if (!first) result+=", "; + first=false; + result+=bound.toString(); + } + result+="}"; + return result; + } + } + + @Override + public int hashCode() + { + final int prime = 31; + int result = 1; + result = prime * result + ((bounds == null) ? 0 : bounds.hashCode()); + return result; + } + + @Override + public boolean equals(Object obj) + { + if (this == obj) + return true; + if (obj == null) + return false; + if (!(obj instanceof TemporalOperatorBounds)) + return false; + TemporalOperatorBounds other = (TemporalOperatorBounds) obj; + if (bounds == null) { + if (other.bounds != null) + return false; + } else if (!bounds.equals(other.bounds)) + return false; + return true; + } + + @Override + public TemporalOperatorBounds deepCopy() { + TemporalOperatorBounds result = new TemporalOperatorBounds(); + for (TemporalOperatorBound bound : bounds) { + result.bounds.add(bound.deepCopy()); + } + return result; + } + + /** Helper: Count the number of bounds with the specified type */ + private int countBoundsOfType(TemporalOperatorBound.BoundType... boundTypes) + { + return getBoundsOfType(boundTypes).size(); + } + + /** Get the first bound of the given type, {@code null} if there is none. */ + public TemporalOperatorBound getFirstOfBoundType(TemporalOperatorBound.BoundType boundType) { + for (TemporalOperatorBound bound : bounds) { + if (bound.getBoundType() == boundType) { + return bound; + } + } + return null; + } + + /** Get a list of all bounds of the given types */ + public List getBoundsOfType(TemporalOperatorBound.BoundType... types) { + HashSet typeSet = new HashSet(Arrays.asList(types)); + ArrayList result = new ArrayList(); + + for (TemporalOperatorBound bound : getBounds()) { + if (typeSet.contains(bound.getBoundType())) { + result.add(bound); + } + } + + return result; + } +} diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 692187e7..16ab7e1c 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -629,6 +629,18 @@ public class ASTTraverse implements ASTVisitor } public void visitPost(TemporalOperatorBound e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(TemporalOperatorBounds e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(TemporalOperatorBounds e) throws PrismLangException + { + visitPre(e); + for (TemporalOperatorBound bound : e.getBounds()) { + bound.accept(this); + } + visitPost(e); + return null; + } + public void visitPost(TemporalOperatorBounds e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(QuotedString e) throws PrismLangException { defaultVisitPre(e); } public Object visit(QuotedString e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 2b7606c5..4d76f815 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -642,6 +642,18 @@ public class ASTTraverseModify implements ASTVisitor } public void visitPost(TemporalOperatorBound e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(TemporalOperatorBounds e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(TemporalOperatorBounds e) throws PrismLangException + { + visitPre(e); + for (int i = 0; i < e.getBounds().size(); i++) { + e.getBounds().set(i, (TemporalOperatorBound) e.getBounds().get(i).accept(this)); + } + visitPost(e); + return e; + } + public void visitPost(TemporalOperatorBounds e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(QuotedString e) throws PrismLangException { defaultVisitPre(e); } public Object visit(QuotedString e) throws PrismLangException {