Skip to content
Snippets Groups Projects
Commit 7db1656d authored by hansen's avatar hansen
Browse files

Bug fix

parent 1519ab96
No related branches found
No related tags found
No related merge requests found
Showing
with 131 additions and 63 deletions
......@@ -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;
......@@ -34,6 +35,9 @@ 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;
......@@ -44,23 +48,55 @@ public class DefinitionsAnalyser extends DepthFirstAdapter{
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);
} 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 size = Integer.parseInt(sizeExpr.getLiteral().getText());
deferredSetSizeTable.put(machineContext.getDeferredSets().get(string), size);
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) {
}
}
......@@ -73,7 +109,8 @@ public class DefinitionsAnalyser extends DepthFirstAdapter{
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) {
integer = (AIntegerExpression) equalsNode.getRight();
......
......@@ -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();
......
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);
}
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;
}
}
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;
}
}
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;
}
......
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;
}
}
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;
}
}
......@@ -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;
}
}
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;
}
}
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;
}
}
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;
}
}
......@@ -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;
}
}
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;
}
......
......@@ -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(" -> ");
......
......@@ -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,9 +260,11 @@ public class Generator extends DepthFirstAdapter {
if (value == null) {
init = true;
this.tlaModule.variables.add(con);
BType type = typechecker.getType(con);
BType conType = typechecker.getType(con);
PExpression n = type.createSyntaxTreeNode();
if (!conType.containsIntegerType()) {
PExpression n = conType
.createSyntaxTreeNode(typechecker);
AMemberPredicate member = new AMemberPredicate(
(PExpression) con.clone(), n);
......@@ -272,6 +275,7 @@ public class Generator extends DepthFirstAdapter {
} else {
}
}
} else {
tlaModule.definitions.add(new TLADefinition(con, value));
......
......@@ -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
......
......@@ -19,7 +19,6 @@ import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class GoalTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
......@@ -31,13 +30,14 @@ public class GoalTest 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
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);
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment