diff --git a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java index 4b2d2a35b8f872be7ff239e7647989f110a68b1e..8519693b69c0e6c23106d3037cba636114c11c6e 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 7ae55d2c6104323961633a3f8d888108b3889d78..18fb1bfb6569f3ea761a5ce2b93c7d0ed3cacea5 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 5043fab19a7c28d6ade3c4ea2ab2729de1c70234..af611ff221e9ff17b9e0c381bb872108cc3f0595 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 ae65354c5b831a99648e7666f7845e8179063c25..64cba2652f67ad68fc83a1fbbc28d7bde0bfdf3e 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 6624b2e05a4d63f0d6435b3c4eefe9bc3cbdcfaa..e3333fc87ee7d014e6431ec1acb1d9257f41cdbb 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 44a872f7f3fe4b703eca9d23e8c86140c53543b0..c7a17bd8ec8bab7de0432d52f7f5b5871fc603de 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 6a8fe02e4572f70d8aef030caa8a0875c88a7b80..cbc286ac6b128d851f7a3f75d6b7fc2e2b72c140 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 00b9e695f48a3c8dae32b94c5c537223543ad1d2..3cda971e9996a6b208048502ed779c91519abe90 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 523b7dabcfda35362435143b005aae5826daac6a..c5eb10a4765e97c2221f5fb0ef2bbb986e16c0f9 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 eebed18c6a19692fb24b54c589e29452cd566879..6f0274770dac65ee0a16dbeb1f9f4eab73af146f 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 98d0046d1285aab5d314acf100a08479ac37f77f..04d84de70ec69b0cd30c5653f41300ece3720efd 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 961c4a6ee7c612cce08c2a040ab4babcf825d0cb..74cf5dba25ec11ce66fe97b2a65e4ba9bbdd5bf0 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 56b88f6c711079bf3b20bb7a5d3a071933c7a887..d4cbdfa5c40770d877f422e581ec4ca26650b83c 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 4ecd78beb0fa09903d29199af1d6448e2acc9a54..808d6b5796eaa8fd5348027f3ffa3e7cc1586b74 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 be5c79b119d8c9580146e6810f5bda62cc3fb26f..bc9e722acf1a2361cf035d0a08efd621ca0abbea 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 083dfc99fe94057bb81e29f2e0d27315be9103ea..cb079745b98e0fe0ee3e8ffcd4b16f9543632032 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 ae6a3480d3f3a8334bb1bdb5cc94f53d6399723c..f2ced2cb3896ad678243b02af65bdb63e7674eb5 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 0eee8c4fd861b1b92c10560225146eda374315de..0249ef0af74d8094be5ee927b7841c787ede355b 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); } }