From d39a355cc5ef14bad11112685982fd0100eafb25 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Sat, 18 Jul 2015 15:51:05 +0200
Subject: [PATCH] refactoring based on findbugs guidelines
---
.../de/tlc4b/analysis/ConstantsEvaluator.java | 37 ++++----
.../de/tlc4b/analysis/MachineContext.java | 7 +-
src/main/java/de/tlc4b/analysis/Renamer.java | 17 +---
.../de/tlc4b/analysis/StandardMadules.java | 48 +++++++---
.../typerestriction/TypeRestrictor.java | 38 ++++----
src/main/java/de/tlc4b/btypes/StructType.java | 89 ++++++++++++-------
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 19 ++--
src/main/java/de/tlc4b/tlc/TLCResults.java | 35 +++++---
.../coverage/IntegrationCoverageTest.java | 1 +
.../de/tlc4b/tlc/integration/BugTest.java | 15 ----
10 files changed, 172 insertions(+), 134 deletions(-)
delete mode 100644 src/test/java/de/tlc4b/tlc/integration/BugTest.java
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
index 0e2a79e..bba3e86 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
@@ -55,15 +55,16 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
public LinkedHashMap<Node, Node> getValueOfIdentifierMap() {
return valueOfIdentifier;
}
-
+
public Integer getIntValue(Node node) {
return integerValueTable.get(node);
}
- public ArrayList<PExpression> getRangeOfIdentifier(Node con){;
+ public ArrayList<PExpression> getRangeOfIdentifier(Node con) {
+ ;
return valuesOfConstantsFinder.rangeOfIdentifierTable.get(con);
}
-
+
public ConstantsEvaluator(MachineContext machineContext) {
this.dependsOnIdentifierTable = new Hashtable<Node, HashSet<Node>>();
this.integerValueTable = new HashMap<Node, Integer>();
@@ -162,7 +163,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
@Override
public void caseAPredicateParseUnit(APredicateParseUnit node) {
defaultIn(node);
- node.getPredicate();
+ node.getPredicate().apply(this);
}
@Override
@@ -194,7 +195,8 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
this.rangeOfIdentifierTable = new Hashtable<Node, ArrayList<PExpression>>();
this.identifiers = new HashSet<Node>();
- this.identifiers.addAll(machineContext.getBMachineConstants().values());
+ this.identifiers.addAll(machineContext.getBMachineConstants()
+ .values());
this.identifiers.addAll(machineContext.getScalarParameter()
.values());
@@ -217,18 +219,19 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (machineContext.getConstantsSetup() instanceof ADisjunctPredicate) {
analyseConstantSetupPredicate(machineContext
.getConstantsSetup());
-
+
for (Node con : this.identifiers) {
- ArrayList<PExpression> list = rangeOfIdentifierTable.get(con);
- if(list.size() == 1){
- // there only one value for the constant con, hence con remains a constant
+ ArrayList<PExpression> list = rangeOfIdentifierTable
+ .get(con);
+ if (list.size() == 1) {
+ // there only one value for the constant con, hence
+ // con remains a constant
valuesOfIdentifierTable.get(con).add(list.get(0));
}
}
- }else{
+ } else {
analysePredicate(machineContext.getConstantsSetup(), true);
}
-
}
@@ -260,20 +263,22 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
AEqualPredicate equals = (AEqualPredicate) constantsSetup;
PExpression left = equals.getLeft();
Node left_ref = machineContext.getReferences().get(left);
- if(rangeOfIdentifierTable.containsKey(left_ref)){
+ if (rangeOfIdentifierTable.containsKey(left_ref)) {
System.out.println("hallo");
}
- ArrayList<PExpression> currentRange = rangeOfIdentifierTable.get(left_ref);
+ ArrayList<PExpression> currentRange = rangeOfIdentifierTable
+ .get(left_ref);
boolean found = false;
for (PExpression pExpression : currentRange) {
- if(pExpression.toString().equals(equals.getRight().toString())){
+ if (pExpression.toString().equals(
+ equals.getRight().toString())) {
found = true;
}
}
- if(found == false){
+ if (found == false) {
currentRange.add((PExpression) equals.getRight());
}
-
+
}
}
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index a9bbc81..24c46ea 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -569,9 +569,10 @@ public class MachineContext extends DepthFirstAdapter {
private ArrayList<MachineContext> lookupExtendedMachines() {
ArrayList<MachineContext> list = new ArrayList<MachineContext>();
- for (String s : seenMachines.keySet()) {
- AIdentifierExpression i = seenMachines.get(s);
- if (i.getIdentifier().size() == 1) {
+ for( Entry<String, AIdentifierExpression> entry : seenMachines.entrySet()){
+ String s = entry.getKey();
+ AIdentifierExpression value = entry.getValue();
+ if (value.getIdentifier().size() == 1) {
list.add(machineContextsTable.get(s));
}
}
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 4b397ec..b2c0c5d 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -93,17 +93,6 @@ public class Renamer extends DepthFirstAdapter {
}
- private final static Set<String> SequencesKeywords = new HashSet<String>();
- static {
- SequencesKeywords.add("Seq");
- SequencesKeywords.add("Len");
- SequencesKeywords.add("Append");
- SequencesKeywords.add("Head");
- SequencesKeywords.add("Tail");
- SequencesKeywords.add("Subseq");
- SequencesKeywords.add("SelectSeq");
- }
-
public Renamer(MachineContext machineContext) {
this.machineContext = machineContext;
this.namesTable = new Hashtable<Node, String>();
@@ -210,11 +199,11 @@ public class Renamer extends DepthFirstAdapter {
return true;
// TODO check only if the standard module is extended
- if (StandardMadules.functions.contains(name))
+ if (StandardMadules.isKeywordInModuleFunctions(name))
return true;
- if (SequencesKeywords.contains(name))
+ if (StandardMadules.isKeywordInModuleSequences(name))
return true;
- if (StandardMadules.SequencesExtendedKeywords.contains(name))
+ if (StandardMadules.isKeywordInModuleSequencesExtended(name))
return true;
for (int i = 0; i < localContexts.size(); i++) {
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 5d8ae04..763d079 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -6,9 +6,9 @@ import java.util.Set;
public final class StandardMadules {
- private StandardMadules(){
+ private StandardMadules() {
}
-
+
// Functions
public static final String FUNC_RANGE = "Range";
public static final String FUNC_IMAGE = "Image";
@@ -21,8 +21,7 @@ public final class StandardMadules {
public static final String FUNC_OVERRIDE = "Override";
public static final String FUNC_ASSIGN = "FuncAssign";
-
- public static final ArrayList<String> functions = new ArrayList<String>();
+ private static final ArrayList<String> functions = new ArrayList<String>();
static {
functions.add(FUNC_RANGE);
functions.add(FUNC_ID);
@@ -35,26 +34,29 @@ public final class StandardMadules {
functions.add(FUNC_ASSIGN);
}
+ public static final boolean isKeywordInModuleFunctions(String name) {
+ return functions.contains(name);
+ }
+
public static final String TOTAL_INJECTIVE_FUNCTION = "TotalInjFunc";
public static final String TOTAL_SURJECTIVE_FUNCTION = "TotalSurFunc";
public static final String TOTAL_BIJECTIVE_FUNCTION = "TotalBijFunc";
-
/** Sets of Partial functions **/
public static final String PARTIAL_FUNCTION = "ParFunc";
public static final String PARTIAL_FUNCTION_ELEMENT_OF = "ParFuncEleOf";
public static final String ELEMENT_OF_PARTIAL_FUNCTION = "isEleOfParFunc";
-
+
// injective
public static final String PARTIAL_INJECTIVE_FUNCTION = "ParInjFunc";
public static final String PARTIAL_INJECTIVE_FUNCTION_ELEMENT_OF = "ParInjFuncEleOf";
- // surjective
+ // surjective
public static final String PARTIAL_SURJECTIVE_FUNCTION = "ParSurFunc";
public static final String PARTIAL_SURJECTIVE_FUNCTION_ELEMENT_OF = "ParSurFuncEleOf";
// bijective
public static final String PARITAL_BIJECTIVE_FUNCTION = "ParBijFunc";
public static final String PARITAL_BIJECTIVE_FUNCTION_ELEMENT_OF = "ParBijFuncEleOf";
-
+
// Relations
public static final String RELATIONS = "Relations";
public static final String REL_DOMAIN = "RelDomain";
@@ -107,6 +109,21 @@ public final class StandardMadules {
public static final String REL_PARTIAL_BIJECTIVE_FUNCTION = "RelParBijFunc";
public static final String REL_PARTIAL_BIJECTIVE_FUNCTION_ELEMENT_OF = "RelParBijFuncEleOf";
+ private final static Set<String> SequencesKeywords = new HashSet<String>();
+ static {
+ SequencesKeywords.add("Seq");
+ SequencesKeywords.add("Len");
+ SequencesKeywords.add("Append");
+ SequencesKeywords.add("Head");
+ SequencesKeywords.add("Tail");
+ SequencesKeywords.add("Subseq");
+ SequencesKeywords.add("SelectSeq");
+ }
+
+ public final static boolean isKeywordInModuleSequences(String name) {
+ return SequencesKeywords.contains(name);
+ }
+
// SequencesExtended
public static final String SEQUENCE_LAST_ELEMENT = "Last";
public static final String SEQUENCE_PREPEND_ELEMENT = "Prepend";
@@ -122,7 +139,7 @@ public final class StandardMadules {
public static final String SEQUENCE_TAKE_FIRST_ELEMENTS = "TakeFirstElements";
public static final String SEQUENCE_DROP_FIRST_ELEMENTS = "DropFirstElements";
- public final static Set<String> SequencesExtendedKeywords = new HashSet<String>();
+ private final static Set<String> SequencesExtendedKeywords = new HashSet<String>();
static {
SequencesExtendedKeywords.add(SEQUENCE_LAST_ELEMENT);
SequencesExtendedKeywords.add(SEQUENCE_PREPEND_ELEMENT);
@@ -138,7 +155,11 @@ public final class StandardMadules {
SequencesExtendedKeywords.add(SEQUENCE_TAKE_FIRST_ELEMENTS);
SequencesExtendedKeywords.add(SEQUENCE_DROP_FIRST_ELEMENTS);
}
-
+
+ public final static boolean isKeywordInModuleSequencesExtended(String name) {
+ return SequencesExtendedKeywords.contains(name);
+ }
+
// SequencesAsRelations
public static final String REL_SEQUENCE_SIZE = "RelSeqSize";
public static final String IS_REL_SEQUENCE = "isRelSeq";
@@ -179,8 +200,7 @@ public final class StandardMadules {
public static final String GENERAL_SUMMATION = "Sigma";
public static final String GENERAL_PRODUCT = "Pi";
- public static final ArrayList<String> Relations = new ArrayList<String>();
-
+ private static final ArrayList<String> Relations = new ArrayList<String>();
static {
Relations.add(RELATIONS);
Relations.add(REL_DOMAIN);
@@ -205,4 +225,8 @@ public final class StandardMadules {
}
+ public static final boolean containsNameFromModuleRelations(String name) {
+ return Relations.contains(name);
+ }
+
}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index e186d6f..fce8f87 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -106,7 +106,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression e = (PExpression) id;
HashSet<PExpression> set = new HashSet<PExpression>();
set.add(e);
- createRestrictedTypeofLocalVariables(set);
+ createRestrictedTypeofLocalVariables(set, true);
} else if (ltlNode instanceof AForallLtl) {
Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode)
.getForallIdentifier().getText());
@@ -117,7 +117,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression e = (PExpression) id;
HashSet<PExpression> set = new HashSet<PExpression>();
set.add(e);
- createRestrictedTypeofLocalVariables(set);
+ createRestrictedTypeofLocalVariables(set, true);
}
bNode.apply(this);
}
@@ -162,7 +162,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (Node param : list) {
set.add((PExpression) param);
}
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set), false);
}
@Override
@@ -175,7 +175,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (Node con : machineContext.getConstants().values()) {
set.add((PExpression) con);
}
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set), false);
}
public void analyseDisjunktionPredicate(PPredicate node, HashSet<Node> list) {
@@ -344,7 +344,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
.getImplication();
analysePredicate(implication.getLeft(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -357,7 +357,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -370,7 +370,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -384,7 +384,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -397,7 +397,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -410,7 +410,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -422,7 +422,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -434,7 +434,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
private Hashtable<Node, HashSet<PExpression>> expectedIdentifieListTable = new Hashtable<Node, HashSet<PExpression>>();
@@ -461,7 +461,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (node.getOperationBody() != null) {
node.getOperationBody().apply(this);
}
- createRestrictedTypeofLocalVariables(list);
+ createRestrictedTypeofLocalVariables(list, false);
}
@Override
@@ -494,7 +494,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getWhere(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
@Override
@@ -508,7 +508,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
- node.getIdentifiers()));
+ node.getIdentifiers()), false);
}
private Hashtable<Node, Node> variablesHashTable;
@@ -527,11 +527,15 @@ public class TypeRestrictor extends DepthFirstAdapter {
variablesHashTable.put(ref, e);
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(copy));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(copy), false);
}
}
- private void createRestrictedTypeofLocalVariables(Set<PExpression> copy) {
+ private void createRestrictedTypeofLocalVariables(Set<PExpression> copy, boolean constant) {
+ //TODO if constant is true, only constant expressions should be used to restrict the type.
+ //This is required by the TLC model checker when checking an LTL formula.
+
+
for (PExpression e : copy) {
PExpression tree = null;
ArrayList<Node> restrictedList = restrictedNodeTable.get(e);
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index a559e31..100ce21 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -4,6 +4,7 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashMap;
+import java.util.Map.Entry;
import java.util.Set;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -43,14 +44,15 @@ public class StructType extends AbstractHasFollowers {
public String toString() {
StringBuffer res = new StringBuffer();
res.append("struct(");
-
- Iterator<String> keys = types.keySet().iterator();
- if (!keys.hasNext())
+
+ Iterator<Entry<String, BType>> iterator = types.entrySet().iterator();
+ if (!iterator.hasNext())
res.append("...");
- while (keys.hasNext()) {
- String fieldName = (String) keys.next();
- res.append(fieldName + ":" + types.get(fieldName));
- if (keys.hasNext())
+ while (iterator.hasNext()) {
+ Entry<String, BType> next = iterator.next();
+ String fieldName = (String) next.getKey();
+ res.append(fieldName).append(":").append(next.getValue());
+ if (iterator.hasNext())
res.append(",");
}
res.append(")");
@@ -58,16 +60,19 @@ public class StructType extends AbstractHasFollowers {
}
public void update(BType oldType, BType newType) {
- Iterator<String> itr = this.types.keySet().iterator();
- while (itr.hasNext()) {
- String name = itr.next();
- BType t = this.types.get(name);
- if (t == oldType) {
+ Iterator<Entry<String, BType>> iterator = this.types.entrySet()
+ .iterator();
+ while (iterator.hasNext()) {
+ Entry<String, BType> next = iterator.next();
+ String name = next.getKey();
+ BType type = next.getValue();
+ if (type == oldType) {
this.types.put(name, newType);
if (newType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) newType).addFollower(this);
}
}
+
}
}
@@ -81,10 +86,13 @@ public class StructType extends AbstractHasFollowers {
}
if (other instanceof StructType) {
StructType s = (StructType) other;
- Iterator<String> itr = s.types.keySet().iterator();
- while (itr.hasNext()) {
- String fieldName = (String) itr.next();
- BType sType = s.types.get(fieldName);
+
+ Iterator<Entry<String, BType>> iterator = s.types.entrySet()
+ .iterator();
+ while (iterator.hasNext()) {
+ Entry<String, BType> next = iterator.next();
+ String fieldName = next.getKey();
+ BType sType = next.getValue();
if (this.types.containsKey(fieldName)) {
BType res = this.types.get(fieldName).unify(sType,
typechecker);
@@ -104,9 +112,9 @@ public class StructType extends AbstractHasFollowers {
}
public boolean isUntyped() {
- Iterator<String> itr = types.keySet().iterator();
- while (itr.hasNext()) {
- if (this.types.get(itr.next()).isUntyped()) {
+ Iterator<BType> iterator = types.values().iterator();
+ while (iterator.hasNext()) {
+ if (iterator.next().isUntyped()) {
return true;
}
}
@@ -142,10 +150,13 @@ public class StructType extends AbstractHasFollowers {
return false;
}
}
- Iterator<String> itr2 = types.keySet().iterator();
- while (itr2.hasNext()) {
- String name = itr2.next();
- if (!this.types.get(name).compare(s.types.get(name))) {
+ Iterator<Entry<String, BType>> iterator = types.entrySet()
+ .iterator();
+ while (iterator.hasNext()) {
+ Entry<String, BType> next = iterator.next();
+ String name = next.getKey();
+ BType value = next.getValue();
+ if (!this.types.get(name).compare(value)) {
return false;
}
}
@@ -174,14 +185,20 @@ public class StructType extends AbstractHasFollowers {
public String getTlaType() {
StringBuffer res = new StringBuffer();
res.append("[");
- Iterator<String> keys = types.keySet().iterator();
- if (!keys.hasNext())
+ Iterator<Entry<String, BType>> iterator = types.entrySet().iterator();
+ if (!iterator.hasNext()) {
res.append("...");
- while (keys.hasNext()) {
- String fieldName = (String) keys.next();
- res.append(fieldName + ":" + types.get(fieldName));
- if (keys.hasNext())
- res.append(",");
+ } else {
+ while (iterator.hasNext()) {
+ Entry<String, BType> next = iterator.next();
+ String fieldName = next.getKey();
+ BType type = next.getValue();
+ res.append(fieldName);
+ res.append(":");
+ res.append(type);
+ if (iterator.hasNext())
+ res.append(",");
+ }
}
res.append("]");
return res.toString();
@@ -198,14 +215,18 @@ public class StructType extends AbstractHasFollowers {
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
ArrayList<PRecEntry> list = new ArrayList<PRecEntry>();
- for (String name : types.keySet()) {
+
+ Set<Entry<String, BType>> entrySet = this.types.entrySet();
+ for (Entry<String, BType> entry : entrySet) {
+ String name = entry.getKey();
+ BType type = entry.getValue();
TIdentifierLiteral literal = new TIdentifierLiteral(name);
ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
idList.add(literal);
AIdentifierExpression id = new AIdentifierExpression(idList);
- ARecEntry entry = new ARecEntry(id, types.get(name)
- .createSyntaxTreeNode(typechecker));
- list.add(entry);
+ ARecEntry recEntry = new ARecEntry(id,
+ type.createSyntaxTreeNode(typechecker));
+ list.add(recEntry);
}
AStructExpression node = new AStructExpression(list);
typechecker.setType(node, new SetType(this));
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index acf0f04..85fdd34 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -144,10 +144,10 @@ public class TLAPrinter extends DepthFirstAdapter {
}
public void printStrongFairness(String s) {
-
+
moduleStringAppend(String
- .format("([]<><<%s>>_vars \\/ <>[]~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
- s, s, s));
+ .format("([]<><<%s>>_vars \\/ <>[]~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ s, s, s));
printVarsStuttering();
moduleStringAppend("))");
@@ -155,8 +155,8 @@ public class TLAPrinter extends DepthFirstAdapter {
public void printWeakFairness(String s) {
moduleStringAppend(String
- .format("([]<><<%s>>_vars \\/ []<>~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
- s, s, s));
+ .format("([]<><<%s>>_vars \\/ []<>~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ s, s, s));
printVarsStuttering();
moduleStringAppend("))");
@@ -275,20 +275,13 @@ public class TLAPrinter extends DepthFirstAdapter {
configFileString.append("Init_action = Init_action\n");
ArrayList<POperation> operations = tlaModule.getOperations();
- StringBuilder sb = new StringBuilder();
- sb.append("{");
for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node);
configFileString.append(name + "_action = ");
configFileString.append(name + "_action");
configFileString.append("\n");
- sb.append(name + "_action");
- if (i < operations.size() - 1) {
- sb.append(", ");
- }
}
- sb.append("}");
configFileString.append("\n");
configFileString.append("VIEW myView");
}
@@ -2909,7 +2902,7 @@ public class TLAPrinter extends DepthFirstAdapter {
return this.translatedLTLFormula.toString();
}
- public TLAModule getTLAModule(){
+ public TLAModule getTLAModule() {
return this.tlaModule;
}
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index cdabda9..e1a1c40 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -8,6 +8,7 @@ import java.util.Map.Entry;
import java.util.Set;
import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.exceptions.NotSupportedException;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
@@ -114,7 +115,7 @@ public class TLCResults implements ToolGlobals {
lineCount.put(endline, entry.getValue());
}
}
- ArrayList<OpDefNode> defs = findOperations(OutputCollector.moduleNode);
+ ArrayList<OpDefNode> defs = getActionsFromGeneratedModule(OutputCollector.moduleNode);
operationsCount = new LinkedHashMap<String, Long>();
for (OpDefNode opDefNode : defs) {
String operationName = opDefNode.getName().toString();
@@ -126,36 +127,52 @@ public class TLCResults implements ToolGlobals {
}
}
- private ArrayList<OpDefNode> findOperations(ModuleNode moduleNode) {
+ private ArrayList<OpDefNode> getActionsFromGeneratedModule(
+ ModuleNode moduleNode) {
+ // list of actions in the module
+ ArrayList<OpDefNode> actions = new ArrayList<OpDefNode>();
+ // get all definitions from the module
OpDefNode[] opDefs = moduleNode.getOpDefs();
+
+ // search for the definition with the name "Next"
ExprNode pred = null;
for (int i = opDefs.length - 1; i > 0; i--) {
+ // start the search from the end because "Next" is usually the last
+ // definition in the module
OpDefNode def = opDefs[i];
if (def.getName().toString().equals("Next")) {
pred = def.getBody();
break;
}
}
+
+ if (pred == null) {
+ // this is the case if there aren't any actions in the module and
+ // consequently there is no "Next" definition
+ return actions;
+ }
OpApplNode dis = (OpApplNode) pred;
- ArrayList<OpDefNode> operations = new ArrayList<OpDefNode>();
for (int i = 0; i < dis.getArgs().length; i++) {
- operations.add(findOperation(dis.getArgs()[i]));
+ actions.add(findAction(dis.getArgs()[i]));
}
- return operations;
+ return actions;
}
- private OpDefNode findOperation(ExprOrOpArgNode arg) {
+ private OpDefNode findAction(ExprOrOpArgNode arg) {
OpApplNode op1 = (OpApplNode) arg;
SymbolNode opNode = op1.getOperator();
int opcode = BuiltInOPs.getOpCode(opNode.getName());
if (opcode == OPCODE_be) { // BoundedExists
- return findOperation(op1.getArgs()[0]);
+ return findAction(op1.getArgs()[0]);
} else if (opNode instanceof OpDefNode) {
OpDefNode def = (OpDefNode) opNode;
return def;
} else {
- throw new RuntimeException("Unkown Node");
+ throw new NotSupportedException(
+ "Can not find action in next state relation. Unkown node: "
+ + opNode.getClass());
+
}
}
@@ -298,8 +315,6 @@ public class TLCResults implements ToolGlobals {
}
private TLCResult evaluatingParameter(String[] params) {
- System.out.println(params.length);
- System.out.println(params[0]);
for (int i = 0; i < params.length; i++) {
String s = params[i];
if (s.contains("not enumerable")) {
diff --git a/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java b/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
index 6b378ad..9614e6f 100644
--- a/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
+++ b/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
@@ -40,6 +40,7 @@ public class IntegrationCoverageTest extends AbstractParseMachineTest {
ignoreList.add("./src/test/resources/test/");
ignoreList.add("./src/test/resources/testing/");
ignoreList.add("./src/test/resources/todo/");
+ ignoreList.add("./src/test/resources/bugs/");
return getConfiguration2(list, ignoreList);
}
diff --git a/src/test/java/de/tlc4b/tlc/integration/BugTest.java b/src/test/java/de/tlc4b/tlc/integration/BugTest.java
deleted file mode 100644
index ec2655e..0000000
--- a/src/test/java/de/tlc4b/tlc/integration/BugTest.java
+++ /dev/null
@@ -1,15 +0,0 @@
-package de.tlc4b.tlc.integration;
-
-import org.junit.Test;
-
-import de.tlc4b.TLC4B;
-
-public class BugTest {
-
- @Test
- public void testTraceValues() {
- String[] a = new String[] { "./src/test/resources/bugs/LTLParseError.mch" };
- TLC4B.main(a);
- }
-
-}
\ No newline at end of file
--
GitLab