You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
148 lines
4.2 KiB
148 lines
4.2 KiB
//==============================================================================
|
|
//
|
|
// Copyright (c) 2002-
|
|
// Authors:
|
|
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
|
|
//
|
|
//------------------------------------------------------------------------------
|
|
//
|
|
// 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 param.BigRational;
|
|
import parser.EvaluateContext;
|
|
import parser.type.TypePathBool;
|
|
import parser.visitor.ASTVisitor;
|
|
import prism.PrismLangException;
|
|
|
|
public class ExpressionAccumulation extends Expression
|
|
{
|
|
AccumulationSymbol symbol;
|
|
AccumulationConstraint constraint;
|
|
ExpressionRegular regexp;
|
|
TemporalOperatorBound bound;
|
|
|
|
public ExpressionAccumulation(AccumulationSymbol symbol) {
|
|
this.symbol = symbol;
|
|
this.setType(TypePathBool.getInstance());
|
|
}
|
|
|
|
public boolean hasRegularExpression() {
|
|
return regexp != null;
|
|
}
|
|
|
|
public boolean hasBoundExpression() {
|
|
return bound != null;
|
|
}
|
|
|
|
public AccumulationSymbol getSymbol() {
|
|
return symbol;
|
|
}
|
|
public void setSymbol(AccumulationSymbol symbol) {
|
|
this.symbol = symbol;
|
|
}
|
|
public AccumulationConstraint getConstraint() {
|
|
return constraint;
|
|
}
|
|
public void setConstraint(AccumulationConstraint constraint) {
|
|
this.constraint = constraint;
|
|
}
|
|
public ExpressionRegular getRegularExpression() {
|
|
if ( hasRegularExpression() ) { return regexp; }
|
|
else throw new RuntimeException("getRegularExpression called without RegularExpression");
|
|
}
|
|
public void setRegularExpression(ExpressionRegular regexp) {
|
|
this.bound = null;
|
|
this.regexp = regexp;
|
|
}
|
|
|
|
public TemporalOperatorBound getBoundExpression() {
|
|
if ( hasBoundExpression() ) { return bound; }
|
|
else throw new RuntimeException("getBoundExpression called without BoundExpression");
|
|
}
|
|
|
|
public void setBoundExpression(TemporalOperatorBound bound) {
|
|
if ( bound.isDefaultBound() && bound.hasUpperBound() ) {
|
|
this.regexp= null;
|
|
this.bound = bound;
|
|
} else {
|
|
throw new RuntimeException("Bounds need to be upper and default.");
|
|
}
|
|
}
|
|
|
|
// Add a toString
|
|
public String toString() {
|
|
String ret = "";
|
|
ret += symbol.toString();
|
|
if ( hasRegularExpression() ) { ret += "( Reg:" + regexp.toString() + ")"; }
|
|
else if ( hasBoundExpression() ) { ret += "(" + bound.toString() + ")"; }
|
|
else throw new RuntimeException("Cannot stringify AccumulationExpression without fragment bounds.");
|
|
ret += "(" + constraint.toString() + ")";
|
|
return ret;
|
|
}
|
|
|
|
@Override
|
|
public boolean isConstant() {
|
|
return false;
|
|
}
|
|
|
|
@Override
|
|
public boolean isProposition() {
|
|
return false;
|
|
}
|
|
|
|
@Override
|
|
public Object evaluate(EvaluateContext ec) throws PrismLangException {
|
|
return null;
|
|
}
|
|
|
|
@Override
|
|
public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException {
|
|
return null;
|
|
}
|
|
|
|
@Override
|
|
public boolean returnsSingleValue() {
|
|
return false;
|
|
}
|
|
|
|
@Override
|
|
public Expression deepCopy() {
|
|
ExpressionAccumulation ret = new ExpressionAccumulation(this.getSymbol());
|
|
|
|
ret.setConstraint(this.getConstraint().deepCopy());
|
|
if ( this.hasBoundExpression() ) {
|
|
ret.setBoundExpression(this.getBoundExpression().deepCopy());
|
|
}
|
|
if ( this.hasRegularExpression() ) {
|
|
ret.setRegularExpression((ExpressionRegular) this.getRegularExpression().deepCopy());
|
|
}
|
|
|
|
return ret;
|
|
}
|
|
|
|
@Override
|
|
public Object accept(ASTVisitor v) throws PrismLangException {
|
|
return v.visit(this);
|
|
}
|
|
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|