diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index f27b3a2ce47e34d7f268886a3a851bdbbf4bd607..c7a1c1c18c1536d098d48048994ad7d1291eee48 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -94,15 +94,15 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(g));
}
- ArrayList<PExpression> left = new ArrayList<PExpression>();
- ArrayList<PExpression> right = new ArrayList<PExpression>();
+ ArrayList<PExpression> leftSideOfAssigment = new ArrayList<PExpression>();
+ ArrayList<PExpression> rightSideOfAssigment = new ArrayList<PExpression>();
for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
- left.add(bASTCreator.createIdentifierNode(entry.getKey()));
- right.add(bASTCreator.visitExprOrOpArgNodeExpression(entry
- .getValue()));
+ leftSideOfAssigment.add(bASTCreator.createIdentifierNode(entry
+ .getKey()));
+ rightSideOfAssigment.add(bASTCreator
+ .visitExprOrOpArgNodeExpression(entry.getValue()));
}
AAssignSubstitution assign = new AAssignSubstitution();
-
if (anyVariables.size() > 0) { // ANY x_n WHERE P THEN A END
AAnySubstitution any = new AAnySubstitution();
any = new AAnySubstitution();
@@ -117,8 +117,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
TLAType t = (TLAType) var.getToolObject(TYPE_ID);
member.setRight(t.getBNode());
whereList.add(member);
- left.add(bASTCreator.createIdentifierNode(var));
- right.add(BAstCreator.createIdentifierNode(nextName));
+ leftSideOfAssigment.add(bASTCreator.createIdentifierNode(var));
+ rightSideOfAssigment.add(BAstCreator
+ .createIdentifierNode(nextName));
+
}
any.setIdentifiers(anyParams);
whereList.addAll(createBeforeAfterPredicates(bASTCreator));
@@ -139,9 +141,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
operation.setOperationBody(block);
}
- if (left.size() > 0) {
- assign.setLhsExpression(left);
- assign.setRhsExpressions(right);
+ if (leftSideOfAssigment.size() > 0) {
+ assign.setLhsExpression(leftSideOfAssigment);
+ assign.setRhsExpressions(rightSideOfAssigment);
} else { // skip
assign.replaceBy(new ASkipSubstitution());
}
@@ -220,6 +222,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
// anyVariables.add((OpDeclNode) symbol);
// }
anyVariables.removeAll(assignments.keySet());
+ anyVariables.removeAll(unchangedVariablesList);
}
private void separateGuardsAndBeforeAfterPredicates(ExprOrOpArgNode node) {
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 6fa75ccdccf48dae3b5669b37d1aa501274dcd95..938cfc33de83757570e7072e68c30fa73fbd7444 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -10,7 +10,7 @@ import java.util.Arrays;
import tla2sany.semantic.FrontEnd;
public interface TranslationGlobals {
- final String VERSION_NUMBER = "1.0.7";
+ final String VERSION_NUMBER = "1.0.8";
final int TLCValueKind = 100;
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index a9f006ef10fd4f554dd060d5fbdf74d0387096ae..301800d8fdb7c538cde5a5abcc653a9a6e4c29c6 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -127,12 +127,14 @@ public class TupleOrFunction extends AbstractHasFollowers {
return true;
}
if (o instanceof TupleType) {
- TupleType t = (TupleType) o;
- for (int i = 0; i < t.getTypes().size(); i++) {
- if (this.types.containsKey(i + 1)) {
- if (!t.getTypes().get(i).compare(this.types.get(i + 1))) {
- return false;
- }
+ TupleType tupleType = (TupleType) o;
+ for (Integer index : this.types.keySet()) {
+ if (index >= 1
+ && index <= tupleType.getTypes().size()
+ && this.types.get(index).compare(
+ tupleType.getTypes().get(index + -1))) {
+ } else {
+ return false;
}
}
return true;
@@ -183,9 +185,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
@Override
public boolean isUntyped() {
-// if (complete == false) {
-// return true;
-// }
+ // if (complete == false) {
+ // return true;
+ // }
for (TLAType type : types.values()) {
if (type.isUntyped())
return true;
@@ -251,56 +253,56 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (o instanceof TupleOrFunction) {
TupleOrFunction other = (TupleOrFunction) o;
for (Integer i : other.types.keySet()) {
- if(this.types.containsKey(i)){
+ if (this.types.containsKey(i)) {
TLAType res = other.types.get(i).unify(this.types.get(i));
- if(res instanceof AbstractHasFollowers)
+ if (res instanceof AbstractHasFollowers)
((AbstractHasFollowers) res).addFollower(this);
this.types.put(i, res);
- }else{
+ } else {
TLAType res = other.types.get(i);
- if(res instanceof AbstractHasFollowers)
+ if (res instanceof AbstractHasFollowers)
((AbstractHasFollowers) res).addFollower(this);
this.types.put(i, res);
}
-
+
}
other.setFollowersTo(this);
return this;
- // if (isTupleOrFunction(this, other)) {
-// for (Integer i : this.types.keySet()) {
-// if (other.types.containsKey(i)) {
-// TLAType res = this.types.get(i).unify(
-// other.types.get(i));
-// if (res instanceof AbstractHasFollowers) {
-// ((AbstractHasFollowers) res).addFollower(this);
-// }
-// this.types.put(i, res);
-// }
-// }
-// for (Integer i : other.types.keySet()) {
-// if (!this.types.containsKey(i)) {
-// TLAType res = other.types.get(i);
-// if (res instanceof AbstractHasFollowers) {
-// ((AbstractHasFollowers) res).addFollower(this);
-// }
-// this.types.put(i, res);
-// }
-// }
-// return this;
-// } else {
-// ArrayList<TLAType> list1 = new ArrayList<TLAType>();
-// for (int i = 1; i <= types.keySet().size(); i++) {
-// list1.add(types.get(i));
-// }
-// TupleType tuple1 = new TupleType(list1);
-//
-// ArrayList<TLAType> list2 = new ArrayList<TLAType>();
-// for (int i = 1; i <= other.types.keySet().size(); i++) {
-// list2.add(other.types.get(i));
-// }
-// TupleType tuple2 = new TupleType(list2);
-// return tuple1.unify(tuple2);
-// }
+ // if (isTupleOrFunction(this, other)) {
+ // for (Integer i : this.types.keySet()) {
+ // if (other.types.containsKey(i)) {
+ // TLAType res = this.types.get(i).unify(
+ // other.types.get(i));
+ // if (res instanceof AbstractHasFollowers) {
+ // ((AbstractHasFollowers) res).addFollower(this);
+ // }
+ // this.types.put(i, res);
+ // }
+ // }
+ // for (Integer i : other.types.keySet()) {
+ // if (!this.types.containsKey(i)) {
+ // TLAType res = other.types.get(i);
+ // if (res instanceof AbstractHasFollowers) {
+ // ((AbstractHasFollowers) res).addFollower(this);
+ // }
+ // this.types.put(i, res);
+ // }
+ // }
+ // return this;
+ // } else {
+ // ArrayList<TLAType> list1 = new ArrayList<TLAType>();
+ // for (int i = 1; i <= types.keySet().size(); i++) {
+ // list1.add(types.get(i));
+ // }
+ // TupleType tuple1 = new TupleType(list1);
+ //
+ // ArrayList<TLAType> list2 = new ArrayList<TLAType>();
+ // for (int i = 1; i <= other.types.keySet().size(); i++) {
+ // list2.add(other.types.get(i));
+ // }
+ // TupleType tuple2 = new TupleType(list2);
+ // return tuple1.unify(tuple2);
+ // }
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index b20e1ef106c58a5301570dcfc078fb0ceec52520..f718e109222ecbcebc25f9f8728db90de4d68632 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -350,81 +350,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<POperation> opList = new ArrayList<POperation>();
for (int i = 0; i < bOperations.size(); i++) {
BOperation op = bOperations.get(i);
-
- String defName = op.getName();
-
- List<PExpression> paramList = new ArrayList<PExpression>();
- ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
- for (int j = 0; j < op.getFormalParams().size(); j++) {
- paramList
- .add(createIdentifierNode(op.getFormalParams().get(j)));
- }
- for (int j = 0; j < op.getExistQuans().size(); j++) {
- OpApplNode o = op.getExistQuans().get(j);
- whereList.add(visitBoundsOfLocalVariables(o));
- }
-
- AOperation operation = new AOperation();
- operation.setOpName(createTIdentifierLiteral(defName));
- operation.setParameters(paramList);
- operation.setReturnValues(new ArrayList<PExpression>());
-
- AAnySubstitution any = new AAnySubstitution();
- OpDeclNode[] vars = moduleNode.getVariableDecls();
- List<PExpression> anyParams = new ArrayList<PExpression>();
- for (int j = 0; j < vars.length; j++) {
- String varName = getName(vars[j]);
- String nextName = varName + "_n";
- if (op.getUnchangedVariables().contains(varName))
- continue;
- anyParams.add(createIdentifierNode(nextName));
-
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(nextName));
- TLAType t = (TLAType) vars[j].getToolObject(TYPE_ID);
- member.setRight(t.getBNode());
- whereList.add(member);
- }
- any.setIdentifiers(anyParams);
-
- PPredicate body = null;
- if (op.getNode() instanceof OpApplNode) {
- OpApplNode opApplNode = (OpApplNode) op.getNode();
- if (opApplNode.getOperator().getKind() == UserDefinedOpKind
- && !BBuiltInOPs.contains(opApplNode.getOperator()
- .getName())) {
- OpDefNode def = (OpDefNode) opApplNode.getOperator();
- FormalParamNode[] params = def.getParams();
- for (int j = 0; j < params.length; j++) {
- FormalParamNode param = params[j];
- param.setToolObject(SUBSTITUTE_PARAM,
- opApplNode.getArgs()[j]);
- }
- body = visitExprNodePredicate(def.getBody());
- }
- }
- if (body == null) {
- body = visitExprOrOpArgNodePredicate(op.getNode());
- }
- whereList.add(body);
- any.setWhere(createConjunction(whereList));
-
- List<PExpression> varList = new ArrayList<PExpression>();
- List<PExpression> valueList = new ArrayList<PExpression>();
- for (int j = 0; j < vars.length; j++) {
- String varName = getName(vars[j]);
- if (op.getUnchangedVariables().contains(varName))
- continue;
- varList.add(createIdentifierNode(vars[j]));
-
- valueList.add(createIdentifierNode(varName + "_n"));
- }
- AAssignSubstitution assign = new AAssignSubstitution(varList,
- valueList);
- any.setThen(assign);
- operation.setOperationBody(any);
- // opList.add(operation);
-
opList.add(op.getBOperation(this));
}
@@ -1580,7 +1505,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AEqualPredicate equals = new AEqualPredicate();
equals.setLeft(createIdentifierNode(nameOfTempVariable));
equals.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- //predList.add(equals);
+ // predList.add(equals);
AExistsPredicate exist = new AExistsPredicate();
exist.setIdentifiers(idList);
exist.setPredicate(createConjunction(predList));
@@ -1590,18 +1515,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
tList.add(createIdentifierNode(nameOfTempVariable));
compre.setIdentifiers(tList);
compre.setPredicates(exist);
-
- //UNION(p1,p2,p3).(P | {e})
+
+ // UNION(p1,p2,p3).(P | {e})
AQuantifiedUnionExpression union = new AQuantifiedUnionExpression();
union.setIdentifiers(idList);
- union.setPredicates(createConjunction(predList));
+ union.setPredicates(createConjunction(predList));
ASetExtensionExpression set = new ASetExtensionExpression();
List<PExpression> list = new ArrayList<PExpression>();
list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
set.setExpressions(list);
union.setExpression(set);
-
-
+
return union;
}
@@ -2423,13 +2347,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
break;
}
case OPCODE_unchanged: {
+ //System.out.println("hier");
OpApplNode node = (OpApplNode) n.getArgs()[0];
if (node.getOperator().getKind() == VariableDeclKind) {
AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(getName(node.getOperator())
+ "_n"));
equal.setRight(createIdentifierNode(node.getOperator()));
- return equal;
+ return new AEqualPredicate(new ABooleanTrueExpression(),
+ new ABooleanTrueExpression());
+ //return equal;
} else if (node.getOperator().getKind() == UserDefinedOpKind) {
OpDefNode operator = (OpDefNode) node.getOperator();
ExprNode e = operator.getBody();
@@ -2446,7 +2373,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
equal.setRight(createIdentifierNode(var.getOperator()));
list.add(equal);
}
- returnNode = createConjunction(list);
+ //returnNode = createConjunction(list);
+ returnNode = new AEqualPredicate(new ABooleanTrueExpression(),
+ new ABooleanTrueExpression());
break;
}
case OPCODE_uc: { // CHOOSE x : P
diff --git a/src/test/java/de/tla2b/prettyprintb/EventsTest.java b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java
similarity index 91%
rename from src/test/java/de/tla2b/prettyprintb/EventsTest.java
rename to src/test/java/de/tla2b/prettyprintb/ActionsTest.java
index 1db65ff2f0ca0d595fddee633e41d541c7a603f2..869d4234e68d862d8179695e95201546884eda98 100644
--- a/src/test/java/de/tla2b/prettyprintb/EventsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java
@@ -2,9 +2,10 @@ package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
+import org.junit.Ignore;
import org.junit.Test;
-public class EventsTest {
+public class ActionsTest {
@Test
@@ -13,14 +14,14 @@ public class EventsTest {
+ "EXTENDS Naturals \n"
+ "VARIABLES x, y \n"
+ "Init == x = 1 /\\ y = 1 \n"
- + "Next == x' = 1 /\\ UNCHANGED y\n"
+ + "Next == x' = 1 /\\ UNCHANGED y \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "VARIABLES x, y\n"
+ "INVARIANT x : INTEGER & y : INTEGER \n"
+ "INITIALISATION x, y:(x = 1 & y = 1) \n"
- + "OPERATIONS Next = ANY y_n WHERE y_n : INTEGER & y_n = y THEN x,y := 1,y_n END \n"
+ + "OPERATIONS Next = BEGIN x := 1 END \n"
+ "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
index c626abdf65ea55aac4040c0d929d6f8c321b4f3b..97838b2afd1dedf53ee90b76d8b0a59a3b3b74f7 100644
--- a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
@@ -6,6 +6,7 @@ import org.junit.Test;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
@@ -69,6 +70,7 @@ public class TupleVsSequenceTest {
assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
}
+
@Test
public void testTupleVsSequence6() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -78,5 +80,13 @@ public class TupleVsSequenceTest {
TestTypeChecker t = TestUtil.typeCheckString(module);
assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
}
+
+ @Test (expected = TypeErrorException.class)
+ public void testTupleVsSequence7() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE>>[3] \n"
+ + "=================================";
+ TestUtil.typeCheckString(module);
+ }
}