From b13aa417ad134d83f9a05e28e66353dbd0196339 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Dec 2012 12:35:27 +0000 Subject: [PATCH] Un-needed files (since fairnesss stuff not in this branch, currently). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6213 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ExpressionAction.java | 83 --------- prism/src/parser/ast/ExpressionFairness.java | 168 ------------------ prism/src/parser/visitor/ASTTraverse.java | 24 --- .../src/parser/visitor/ASTTraverseModify.java | 25 --- prism/src/parser/visitor/ASTVisitor.java | 2 - 5 files changed, 302 deletions(-) delete mode 100644 prism/src/parser/ast/ExpressionAction.java delete mode 100644 prism/src/parser/ast/ExpressionFairness.java diff --git a/prism/src/parser/ast/ExpressionAction.java b/prism/src/parser/ast/ExpressionAction.java deleted file mode 100644 index c75a4e24..00000000 --- a/prism/src/parser/ast/ExpressionAction.java +++ /dev/null @@ -1,83 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Hongyang Qu (University of Oxford) -// * Dave Parker (University of 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 parser.EvaluateContext; -import parser.visitor.ASTVisitor; -import prism.PrismLangException; - -/** - * Store an action in fairness constraints - * @author hongyang - * - */ -public class ExpressionAction extends Expression { - protected String action; - protected int index; // index in the action list - - public ExpressionAction(String action) { - this.action = action; - } - - public String getName() { - return action; - } - - public void setIndex(int index) { - this.index = index; - } - - public int getIndex() { - return index; - } - - public Expression deepCopy() { - return new ExpressionAction(new String(action)); - } - - public Object evaluate(EvaluateContext ec) throws PrismLangException { - throw new PrismLangException("Cannot evaluate action", this); - } - - public boolean isConstant() { - return false; - } - - public boolean returnsSingleValue() { - return false; - } - - public Object accept(ASTVisitor v) throws PrismLangException { - return v.visit(this); - } - - public String toString() { - return "[" + action + "]"; - } - -} diff --git a/prism/src/parser/ast/ExpressionFairness.java b/prism/src/parser/ast/ExpressionFairness.java deleted file mode 100644 index e361f31a..00000000 --- a/prism/src/parser/ast/ExpressionFairness.java +++ /dev/null @@ -1,168 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Hongyang Qu (University of Oxford) -// * Dave Parker (University of 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.Vector; - -import parser.EvaluateContext; -import parser.visitor.ASTVisitor; -import prism.PrismLangException; - -/** - * Encode a fairness constraint, which has two set H and K of states and actions. - * @author Hongyang Qu - * - */ -public class ExpressionFairness extends Expression { - protected boolean isStrong; - // Strong fairness: G F H -> G F K - // Weak fairness: F G H -> G F K - // Each expression can be either Boolean (for states) or Label (for actions) - protected Vector H; - protected Vector K; - - public ExpressionFairness(boolean isStrong, Vector H, Vector K) { - this.isStrong = isStrong; - this.H = H; - this.K = K; - } - - public boolean isStrongFairness() { - return isStrong; - } - - public Vector getH() { - return H; - } - - public int getSizeH() { - if(H == null) - return 0; - return H.size(); - } - - public Vector getK() { - return K; - } - - public int getSizeK() { - if(K == null) - return 0; - return K.size(); - } - - public Expression getExpressionH(int index) { - if(H != null && H.size()+1>= index) - return H.get(index); - return null; - } - - public Expression getExpressionK(int index) { - if(K != null && K.size()+1>= index) - return K.get(index); - return null; - } - - public void setExpressionH(int index, Expression e) { - if(H != null && H.size()+1>= index) { - H.remove(index); - H.add(index, e); - } - } - - public void setExpressionK(int index, Expression e) { - if(K != null && K.size()+1>= index) { - K.remove(index); - K.add(index, e); - } - } - - @Override - public Expression deepCopy() { - Vector newH = null; - if(H != null) { - newH = new Vector(); - for(Expression e: H) { - newH.add(e.deepCopy()); - } - } - Vector newK = null; - if(K != null) { - newK = new Vector(); - for(Expression e: K) { - newK.add(e.deepCopy()); - } - } - - return new ExpressionFairness(isStrong, newH, newK); - } - - @Override - public Object evaluate(EvaluateContext ec) throws PrismLangException { - throw new PrismLangException("Cannot evaluate Fairness constraint", this); - } - - @Override - public boolean isConstant() { - return false; - } - - @Override - public boolean returnsSingleValue() { - return false; - } - - @Override - public Object accept(ASTVisitor v) throws PrismLangException { - return v.visit(this); - } - - @Override - public String toString() { - String s = isStrong? "SF" : "WF"; - s += "("; - s += "{"; - if(H != null) { - int i=0; - for(Expression e: H) { - s += (i==0? "" : ", ") + e.toString(); - } - } - s += "}, {"; - if(K != null) { - int i=0; - for(Expression e: K) { - s += (i==0? "" : ", ") + e.toString(); - } - } - s += "}"; - s += ")"; - - return s; - } -} diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 0379186e..ea3e86c2 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -552,30 +552,6 @@ public class ASTTraverse implements ASTVisitor } public void visitPost(ExpressionFilter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- - public void visitPre(ExpressionFairness e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFairness e) throws PrismLangException { - visitPre(e); - int i, n; - n = e.getSizeH(); - for (i = 0; i < n; i++) - e.getExpressionH(i).accept(this); - n = e.getSizeK(); - for (i = 0; i < n; i++) - e.getExpressionK(i).accept(this); - visitPost(e); - return null; - } - public void visitPost(ExpressionFairness e) throws PrismLangException { defaultVisitPost(e); } - // ----------------------------------------------------------------------------------- - public void visitPre(ExpressionAction e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionAction e) throws PrismLangException - { - visitPre(e); - visitPost(e); - return null; - } - public void visitPost(ExpressionAction e) throws PrismLangException { defaultVisitPost(e); } - // ----------------------------------------------------------------------------------- public void visitPre(Filter e) throws PrismLangException { defaultVisitPre(e); } public Object visit(Filter e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index b3372494..59826150 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -561,31 +561,6 @@ public class ASTTraverseModify implements ASTVisitor } public void visitPost(ExpressionFilter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- - public void visitPre(ExpressionFairness e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFairness e) throws PrismLangException - { - visitPre(e); - int i, n; - n = e.getSizeH(); - for (i = 0; i < n; i++) - e.setExpressionH(i, (Expression) e.getExpressionH(i).accept(this)); - n = e.getSizeK(); - for (i = 0; i < n; i++) - e.setExpressionK(i, (Expression) e.getExpressionK(i).accept(this)); - visitPost(e); - return e; - } - public void visitPost(ExpressionFairness e) throws PrismLangException { defaultVisitPost(e); } - // ----------------------------------------------------------------------------------- - public void visitPre(ExpressionAction e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionAction e) throws PrismLangException - { - visitPre(e); - visitPost(e); - return e; - } - public void visitPost(ExpressionAction e) throws PrismLangException { defaultVisitPost(e); } - // ----------------------------------------------------------------------------------- public void visitPre(ForLoop e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ForLoop e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 3ea8bfe6..6e8b1620 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -77,8 +77,6 @@ public interface ASTVisitor public Object visit(ExpressionLabel e) throws PrismLangException; public Object visit(ExpressionProp e) throws PrismLangException; public Object visit(ExpressionFilter e) throws PrismLangException; - public Object visit(ExpressionFairness e) throws PrismLangException; - public Object visit(ExpressionAction e) throws PrismLangException; // ASTElement classes (misc.) public Object visit(Filter e) throws PrismLangException; public Object visit(ForLoop e) throws PrismLangException;