s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Code tidy. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10564 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
9493710a0f
commit
a9456fa826
18 changed files with 96 additions and 297 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 21
      prism/src/parser/ast/ExpressionBinaryOp.java
  2. 21
      prism/src/parser/ast/ExpressionConstant.java
  3. 21
      prism/src/parser/ast/ExpressionExists.java
  4. 24
      prism/src/parser/ast/ExpressionFilter.java
  5. 21
      prism/src/parser/ast/ExpressionForAll.java
  6. 21
      prism/src/parser/ast/ExpressionFormula.java
  7. 21
      prism/src/parser/ast/ExpressionFunc.java
  8. 21
      prism/src/parser/ast/ExpressionITE.java
  9. 21
      prism/src/parser/ast/ExpressionIdent.java
  10. 21
      prism/src/parser/ast/ExpressionLabel.java
  11. 21
      prism/src/parser/ast/ExpressionLiteral.java
  12. 25
      prism/src/parser/ast/ExpressionProb.java
  13. 21
      prism/src/parser/ast/ExpressionProp.java
  14. 25
      prism/src/parser/ast/ExpressionReward.java
  15. 25
      prism/src/parser/ast/ExpressionSS.java
  16. 21
      prism/src/parser/ast/ExpressionTemporal.java
  17. 21
      prism/src/parser/ast/ExpressionUnaryOp.java
  18. 21
      prism/src/parser/ast/ExpressionVar.java

21
prism/src/parser/ast/ExpressionBinaryOp.java
View File

@ -115,9 +115,7 @@ public class ExpressionBinaryOp extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return operand1.isConstant() && operand2.isConstant();
@ -129,10 +127,7 @@ public class ExpressionBinaryOp extends Expression
return operand1.isProposition() && operand2.isProposition();
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
switch (op) {
@ -212,25 +207,19 @@ public class ExpressionBinaryOp extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return operand1 + opSymbols[op] + operand2;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionBinaryOp expr = new ExpressionBinaryOp(op, operand1.deepCopy(), operand2.deepCopy());

21
prism/src/parser/ast/ExpressionConstant.java
View File

@ -63,9 +63,7 @@ public class ExpressionConstant extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return true;
@ -77,10 +75,7 @@ public class ExpressionConstant extends Expression
return true;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
Object res = ec.getConstantValue(name);
@ -97,25 +92,19 @@ public class ExpressionConstant extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return name;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
Expression ret = new ExpressionConstant(name, type);

21
prism/src/parser/ast/ExpressionExists.java
View File

@ -61,9 +61,7 @@ public class ExpressionExists extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -75,10 +73,7 @@ public class ExpressionExists extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate an E operator without a model");
@ -92,17 +87,13 @@ public class ExpressionExists extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -112,9 +103,7 @@ public class ExpressionExists extends Expression
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionExists expr = new ExpressionExists(expression.deepCopy());

24
prism/src/parser/ast/ExpressionFilter.java
View File

@ -184,9 +184,7 @@ public class ExpressionFilter extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
// Note: In some sense, ExpressionFilters are (often) constant since they return the same
@ -201,15 +199,13 @@ public class ExpressionFilter extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate a filter without a model");
}
@Override
public boolean returnsSingleValue()
{
// Most filters return a single value, but there are some exceptions...
@ -223,17 +219,13 @@ public class ExpressionFilter extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -246,9 +238,7 @@ public class ExpressionFilter extends Expression
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionFilter e;
@ -261,6 +251,8 @@ public class ExpressionFilter extends Expression
return e;
}
// Utility methods
/**
* Wrap a "default" ExpressionFilter around an Expression representing a property to be model checked,
* in order to pick out a single value (the final result of model checking) from a vector of values for all states.

21
prism/src/parser/ast/ExpressionForAll.java
View File

@ -61,9 +61,7 @@ public class ExpressionForAll extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -75,10 +73,7 @@ public class ExpressionForAll extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate an E operator without a model");
@ -92,17 +87,13 @@ public class ExpressionForAll extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -112,9 +103,7 @@ public class ExpressionForAll extends Expression
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionForAll expr = new ExpressionForAll(expression.deepCopy());

21
prism/src/parser/ast/ExpressionFormula.java
View File

@ -73,9 +73,7 @@ public class ExpressionFormula extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
// Unless defined, don't know so err on the side of caution
@ -89,10 +87,7 @@ public class ExpressionFormula extends Expression
return definition == null ? false : definition.isProposition();
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
// Should only be called (if at all) after definition has been set
@ -111,25 +106,19 @@ public class ExpressionFormula extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return name;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionFormula ret = new ExpressionFormula(name);

21
prism/src/parser/ast/ExpressionFunc.java
View File

@ -144,9 +144,7 @@ public class ExpressionFunc extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
int i, n;
@ -170,10 +168,7 @@ public class ExpressionFunc extends Expression
return true;
}
/**
* Evaluate this expression, return result. Note: assumes that type checking
* has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
switch (code) {
@ -362,17 +357,13 @@ public class ExpressionFunc extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
int i, n;
@ -396,9 +387,7 @@ public class ExpressionFunc extends Expression
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
int i, n;

21
prism/src/parser/ast/ExpressionITE.java
View File

@ -82,9 +82,7 @@ public class ExpressionITE extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return operand1.isConstant() && operand2.isConstant() && operand3.isConstant();
@ -96,10 +94,7 @@ public class ExpressionITE extends Expression
return operand1.isProposition() && operand2.isProposition() && operand3.isProposition();
}
/**
* Evaluate this expression, return result. Note: assumes that type checking
* has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
return operand1.evaluateBoolean(ec) ? operand2.evaluate(ec) : operand3.evaluate(ec);
@ -113,25 +108,19 @@ public class ExpressionITE extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return operand1 + " ? " + operand2 + " : " + operand3;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionITE expr = new ExpressionITE(operand1.deepCopy(), operand2.deepCopy(), operand3.deepCopy());

21
prism/src/parser/ast/ExpressionIdent.java
View File

@ -61,9 +61,7 @@ public class ExpressionIdent extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
// Don't know - err on the side of caution
@ -77,10 +75,7 @@ public class ExpressionIdent extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
// This should never be called.
@ -97,25 +92,19 @@ public class ExpressionIdent extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return name;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionIdent expr = new ExpressionIdent(name);

21
prism/src/parser/ast/ExpressionLabel.java
View File

@ -50,9 +50,7 @@ public class ExpressionLabel extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
// Don't know - err on the side of caution
@ -65,10 +63,7 @@ public class ExpressionLabel extends Expression
return true;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate labels", this);
@ -82,25 +77,19 @@ public class ExpressionLabel extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return "\"" + name + "\"";
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionLabel expr = new ExpressionLabel(name);

21
prism/src/parser/ast/ExpressionLiteral.java
View File

@ -76,9 +76,7 @@ public class ExpressionLiteral extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return true;
@ -90,10 +88,7 @@ public class ExpressionLiteral extends Expression
return true;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
return value;
@ -107,25 +102,19 @@ public class ExpressionLiteral extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return string;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
Expression expr = new ExpressionLiteral(type, value, string);

25
prism/src/parser/ast/ExpressionProb.java
View File

@ -94,9 +94,7 @@ public class ExpressionProb extends ExpressionQuant
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -108,18 +106,13 @@ public class ExpressionProb extends ExpressionQuant
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate a P operator without a model");
}
/**
* Get "name" of the result of this expression (used for y-axis of any graphs plotted)
*/
@Override
public String getResultName()
{
if (getBound() != null)
@ -140,17 +133,13 @@ public class ExpressionProb extends ExpressionQuant
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -165,9 +154,7 @@ public class ExpressionProb extends ExpressionQuant
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionProb expr = new ExpressionProb();

21
prism/src/parser/ast/ExpressionProp.java
View File

@ -53,9 +53,7 @@ public class ExpressionProp extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
// Don't know - err on the side of caution
@ -69,10 +67,7 @@ public class ExpressionProp extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate property references", this);
@ -86,25 +81,19 @@ public class ExpressionProp extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return "\"" + name + "\"";
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionProp expr = new ExpressionProp(name);

25
prism/src/parser/ast/ExpressionReward.java
View File

@ -166,9 +166,7 @@ public class ExpressionReward extends ExpressionQuant
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -180,18 +178,13 @@ public class ExpressionReward extends ExpressionQuant
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate an R operator without a model");
}
/**
* Get "name" of the result of this expression (used for y-axis of any graphs plotted)
*/
@Override
public String getResultName()
{
// For R=? properties, use name of reward structure where applicable
@ -226,17 +219,13 @@ public class ExpressionReward extends ExpressionQuant
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -260,9 +249,7 @@ public class ExpressionReward extends ExpressionQuant
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionReward expr = new ExpressionReward();

25
prism/src/parser/ast/ExpressionSS.java
View File

@ -87,9 +87,7 @@ public class ExpressionSS extends ExpressionQuant
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -101,18 +99,13 @@ public class ExpressionSS extends ExpressionQuant
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate an S operator without a model");
}
/**
* Get "name" of the result of this expression (used for y-axis of any graphs plotted)
*/
@Override
public String getResultName()
{
return (getBound() == null) ? "Probability" : "Result";
@ -126,17 +119,13 @@ public class ExpressionSS extends ExpressionQuant
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -150,9 +139,7 @@ public class ExpressionSS extends ExpressionQuant
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionSS expr = new ExpressionSS();

21
prism/src/parser/ast/ExpressionTemporal.java
View File

@ -205,9 +205,7 @@ public class ExpressionTemporal extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -219,10 +217,7 @@ public class ExpressionTemporal extends Expression
return false;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
throw new PrismLangException("Cannot evaluate a temporal operator without a path");
@ -236,17 +231,13 @@ public class ExpressionTemporal extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
String s = "";
@ -275,9 +266,7 @@ public class ExpressionTemporal extends Expression
return s;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionTemporal expr = new ExpressionTemporal();

21
prism/src/parser/ast/ExpressionUnaryOp.java
View File

@ -88,9 +88,7 @@ public class ExpressionUnaryOp extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return operand.isConstant();
@ -102,10 +100,7 @@ public class ExpressionUnaryOp extends Expression
return operand.isProposition();
}
/**
* Evaluate this expression, return result. Note: assumes that type checking
* has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
switch (op) {
@ -131,17 +126,13 @@ public class ExpressionUnaryOp extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
if (op == PARENTH)
@ -150,9 +141,7 @@ public class ExpressionUnaryOp extends Expression
return opSymbols[op] + operand;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionUnaryOp expr = new ExpressionUnaryOp(op, operand.deepCopy());

21
prism/src/parser/ast/ExpressionVar.java
View File

@ -73,9 +73,7 @@ public class ExpressionVar extends Expression
// Methods required for Expression:
/**
* Is this expression constant?
*/
@Override
public boolean isConstant()
{
return false;
@ -87,10 +85,7 @@ public class ExpressionVar extends Expression
return true;
}
/**
* Evaluate this expression, return result.
* Note: assumes that type checking has been done already.
*/
@Override
public Object evaluate(EvaluateContext ec) throws PrismLangException
{
Object res = ec.getVarValue(name, index);
@ -107,25 +102,19 @@ public class ExpressionVar extends Expression
// Methods required for ASTElement:
/**
* Visitor method.
*/
@Override
public Object accept(ASTVisitor v) throws PrismLangException
{
return v.visit(this);
}
/**
* Convert to string.
*/
@Override
public String toString()
{
return name;
}
/**
* Perform a deep copy.
*/
@Override
public Expression deepCopy()
{
ExpressionVar expr = new ExpressionVar(name, type);

Write Preview
Loading…
Cancel
Save