From 7db1656d32fdcc6f54eb7c7343295b8709aa8e17 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 1 Aug 2013 10:25:31 +0200
Subject: [PATCH] Bug fix
---
.../b2tla/analysis/DefinitionsAnalyser.java | 75 ++++++++++++++-----
.../transformation/DefinitionsEliminator.java | 2 +-
src/main/java/de/b2tla/btypes/BType.java | 3 +-
src/main/java/de/b2tla/btypes/BoolType.java | 7 +-
.../java/de/b2tla/btypes/FunctionType.java | 11 ++-
.../b2tla/btypes/IntegerOrSetOfPairType.java | 3 +-
.../de/b2tla/btypes/IntegerOrSetType.java | 3 +-
.../java/de/b2tla/btypes/IntegerType.java | 7 +-
.../java/de/b2tla/btypes/ModelValueType.java | 4 +-
src/main/java/de/b2tla/btypes/PairType.java | 11 ++-
src/main/java/de/b2tla/btypes/SetType.java | 7 +-
src/main/java/de/b2tla/btypes/StringType.java | 7 +-
src/main/java/de/b2tla/btypes/StructType.java | 9 ++-
.../java/de/b2tla/btypes/UntypedType.java | 3 +-
.../java/de/b2tla/prettyprint/TLAPrinter.java | 4 +-
src/main/java/de/b2tla/tla/Generator.java | 26 ++++---
.../probprivate/AssertionErrorTest.java | 2 +-
.../tlc/integration/probprivate/GoalTest.java | 10 +--
18 files changed, 131 insertions(+), 63 deletions(-)
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
index 4b2d2a3..8519693 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
@@ -4,6 +4,7 @@ import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;
+import de.b2tla.B2TLAGlobals;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
@@ -18,10 +19,10 @@ import de.be4.classicalb.core.parser.node.Node;
*
*
* @author hansen
- *
+ *
*/
-public class DefinitionsAnalyser extends DepthFirstAdapter{
+public class DefinitionsAnalyser extends DepthFirstAdapter {
private MachineContext machineContext;
private HashMap<Node, Integer> deferredSetSizeTable;
@@ -34,50 +35,86 @@ public class DefinitionsAnalyser extends DepthFirstAdapter{
deferredSetSizeTable = new HashMap<Node, Integer>();
HashSet<Node> deferredSets = new HashSet<Node>(machineContext
.getDeferredSets().values());
+
+ findMaxMin();
+
if (deferredSets.size() == 0)
return;
Set<String> strings = machineContext.getDeferredSets().keySet();
for (String string : strings) {
- String s = "scope_"+ string;
+ String s = "scope_" + string;
Node node = machineContext.getDefinitions().get(s);
- if(null != node){
+ if (null != node) {
try {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
- AIntervalExpression interval = (AIntervalExpression) d.getRhs();
- AIntegerExpression left = (AIntegerExpression) interval.getLeftBorder();
- AIntegerExpression right = (AIntegerExpression) interval.getRightBorder();
+ AIntervalExpression interval = (AIntervalExpression) d
+ .getRhs();
+ AIntegerExpression left = (AIntegerExpression) interval
+ .getLeftBorder();
+ AIntegerExpression right = (AIntegerExpression) interval
+ .getRightBorder();
int l_int = Integer.parseInt(left.getLiteral().getText());
int r_int = Integer.parseInt(right.getLiteral().getText());
int size = r_int - l_int + 1;
- deferredSetSizeTable.put(machineContext.getDeferredSets().get(string), size);
+ deferredSetSizeTable.put(machineContext.getDeferredSets()
+ .get(string), size);
} catch (ClassCastException e) {
}
try {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
- AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
- int size = Integer.parseInt(sizeExpr.getLiteral().getText());
- deferredSetSizeTable.put(machineContext.getDeferredSets().get(string), size);
+ AIntegerExpression sizeExpr = (AIntegerExpression) d
+ .getRhs();
+ int size = Integer
+ .parseInt(sizeExpr.getLiteral().getText());
+ deferredSetSizeTable.put(machineContext.getDeferredSets()
+ .get(string), size);
} catch (ClassCastException e) {
}
-
-
+
+ }
+ }
+ }
+
+ private void findMaxMin() {
+ Node node = machineContext.getDefinitions().get("SET_PREF_MAXINT");
+ if (null != node) {
+ try {
+ AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
+ AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
+ int value = Integer.parseInt(sizeExpr.getLiteral().getText());
+ B2TLAGlobals.setMAX_INT(value);
+ } catch (ClassCastException e) {
+
+ }
+ }
+
+ node = machineContext.getDefinitions().get("SET_PREF_MININT");
+ if (null != node) {
+ try {
+ AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
+ AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
+ int value = Integer.parseInt(sizeExpr.getLiteral().getText());
+ B2TLAGlobals.setMIN_INT(value);
+ } catch (ClassCastException e) {
+
}
}
}
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- //TODO never reached
+ // TODO never reached
Node ref_node = machineContext.getReferences().get(node);
- if(deferredSetSizeTable.containsKey(ref_node)){
+ if (deferredSetSizeTable.containsKey(ref_node)) {
try {
ACardExpression cardNode = (ACardExpression) node.parent();
- AEqualPredicate equalsNode = (AEqualPredicate) cardNode.parent();
+ AEqualPredicate equalsNode = (AEqualPredicate) cardNode
+ .parent();
AIntegerExpression integer;
- if(equalsNode.getLeft() == cardNode){
+ if (equalsNode.getLeft() == cardNode) {
integer = (AIntegerExpression) equalsNode.getRight();
- }else{
+ } else {
integer = (AIntegerExpression) equalsNode.getLeft();
}
String intString = integer.getLiteral().getText();
@@ -85,7 +122,7 @@ public class DefinitionsAnalyser extends DepthFirstAdapter{
} catch (ClassCastException e) {
return;
}
-
+
}
}
}
diff --git a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
index 7ae55d2..18fb1bf 100644
--- a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
@@ -68,7 +68,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
if (e instanceof AExpressionDefinitionDefinition) {
String name = ((AExpressionDefinitionDefinition) e).getName()
.getText().toString();
- if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_"))
+ if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")|| name.startsWith("SET_PREF_"))
continue;
} else if (e instanceof APredicateDefinitionDefinition) {
String name = ((APredicateDefinitionDefinition) e).getName().getText().toString();
diff --git a/src/main/java/de/b2tla/btypes/BType.java b/src/main/java/de/b2tla/btypes/BType.java
index 5043fab..af611ff 100644
--- a/src/main/java/de/b2tla/btypes/BType.java
+++ b/src/main/java/de/b2tla/btypes/BType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.be4.classicalb.core.parser.node.PExpression;
public interface BType extends ITypeConstants{
@@ -8,5 +9,5 @@ public interface BType extends ITypeConstants{
public boolean compare(BType other);
public String getTlaType();
public boolean containsIntegerType();
- public PExpression createSyntaxTreeNode();
+ public PExpression createSyntaxTreeNode(Typechecker typechecker);
}
diff --git a/src/main/java/de/b2tla/btypes/BoolType.java b/src/main/java/de/b2tla/btypes/BoolType.java
index ae65354..64cba26 100644
--- a/src/main/java/de/b2tla/btypes/BoolType.java
+++ b/src/main/java/de/b2tla/btypes/BoolType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ABoolSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -50,8 +51,10 @@ public class BoolType implements BType {
return false;
}
- public PExpression createSyntaxTreeNode() {
- return new ABoolSetExpression();
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ ABoolSetExpression node = new ABoolSetExpression();
+ typechecker.setType(node, new SetType(this));
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/FunctionType.java b/src/main/java/de/b2tla/btypes/FunctionType.java
index 6624b2e..e3333fc 100644
--- a/src/main/java/de/b2tla/btypes/FunctionType.java
+++ b/src/main/java/de/b2tla/btypes/FunctionType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -127,9 +128,13 @@ public class FunctionType extends AbstractHasFollowers {
|| this.range.containsIntegerType();
}
- public PExpression createSyntaxTreeNode() {
- return new ATotalFunctionExpression(domain.createSyntaxTreeNode(),
- range.createSyntaxTreeNode());
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ ATotalFunctionExpression node = new ATotalFunctionExpression(
+ domain.createSyntaxTreeNode(typechecker),
+ range.createSyntaxTreeNode(typechecker));
+ typechecker.setType(node, new SetType(this));
+
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
index 44a872f..c7a17bd 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.TypeErrorException;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -230,7 +231,7 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode() {
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
return null;
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java b/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
index 6a8fe02..cbc286a 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -62,7 +63,7 @@ public class IntegerOrSetType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode() {
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
return null;
}
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerType.java b/src/main/java/de/b2tla/btypes/IntegerType.java
index 00b9e69..3cda971 100644
--- a/src/main/java/de/b2tla/btypes/IntegerType.java
+++ b/src/main/java/de/b2tla/btypes/IntegerType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
@@ -60,7 +61,9 @@ public class IntegerType implements BType {
return true;
}
- public PExpression createSyntaxTreeNode() {
- return new AIntegerSetExpression();
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ AIntegerSetExpression node = new AIntegerSetExpression();
+ typechecker.setType(node, new SetType(this));
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/ModelValueType.java b/src/main/java/de/b2tla/btypes/ModelValueType.java
index 523b7da..c5eb10a 100644
--- a/src/main/java/de/b2tla/btypes/ModelValueType.java
+++ b/src/main/java/de/b2tla/btypes/ModelValueType.java
@@ -2,6 +2,7 @@ package de.b2tla.btypes;
import java.util.ArrayList;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -64,11 +65,12 @@ public class ModelValueType implements BType {
return false;
}
- public PExpression createSyntaxTreeNode() {
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
TIdentifierLiteral literal = new TIdentifierLiteral(name);
ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
idList.add(literal);
AIdentifierExpression id = new AIdentifierExpression(idList);
+ typechecker.setType(id, new SetType(this));
return id;
}
}
diff --git a/src/main/java/de/b2tla/btypes/PairType.java b/src/main/java/de/b2tla/btypes/PairType.java
index eebed18..6f02747 100644
--- a/src/main/java/de/b2tla/btypes/PairType.java
+++ b/src/main/java/de/b2tla/btypes/PairType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ACartesianProductExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -122,9 +123,11 @@ public class PairType extends AbstractHasFollowers {
|| this.second.containsIntegerType();
}
- public PExpression createSyntaxTreeNode() {
- return new ACartesianProductExpression(first.createSyntaxTreeNode(),
- second.createSyntaxTreeNode());
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ ACartesianProductExpression node = new ACartesianProductExpression(
+ first.createSyntaxTreeNode(typechecker),
+ second.createSyntaxTreeNode(typechecker));
+ typechecker.setType(node, new SetType(this));
+ return node;
}
-
}
diff --git a/src/main/java/de/b2tla/btypes/SetType.java b/src/main/java/de/b2tla/btypes/SetType.java
index 98d0046..04d84de 100644
--- a/src/main/java/de/b2tla/btypes/SetType.java
+++ b/src/main/java/de/b2tla/btypes/SetType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -97,8 +98,10 @@ public class SetType extends AbstractHasFollowers {
return this.subtype.containsIntegerType();
}
- public PExpression createSyntaxTreeNode() {
- return new APowSubsetExpression(subtype.createSyntaxTreeNode());
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ APowSubsetExpression node = new APowSubsetExpression(subtype.createSyntaxTreeNode(typechecker));
+ typechecker.setType(node, this);
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/StringType.java b/src/main/java/de/b2tla/btypes/StringType.java
index 961c4a6..74cf5db 100644
--- a/src/main/java/de/b2tla/btypes/StringType.java
+++ b/src/main/java/de/b2tla/btypes/StringType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -55,8 +56,10 @@ public class StringType implements BType {
return false;
}
- public PExpression createSyntaxTreeNode() {
- return new AStringSetExpression();
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ AStringSetExpression node = new AStringSetExpression();
+ typechecker.setType(node, new SetType(this));
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/StructType.java b/src/main/java/de/b2tla/btypes/StructType.java
index 56b88f6..d4cbdfa 100644
--- a/src/main/java/de/b2tla/btypes/StructType.java
+++ b/src/main/java/de/b2tla/btypes/StructType.java
@@ -6,6 +6,7 @@ import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Set;
+import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ARecEntry;
@@ -192,7 +193,7 @@ public class StructType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode() {
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
ArrayList<PRecEntry> list = new ArrayList<PRecEntry>();
for (String name : types.keySet()) {
TIdentifierLiteral literal = new TIdentifierLiteral(name);
@@ -200,10 +201,12 @@ public class StructType extends AbstractHasFollowers {
idList.add(literal);
AIdentifierExpression id = new AIdentifierExpression(idList);
ARecEntry entry = new ARecEntry(id, types.get(name)
- .createSyntaxTreeNode());
+ .createSyntaxTreeNode(typechecker));
list.add(entry);
}
- return new AStructExpression(list);
+ AStructExpression node = new AStructExpression(list);
+ typechecker.setType(node, new SetType(this));
+ return node;
}
}
diff --git a/src/main/java/de/b2tla/btypes/UntypedType.java b/src/main/java/de/b2tla/btypes/UntypedType.java
index 4ecd78b..808d6b5 100644
--- a/src/main/java/de/b2tla/btypes/UntypedType.java
+++ b/src/main/java/de/b2tla/btypes/UntypedType.java
@@ -1,5 +1,6 @@
package de.b2tla.btypes;
+import de.b2tla.analysis.Typechecker;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -31,7 +32,7 @@ public class UntypedType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode() {
+ public PExpression createSyntaxTreeNode(Typechecker typechecker) {
return null;
}
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index be5c79b..bc9e722 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -1591,11 +1591,9 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseATotalFunctionExpression(ATotalFunctionExpression node) {
BType type = this.typechecker.getType(node);
- if(type == null){
- type = new SetType(new FunctionType(new UntypedType(), new UntypedType()));
- }
BType subtype = ((SetType) type).getSubtype();
if (subtype instanceof FunctionType) {
+ System.out.println(node.getLeft().getClass());
tlaModuleString.append("[");
node.getLeft().apply(this);
tlaModuleString.append(" -> ");
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index 083dfc9..cb07974 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -15,6 +15,7 @@ import de.b2tla.analysis.TypeRestrictor;
import de.b2tla.analysis.Typechecker;
import de.b2tla.analysis.nodes.NodeType;
import de.b2tla.btypes.BType;
+import de.b2tla.btypes.SetType;
import de.b2tla.tla.config.ModelValueAssignment;
import de.b2tla.tla.config.SetOfModelValuesAssignment;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
@@ -259,18 +260,21 @@ public class Generator extends DepthFirstAdapter {
if (value == null) {
init = true;
this.tlaModule.variables.add(con);
- BType type = typechecker.getType(con);
-
- PExpression n = type.createSyntaxTreeNode();
- AMemberPredicate member = new AMemberPredicate(
- (PExpression) con.clone(), n);
-
- ArrayList<NodeType> list = this.typeRestrictor
- .getRestrictedTypesSet(con);
- if (list == null || list.size() == 0) {
- tlaModule.addInit(member);
- } else {
+ BType conType = typechecker.getType(con);
+ if (!conType.containsIntegerType()) {
+ PExpression n = conType
+ .createSyntaxTreeNode(typechecker);
+ AMemberPredicate member = new AMemberPredicate(
+ (PExpression) con.clone(), n);
+
+ ArrayList<NodeType> list = this.typeRestrictor
+ .getRestrictedTypesSet(con);
+ if (list == null || list.size() == 0) {
+ tlaModule.addInit(member);
+ } else {
+
+ }
}
} else {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
index ae6a348..f2ced2c 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
@@ -31,7 +31,7 @@ public class AssertionErrorTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a, false));
+ assertEquals(error, B2TLA.test(a, true));
}
@Config
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
index 0eee8c4..0249ef0 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
@@ -17,9 +17,8 @@ import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
-public class GoalTest extends AbstractParseMachineTest{
+public class GoalTest extends AbstractParseMachineTest {
-
private final File machine;
private final TLCResult error;
@@ -30,14 +29,15 @@ public class GoalTest extends AbstractParseMachineTest{
@Test
public void testRunTLC() throws Exception {
- String[] a = new String[] { machine.getPath()};
- assertEquals(error, B2TLA.test(a,false));
+ String[] a = new String[] { machine.getPath() };
+ assertEquals(error, B2TLA.test(a, true));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
- list.add(new TestPair(TLCResult.Goal, "../probprivate/public_examples/TLC/GOAL"));
+ list.add(new TestPair(TLCResult.Goal,
+ "../probprivate/public_examples/TLC/GOAL"));
return getConfiguration(list);
}
}
--
GitLab