Browse Source
Add strategy operators (<<>> and [[]]) to parser, but no support model checking.
Add strategy operators (<<>> and [[]]) to parser, but no support model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9219 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
12 years ago
11 changed files with 928 additions and 509 deletions
-
937prism/src/parser/PrismParser.java
-
32prism/src/parser/PrismParser.jj
-
56prism/src/parser/PrismParserConstants.java
-
198prism/src/parser/PrismParserTokenManager.java
-
175prism/src/parser/ast/ExpressionStrategy.java
-
10prism/src/parser/visitor/ASTTraverse.java
-
10prism/src/parser/visitor/ASTTraverseModify.java
-
1prism/src/parser/visitor/ASTVisitor.java
-
6prism/src/parser/visitor/CheckValid.java
-
7prism/src/parser/visitor/Rename.java
-
5prism/src/parser/visitor/TypeCheck.java
937
prism/src/parser/PrismParser.java
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,175 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2002- |
|||
// Authors: |
|||
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford) |
|||
// |
|||
//------------------------------------------------------------------------------ |
|||
// |
|||
// 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.List; |
|||
|
|||
import parser.EvaluateContext; |
|||
import parser.visitor.ASTVisitor; |
|||
import prism.PrismLangException; |
|||
import prism.PrismUtils; |
|||
|
|||
/** |
|||
* Class to represent ATL <<.>> and [[.]] operators, i.e. quantification over strategies |
|||
* ("there exists a strategy" or "for all strategies"). |
|||
*/ |
|||
public class ExpressionStrategy extends Expression |
|||
{ |
|||
/** "There exists a strategy" (true) or "for all strategies" (false) */ |
|||
protected boolean thereExists = false; |
|||
|
|||
// Coalition info (for game models) |
|||
/** Coalition: list of player names */ |
|||
protected List<String> coalition = null; |
|||
|
|||
/** Child expression */ |
|||
protected Expression expression = null; |
|||
|
|||
// Constructors |
|||
|
|||
public ExpressionStrategy() |
|||
{ |
|||
|
|||
} |
|||
|
|||
public ExpressionStrategy(boolean thereExists) |
|||
{ |
|||
this.thereExists = thereExists; |
|||
} |
|||
|
|||
public ExpressionStrategy(boolean thereExists, Expression expression) |
|||
{ |
|||
this.thereExists = thereExists; |
|||
this.expression = expression; |
|||
} |
|||
|
|||
// Set methods |
|||
|
|||
public void setThereExists(boolean thereExists) |
|||
{ |
|||
this.thereExists = thereExists; |
|||
} |
|||
|
|||
public void setCoalition(List<String> coalition) |
|||
{ |
|||
this.coalition = coalition; |
|||
} |
|||
|
|||
public void setExpression(Expression expression) |
|||
{ |
|||
this.expression = expression; |
|||
} |
|||
|
|||
// Get methods |
|||
|
|||
public boolean isThereExists() |
|||
{ |
|||
return thereExists; |
|||
} |
|||
|
|||
/** |
|||
* Get a string ""<<>>"" or "[[]]" indicating type of quantification. |
|||
*/ |
|||
public String getOperatorString() |
|||
{ |
|||
return thereExists ? "<<>>" : "[[]]"; |
|||
} |
|||
|
|||
public List<String> getCoalition() |
|||
{ |
|||
return coalition; |
|||
} |
|||
|
|||
public Expression getExpression() |
|||
{ |
|||
return expression; |
|||
} |
|||
|
|||
// Methods required for Expression: |
|||
|
|||
@Override |
|||
public boolean isConstant() |
|||
{ |
|||
return false; |
|||
} |
|||
|
|||
@Override |
|||
public boolean isProposition() |
|||
{ |
|||
return false; |
|||
} |
|||
|
|||
@Override |
|||
public Object evaluate(EvaluateContext ec) throws PrismLangException |
|||
{ |
|||
throw new PrismLangException("Cannot evaluate a " + getOperatorString() + " operator without a model"); |
|||
} |
|||
|
|||
@Override |
|||
public String getResultName() |
|||
{ |
|||
return expression.getResultName(); |
|||
} |
|||
|
|||
@Override |
|||
public boolean returnsSingleValue() |
|||
{ |
|||
return false; |
|||
} |
|||
|
|||
// Methods required for ASTElement: |
|||
|
|||
@Override |
|||
public Object accept(ASTVisitor v) throws PrismLangException |
|||
{ |
|||
return v.visit(this); |
|||
} |
|||
|
|||
@Override |
|||
public String toString() |
|||
{ |
|||
String s = ""; |
|||
s += (thereExists ? "<<" : "[["); |
|||
s += PrismUtils.joinString(coalition, ","); |
|||
s += (thereExists ? ">>" : "]]"); |
|||
s += " " + expression.toString(); |
|||
return s; |
|||
} |
|||
|
|||
@Override |
|||
public Expression deepCopy() |
|||
{ |
|||
ExpressionStrategy expr = new ExpressionStrategy(); |
|||
expr.setThereExists(isThereExists()); |
|||
expr.setCoalition(new ArrayList<String>(coalition)); |
|||
expr.setExpression(expression == null ? null : expression.deepCopy()); |
|||
expr.setType(type); |
|||
expr.setPosition(this); |
|||
return expr; |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue