Browse Source
Added CTL operators to the parser.
Added CTL operators to the parser.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@830 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
17 years ago
11 changed files with 1148 additions and 706 deletions
-
774prism/src/parser/PrismParser.java
-
46prism/src/parser/PrismParser.jj
-
158prism/src/parser/PrismParserConstants.java
-
580prism/src/parser/PrismParserTokenManager.java
-
115prism/src/parser/ast/ExpressionExists.java
-
115prism/src/parser/ast/ExpressionForAll.java
-
20prism/src/parser/visitor/ASTTraverse.java
-
20prism/src/parser/visitor/ASTTraverseModify.java
-
2prism/src/parser/visitor/ASTVisitor.java
-
14prism/src/parser/visitor/Rename.java
-
10prism/src/parser/visitor/TypeCheck.java
774
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
580
prism/src/parser/PrismParserTokenManager.java
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,115 @@ |
|||
//============================================================================== |
|||
// |
|||
// 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 parser.*; |
|||
import parser.visitor.*; |
|||
import prism.PrismLangException; |
|||
|
|||
public class ExpressionExists extends Expression |
|||
{ |
|||
Expression expression = null; |
|||
|
|||
// Constructors |
|||
|
|||
public ExpressionExists() |
|||
{ |
|||
} |
|||
|
|||
public ExpressionExists(Expression e) |
|||
{ |
|||
expression = e; |
|||
} |
|||
|
|||
// Set methods |
|||
|
|||
public void setExpression(Expression e) |
|||
{ |
|||
expression = e; |
|||
} |
|||
|
|||
// Get methods |
|||
|
|||
public Expression getExpression() |
|||
{ |
|||
return expression; |
|||
} |
|||
|
|||
// Methods required for Expression: |
|||
|
|||
/** |
|||
* Is this expression constant? |
|||
*/ |
|||
public boolean isConstant() |
|||
{ |
|||
return false; |
|||
} |
|||
|
|||
/** |
|||
* Evaluate this expression, return result. |
|||
* Note: assumes that type checking has been done already. |
|||
*/ |
|||
public Object evaluate(Values constantValues, Values varValues) throws PrismLangException |
|||
{ |
|||
throw new PrismLangException("Cannot evaluate an E operator without a model"); |
|||
} |
|||
|
|||
// Methods required for ASTElement: |
|||
|
|||
/** |
|||
* Visitor method. |
|||
*/ |
|||
public Object accept(ASTVisitor v) throws PrismLangException |
|||
{ |
|||
return v.visit(this); |
|||
} |
|||
|
|||
/** |
|||
* Convert to string. |
|||
*/ |
|||
public String toString() |
|||
{ |
|||
String s = ""; |
|||
|
|||
s += "E [ " + expression + " ]"; |
|||
|
|||
return s; |
|||
} |
|||
|
|||
/** |
|||
* Perform a deep copy. |
|||
*/ |
|||
public Expression deepCopy() |
|||
{ |
|||
ExpressionExists expr = new ExpressionExists(expression.deepCopy()); |
|||
expr.setType(type); |
|||
expr.setPosition(this); |
|||
return expr; |
|||
} |
|||
} |
|||
|
|||
//------------------------------------------------------------------------------ |
|||
@ -0,0 +1,115 @@ |
|||
//============================================================================== |
|||
// |
|||
// 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 parser.*; |
|||
import parser.visitor.*; |
|||
import prism.PrismLangException; |
|||
|
|||
public class ExpressionForAll extends Expression |
|||
{ |
|||
Expression expression = null; |
|||
|
|||
// Constructors |
|||
|
|||
public ExpressionForAll() |
|||
{ |
|||
} |
|||
|
|||
public ExpressionForAll(Expression e) |
|||
{ |
|||
expression = e; |
|||
} |
|||
|
|||
// Set methods |
|||
|
|||
public void setExpression(Expression e) |
|||
{ |
|||
expression = e; |
|||
} |
|||
|
|||
// Get methods |
|||
|
|||
public Expression getExpression() |
|||
{ |
|||
return expression; |
|||
} |
|||
|
|||
// Methods required for Expression: |
|||
|
|||
/** |
|||
* Is this expression constant? |
|||
*/ |
|||
public boolean isConstant() |
|||
{ |
|||
return false; |
|||
} |
|||
|
|||
/** |
|||
* Evaluate this expression, return result. |
|||
* Note: assumes that type checking has been done already. |
|||
*/ |
|||
public Object evaluate(Values constantValues, Values varValues) throws PrismLangException |
|||
{ |
|||
throw new PrismLangException("Cannot evaluate an E operator without a model"); |
|||
} |
|||
|
|||
// Methods required for ASTElement: |
|||
|
|||
/** |
|||
* Visitor method. |
|||
*/ |
|||
public Object accept(ASTVisitor v) throws PrismLangException |
|||
{ |
|||
return v.visit(this); |
|||
} |
|||
|
|||
/** |
|||
* Convert to string. |
|||
*/ |
|||
public String toString() |
|||
{ |
|||
String s = ""; |
|||
|
|||
s += "A [ " + expression + " ]"; |
|||
|
|||
return s; |
|||
} |
|||
|
|||
/** |
|||
* Perform a deep copy. |
|||
*/ |
|||
public Expression deepCopy() |
|||
{ |
|||
ExpressionForAll expr = new ExpressionForAll(expression.deepCopy()); |
|||
expr.setType(type); |
|||
expr.setPosition(this); |
|||
return expr; |
|||
} |
|||
} |
|||
|
|||
//------------------------------------------------------------------------------ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue