From 3d39850cb3645409ba4b7f5d499cd34f28c60559 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 2 Aug 2013 16:00:57 +0200
Subject: [PATCH] Sequences as relations
---
build.gradle | 3 +-
src/main/java/de/b2tla/B2TLA.java | 18 ++
src/main/java/de/b2tla/TLCRunner.java | 3 +-
.../b2tla/analysis/DefinitionsAnalyser.java | 15 +-
.../de/b2tla/analysis/StandardMadules.java | 22 ++-
.../de/b2tla/analysis/TypeRestrictor.java | 109 +++++++-----
.../b2tla/analysis/UsedStandardModules.java | 69 +++++---
.../java/de/b2tla/btypes/IntegerType.java | 5 +-
.../java/de/b2tla/prettyprint/TLAPrinter.java | 160 ++++++++++--------
src/main/java/de/b2tla/tla/Generator.java | 2 +-
src/main/java/de/b2tla/tlc/TLCOutput.java | 6 +-
.../standardModules/SequencesAsRelations.tla | 57 +++++++
.../ExpressionConstantTest.java | 4 +-
.../b2tla/analysis/TypeRestrictionsTest.java | 18 +-
.../de/b2tla/prettyprint/FunctionTest.java | 4 +-
.../de/b2tla/prettyprint/NumbersTest.java | 35 ++++
.../de/b2tla/prettyprint/SequenceTest.java | 20 ---
.../de/b2tla/tlc/integration/BasicsTest.java | 1 +
.../de/b2tla/tlc/integration/ErrorTest.java | 6 +
src/test/resources/errors/LTLError.mch | 11 ++
.../laws/SequencesAsRelationsTest.mch | 92 +++++++---
21 files changed, 464 insertions(+), 196 deletions(-)
create mode 100644 src/main/resources/standardModules/SequencesAsRelations.tla
rename src/test/java/de/b2tla/{prettyprint => analysis}/ExpressionConstantTest.java (90%)
delete mode 100644 src/test/java/de/b2tla/prettyprint/SequenceTest.java
create mode 100644 src/test/resources/errors/LTLError.mch
diff --git a/build.gradle b/build.gradle
index 0425b65..92b4cce 100644
--- a/build.gradle
+++ b/build.gradle
@@ -35,7 +35,8 @@ dependencies {
test {
- exclude('de/b2tla/tlc/integration/**')
+ exclude('de/b2tla/tlc/integration/probprivate')
+ exclude('de/b2tla/tlc/integration/testing')
}
diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java
index 5865ec0..7b239f0 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/b2tla/B2TLA.java
@@ -226,6 +226,24 @@ public class B2TLA {
STANDARD_MODULES.SequencesAsRelations)) {
createStandardModule(path,
STANDARD_MODULES.SequencesAsRelations.toString());
+
+ if (!translator.getUsedStandardModule().contains(
+ STANDARD_MODULES.Relations)) {
+ createStandardModule(path,
+ STANDARD_MODULES.Relations.toString());
+ }
+
+ if (!translator.getUsedStandardModule().contains(
+ STANDARD_MODULES.FunctionsAsRelations)) {
+ createStandardModule(path,
+ STANDARD_MODULES.FunctionsAsRelations.toString());
+ }
+
+ if (!translator.getUsedStandardModule().contains(
+ STANDARD_MODULES.Functions)) {
+ createStandardModule(path,
+ STANDARD_MODULES.Functions.toString());
+ }
}
}
diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java
index 44e3b38..63da307 100644
--- a/src/main/java/de/b2tla/TLCRunner.java
+++ b/src/main/java/de/b2tla/TLCRunner.java
@@ -70,8 +70,7 @@ public class TLCRunner {
String[] args = list.toArray(new String[list.size()]);
System.out.println("Starting JVM...");
- Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
-
+ final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
index 8519693..82b1784 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
@@ -12,6 +12,7 @@ import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AIntervalExpression;
+import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.Node;
/**
@@ -93,11 +94,19 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
if (null != node) {
try {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
- AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
- int value = Integer.parseInt(sizeExpr.getLiteral().getText());
+ AIntegerExpression sizeExpr = null;
+ Integer value = null;
+ if (d.getRhs() instanceof AUnaryMinusExpression){
+ AUnaryMinusExpression minus = (AUnaryMinusExpression) d.getRhs();
+ sizeExpr = (AIntegerExpression) minus.getExpression();
+ value = - Integer.parseInt(sizeExpr.getLiteral().getText());
+ }else{
+ sizeExpr = (AIntegerExpression) d.getRhs();
+ value = Integer.parseInt(sizeExpr.getLiteral().getText());
+ }
B2TLAGlobals.setMIN_INT(value);
} catch (ClassCastException e) {
-
+ e.printStackTrace();
}
}
}
diff --git a/src/main/java/de/b2tla/analysis/StandardMadules.java b/src/main/java/de/b2tla/analysis/StandardMadules.java
index 9e27cef..1df77a1 100644
--- a/src/main/java/de/b2tla/analysis/StandardMadules.java
+++ b/src/main/java/de/b2tla/analysis/StandardMadules.java
@@ -83,9 +83,27 @@ public class StandardMadules {
public static final String SEQUENCE_TAKE_FIRST_ELEMENTS = "TakeFirstElements";
public static final String SEQUENCE_DROP_FIRST_ELEMENTS = "DropFirstElements";
- public static final String REL_INJECTIVE_SEQUENCES = "RelISeq";
- public static final String REL_NOT_EMPTY_INJECTIVE_SEQUENCES = "RelISeq1";
+
+ // SequencesAsRelations
+ public static final String REL_SEQUENCE_SIZE = "RelSeqSize";
+ public static final String IS_REL_SEQUENCE = "isRelSeq";
+ public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
+ public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";
+ public static final String REL_INJECTIVE_SEQUENCE_1 = "RelISeq1";
+ public static final String REL_SEQUENCE_Concat = "RelSeqConcat";
+ public static final String REL_SEQUENCE_PREPAND = "RelSeqPrepand";
+ public static final String REL_SEQUENCE_APPEND = "RelSeqAppend";
+ public static final String REL_SEQUENCE_REVERSE = "RelSeqRev";
+ public static final String REL_SEQUENCE_FIRST_ELEMENT = "RelSeqFirst";
+ public static final String REL_SEQUENCE_LAST_ELEMENT = "RelSeqLast";
+ public static final String REL_SEQUENCE_FRONT = "RelSeqFront";
+ public static final String REL_SEQUENCE_TAIL = "RelSeqTail";
+ public static final String REL_SEQUENCE_PERM = "RelSeqPerm";
+ public static final String REL_SEQUENCE_GENERAL_CONCATINATION = "RelSeqConc";
+ public static final String REL_SEQUENCE_TAKE_FIRST_ELEMENTS = "RelSeqTakeFirstElements";
+ public static final String REL_SEQUENCE_DROP_FIRST_ELEMENTS = "RelSeqDropFirstElements";
+
/*
* BBuiltIns
*/
diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
index f83347a..477f80c 100644
--- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java
+++ b/src/main/java/de/b2tla/analysis/TypeRestrictor.java
@@ -43,7 +43,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
private MachineContext machineContext;
private final IdentifierDependencies identifierDependencies;
-
+
private Hashtable<Node, ArrayList<NodeType>> restrictedTypesSet;
private HashSet<Node> removedNodes;
@@ -52,9 +52,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
this.machineContext = machineContext;
this.restrictedTypesSet = new Hashtable<Node, ArrayList<NodeType>>();
this.removedNodes = new HashSet<Node>();
-
+
this.identifierDependencies = new IdentifierDependencies(machineContext);
-
+
start.apply(this);
checkLTLFormulas();
@@ -66,17 +66,19 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (de.be4.ltl.core.parser.node.Node ltlNode : visitor
.getUnparsedHashTable().keySet()) {
Node bNode = visitor.getBAst(ltlNode);
-
- if(ltlNode instanceof AExistsLtl){
- Node id = visitor.getLTLIdentifier(((AExistsLtl) ltlNode).getExistsIdentifier().getText());
+
+ if (ltlNode instanceof AExistsLtl) {
+ Node id = visitor.getLTLIdentifier(((AExistsLtl) ltlNode)
+ .getExistsIdentifier().getText());
HashSet<Node> list = new HashSet<Node>();
list.add(id);
- analysePredicate(bNode, list);
- }else if (ltlNode instanceof AForallLtl){
- Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode).getForallIdentifier().getText());
+ analysePredicate(bNode, list, new HashSet<Node>());
+ } else if (ltlNode instanceof AForallLtl) {
+ Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode)
+ .getForallIdentifier().getText());
HashSet<Node> list = new HashSet<Node>();
list.add(id);
- analysePredicate(bNode, list);
+ analysePredicate(bNode, list, new HashSet<Node>());
}
bNode.apply(this);
}
@@ -113,35 +115,37 @@ public class TypeRestrictor extends DepthFirstAdapter {
HashSet<Node> list = new HashSet<Node>();
list.addAll(machineContext.getSetParamter().values());
list.addAll(machineContext.getScalarParameter().values());
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
@Override
public void inAPropertiesMachineClause(APropertiesMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
list.addAll(machineContext.getConstants().values());
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
- private void analysePredicate(Node n, HashSet<Node> list) {
+ private void analysePredicate(Node n, HashSet<Node> list, HashSet<Node> ignoreList) {
if (n instanceof AEqualPredicate) {
PExpression left = ((AEqualPredicate) n).getLeft();
Node r_left = machineContext.getReferences().get(left);
PExpression right = ((AEqualPredicate) n).getRight();
Node r_right = machineContext.getReferences().get(right);
- if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+ if (list.contains(r_left)
+ && isAConstantExpression(right, list, ignoreList)) {
EqualsNode setNode = new EqualsNode(right);
putRestrictedType(r_left, setNode);
- if(!machineContext.getConstants().containsValue(r_left)){
+ if (!machineContext.getConstants().containsValue(r_left)) {
removedNodes.add(n);
}
-
+
}
- if (list.contains(r_right) && !identifierDependencies.containsIdentifier(left, list)) {
+ if (list.contains(r_right)
+ && isAConstantExpression(right, list, ignoreList)) {
EqualsNode setNode = new EqualsNode(left);
putRestrictedType(r_right, setNode);
- if(!machineContext.getConstants().containsValue(r_left)){
+ if (!machineContext.getConstants().containsValue(r_left)) {
removedNodes.add(n);
}
}
@@ -152,9 +156,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
PExpression left = ((AMemberPredicate) n).getLeft();
Node r_left = machineContext.getReferences().get(left);
PExpression right = ((AMemberPredicate) n).getRight();
- if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+ if (list.contains(r_left)
+ && isAConstantExpression(right, list, ignoreList)) {
putRestrictedType(r_left, new ElementOfNode(right));
- if(!machineContext.getConstants().containsValue(r_left)){
+ if (!machineContext.getConstants().containsValue(r_left)) {
removedNodes.add(n);
}
}
@@ -166,9 +171,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
Node r_left = machineContext.getReferences().get(left);
PExpression right = ((ASubsetPredicate) n).getRight();
- if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+ if (list.contains(r_left)
+ && isAConstantExpression(right, list, ignoreList)) {
putRestrictedType(r_left, new SubsetNode(right));
- if(!machineContext.getConstants().containsValue(r_left)){
+ if (!machineContext.getConstants().containsValue(r_left)) {
removedNodes.add(n);
}
}
@@ -176,20 +182,39 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
if (n instanceof AConjunctPredicate) {
- analysePredicate(((AConjunctPredicate) n).getLeft(), list);
- analysePredicate(((AConjunctPredicate) n).getRight(), list);
+ analysePredicate(((AConjunctPredicate) n).getLeft(), list, ignoreList);
+ analysePredicate(((AConjunctPredicate) n).getRight(), list, ignoreList);
return;
}
-
- if(n instanceof Start){
- analysePredicate(((Start) n).getPParseUnit(), list);
+
+ if (n instanceof AExistsPredicate) {
+ HashSet<Node> set = new HashSet<Node>();
+ for (PExpression e : ((AExistsPredicate) n).getIdentifiers()) {
+ set.add(e);
+ }
+ set.addAll(ignoreList);
+ analysePredicate(((AExistsPredicate) n).getPredicate(), list, set);
+ }
+
+ if (n instanceof Start) {
+ analysePredicate(((Start) n).getPParseUnit(), list, ignoreList);
}
-
- if(n instanceof APredicateParseUnit){
- analysePredicate(((APredicateParseUnit) n).getPredicate(), list);
+
+ if (n instanceof APredicateParseUnit) {
+ analysePredicate(((APredicateParseUnit) n).getPredicate(), list, ignoreList);
return;
}
}
+
+ public boolean isAConstantExpression(Node node, HashSet<Node> list, HashSet<Node> ignoreList){
+ HashSet<Node> newList = new HashSet<Node>();
+ newList.addAll(list);
+ newList.addAll(ignoreList);
+ if(identifierDependencies.containsIdentifier(node, newList)){
+ return false;
+ }
+ return true;
+ }
@Override
public void inAForallPredicate(AForallPredicate node) {
@@ -201,7 +226,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
AImplicationPredicate implication = (AImplicationPredicate) node
.getImplication();
- analysePredicate(implication.getLeft(), list);
+ analysePredicate(implication.getLeft(), list, new HashSet<Node>());
}
@Override
@@ -212,7 +237,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicate(), list);
+ analysePredicate(node.getPredicate(), list, new HashSet<Node>());
}
@Override
@@ -223,7 +248,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
@Override
@@ -235,7 +260,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
@Override
@@ -247,7 +272,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
// e.apply(this);
}
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
@Override
@@ -258,7 +283,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicate(), list);
+ analysePredicate(node.getPredicate(), list, new HashSet<Node>());
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -268,7 +293,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -278,7 +303,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
for (PExpression e : copy) {
list.add(e);
}
- analysePredicate(node.getPredicates(), list);
+ analysePredicate(node.getPredicates(), list, new HashSet<Node>());
}
private Hashtable<Node, HashSet<Node>> expectedIdentifieListTable = new Hashtable<Node, HashSet<Node>>();
@@ -317,7 +342,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
@Override
public void inAPreconditionSubstitution(APreconditionSubstitution node) {
HashSet<Node> list = getExpectedIdentifier(node);
- analysePredicate(node.getPredicate(), list);
+ analysePredicate(node.getPredicate(), list, new HashSet<Node>());
}
private HashSet<Node> getExpectedIdentifier(Node node) {
@@ -330,7 +355,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
@Override
public void inASelectSubstitution(ASelectSubstitution node) {
HashSet<Node> list = getExpectedIdentifier(node);
- analysePredicate(node.getCondition(), list);
+ analysePredicate(node.getCondition(), list, new HashSet<Node>());
}
@Override
@@ -342,7 +367,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
list.addAll(getExpectedIdentifier(node));
- analysePredicate(node.getWhere(), list);
+ analysePredicate(node.getWhere(), list, new HashSet<Node>());
}
@Override
@@ -354,7 +379,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
list.addAll(getExpectedIdentifier(node));
- analysePredicate(node.getPredicate(), list);
+ analysePredicate(node.getPredicate(), list, new HashSet<Node>());
}
}
diff --git a/src/main/java/de/b2tla/analysis/UsedStandardModules.java b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
index 924b3b7..82777e2 100644
--- a/src/main/java/de/b2tla/analysis/UsedStandardModules.java
+++ b/src/main/java/de/b2tla/analysis/UsedStandardModules.java
@@ -105,7 +105,8 @@ import de.be4.classicalb.core.parser.node.PExpression;
public class UsedStandardModules extends DepthFirstAdapter {
public static enum STANDARD_MODULES {
- Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations
+ Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations,
+ FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations,
}
private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<UsedStandardModules.STANDARD_MODULES>();
@@ -569,64 +570,88 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
public void inAFirstExpression(AFirstExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Sequences);
+ evalSequenceOrRelation(node);
}
public void inATailExpression(ATailExpression node) {
- usedStandardModules.add(STANDARD_MODULES.Sequences);
+ evalSequenceOrRelation(node);
}
/**
* SequencesExtended
*/
+ private void evalSequenceExtendedOrRelation(Node node){
+ BType type = typechecker.getType(node);
+ if (type instanceof FunctionType) {
+ usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ }
+ }
+
public void inAIseqExpression(AIseqExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof FunctionType) {
+ usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ }
}
public void inASeq1Expression(ASeq1Expression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof FunctionType) {
+ usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ }
}
+ public void inAIseq1Expression(AIseq1Expression node) {
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof FunctionType) {
+ usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ }
+ }
+
public void inAInsertFrontExpression(AInsertFrontExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inALastExpression(ALastExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inAFrontExpression(AFrontExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inAPermExpression(APermExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof SetType) {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ }
}
public void inARevExpression(ARevExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inAGeneralConcatExpression(AGeneralConcatExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inARestrictFrontExpression(ARestrictFrontExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+ evalSequenceExtendedOrRelation(node);
}
public void inARestrictTailExpression(ARestrictTailExpression node) {
- usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
- }
-
- /**
- * sonst
- *
- */
-
- public void inAIseq1Expression(AIseq1Expression node) {
- usedStandardModules.add(STANDARD_MODULES.Relations);
+ evalSequenceExtendedOrRelation(node);
}
}
diff --git a/src/main/java/de/b2tla/btypes/IntegerType.java b/src/main/java/de/b2tla/btypes/IntegerType.java
index 3cda971..d86b774 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.B2TLAGlobals;
import de.b2tla.analysis.Typechecker;
import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIntegerExpression;
@@ -41,9 +42,11 @@ public class IntegerType implements BType {
}
public String getTlaType() {
- return "Int";
+ return B2TLAGlobals.getMIN_INT() + ".." + B2TLAGlobals.getMAX_INT();
}
+
+
public boolean isUntyped() {
return false;
}
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index bc9e722..5696a29 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -23,7 +23,6 @@ import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
import de.b2tla.btypes.PairType;
import de.b2tla.btypes.SetType;
-import de.b2tla.btypes.UntypedType;
import de.b2tla.ltl.LTLFormulaVisitor;
import de.b2tla.tla.ConfigFile;
import de.b2tla.tla.TLADefinition;
@@ -196,11 +195,13 @@ public class TLAPrinter extends DepthFirstAdapter {
}
- for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
- LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas().get(
- i);
- this.configFileString.append("PROPERTIES " + ltlVisitor.getName()
- + "\n");
+ if (B2TLAGlobals.isCheckltl()) {
+ for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
+ LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas()
+ .get(i);
+ this.configFileString.append("PROPERTIES "
+ + ltlVisitor.getName() + "\n");
+ }
}
// CONSTANTS
@@ -1620,7 +1621,8 @@ public class TLAPrinter extends DepthFirstAdapter {
&& !typeRestrictor.removeNode(parent)) {
return true;
} else {
- if (parent instanceof ATotalFunctionExpression) {
+ String clazz = parent.getClass().getName();
+ if (clazz.contains("Total") || clazz.contains("Partial")) {
return isElementOf(node.parent());
} else
return false;
@@ -2244,45 +2246,63 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseASizeExpression(ASizeExpression node) {
- tlaModuleString.append("Len");
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), "Len", REL_SEQUENCE_SIZE,
+ node.getExpression(), null);
}
@Override
public void caseAConcatExpression(AConcatExpression node) {
- inAConcatExpression(node);
- node.getLeft().apply(this);
- tlaModuleString.append(" \\o ");
- node.getRight().apply(this);
- outAConcatExpression(node);
+ BType type = typechecker.getType(node);
+ if (type instanceof SetType) {
+ tlaModuleString.append(REL_SEQUENCE_Concat);
+ tlaModuleString.append("(");
+ node.getLeft().apply(this);
+ tlaModuleString.append(", ");
+ node.getRight().apply(this);
+ tlaModuleString.append(")");
+ } else {
+ inAConcatExpression(node);
+ node.getLeft().apply(this);
+ tlaModuleString.append(" \\o ");
+ node.getRight().apply(this);
+ outAConcatExpression(node);
+ }
}
@Override
public void caseAInsertTailExpression(AInsertTailExpression node) {
- tlaModuleString.append("Append");
+ printSequenceOrRelation(node, "Append",
+ REL_SEQUENCE_APPEND, node.getLeft(), node.getRight());
+ }
+
+ private void printSequenceOrRelation(Node node, String sequence,
+ String relation, Node left, Node right) {
+ BType type = typechecker.getType(node);
+ if (type instanceof SetType) {
+ tlaModuleString.append(relation);
+ } else {
+ tlaModuleString.append(sequence);
+ }
tlaModuleString.append("(");
- node.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getRight().apply(this);
+ left.apply(this);
+
+ if (right != null) {
+ tlaModuleString.append(",");
+ right.apply(this);
+ }
tlaModuleString.append(")");
}
@Override
public void caseAFirstExpression(AFirstExpression node) {
- tlaModuleString.append("Head");
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), "Head",
+ REL_SEQUENCE_FIRST_ELEMENT, node.getExpression(), null);
}
@Override
public void caseATailExpression(ATailExpression node) {
- tlaModuleString.append("Tail");
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), "Tail",
+ REL_SEQUENCE_TAIL, node.getExpression(), null);
}
/**
@@ -2291,11 +2311,16 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIseqExpression(AIseqExpression node) {
- if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
- tlaModuleString.append(INJECTIVE_SEQUENCE_ELEMENT_OF);
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof SetType) {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
} else {
- tlaModuleString.append(INJECTIVE_SEQUENCE);
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
+ tlaModuleString.append(INJECTIVE_SEQUENCE_ELEMENT_OF);
+ } else {
+ tlaModuleString.append(INJECTIVE_SEQUENCE);
+ }
}
tlaModuleString.append("(");
node.getExpression().apply(this);
@@ -2304,11 +2329,17 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIseq1Expression(AIseq1Expression node) {
- if (node.parent() instanceof AMemberPredicate
- && !typeRestrictor.removeNode(node.parent())) {
- tlaModuleString.append(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
+ SetType set = (SetType) typechecker.getType(node);
+ System.out.println(set + " " + node.hashCode());
+ if (set.getSubtype() instanceof SetType) {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
} else {
- tlaModuleString.append(INJECTIVE_SEQUENCE_1);
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.removeNode(node.parent())) {
+ tlaModuleString.append(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
+ } else {
+ tlaModuleString.append(INJECTIVE_SEQUENCE_1);
+ }
}
tlaModuleString.append("(");
node.getExpression().apply(this);
@@ -2325,25 +2356,24 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseALastExpression(ALastExpression node) {
- tlaModuleString.append(SEQUENCE_LAST_ELEMENT);
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), SEQUENCE_LAST_ELEMENT,
+ REL_SEQUENCE_LAST_ELEMENT, node.getExpression(), null);
}
@Override
public void caseAInsertFrontExpression(AInsertFrontExpression node) {
- tlaModuleString.append(SEQUENCE_PREPEND_ELEMENT);
- tlaModuleString.append("(");
- node.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getRight().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getRight(), SEQUENCE_PREPEND_ELEMENT,
+ REL_SEQUENCE_PREPAND, node.getLeft(), node.getRight());
}
@Override
public void caseAPermExpression(APermExpression node) {
- tlaModuleString.append(SEQUENCE_PERMUTATION);
+ SetType set = (SetType) typechecker.getType(node);
+ if (set.getSubtype() instanceof SetType) {
+ tlaModuleString.append(REL_SEQUENCE_PERM);
+ } else {
+ tlaModuleString.append(SEQUENCE_PERMUTATION);
+ }
tlaModuleString.append("(");
node.getExpression().apply(this);
tlaModuleString.append(")");
@@ -2351,46 +2381,34 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseARevExpression(ARevExpression node) {
- tlaModuleString.append(SEQUENCE_REVERSE);
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node, SEQUENCE_REVERSE, REL_SEQUENCE_REVERSE,
+ node.getExpression(), null);
}
@Override
public void caseAFrontExpression(AFrontExpression node) {
- tlaModuleString.append(SEQUENCE_FRONT);
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), SEQUENCE_FRONT,
+ REL_SEQUENCE_FRONT, node.getExpression(), null);
}
@Override
public void caseAGeneralConcatExpression(AGeneralConcatExpression node) {
- tlaModuleString.append(SEQUENCE_GENERAL_CONCATINATION);
- tlaModuleString.append("(");
- node.getExpression().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node.getExpression(), SEQUENCE_GENERAL_CONCATINATION,
+ REL_SEQUENCE_GENERAL_CONCATINATION, node.getExpression(), null);
}
@Override
public void caseARestrictFrontExpression(ARestrictFrontExpression node) {
- tlaModuleString.append(SEQUENCE_TAKE_FIRST_ELEMENTS);
- tlaModuleString.append("(");
- node.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getRight().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node, SEQUENCE_TAKE_FIRST_ELEMENTS,
+ REL_SEQUENCE_TAKE_FIRST_ELEMENTS, node.getLeft(),
+ node.getRight());
}
@Override
public void caseARestrictTailExpression(ARestrictTailExpression node) {
- tlaModuleString.append(SEQUENCE_DROP_FIRST_ELEMENTS);
- tlaModuleString.append("(");
- node.getLeft().apply(this);
- tlaModuleString.append(", ");
- node.getRight().apply(this);
- tlaModuleString.append(")");
+ printSequenceOrRelation(node, SEQUENCE_DROP_FIRST_ELEMENTS,
+ REL_SEQUENCE_DROP_FIRST_ELEMENTS, node.getLeft(),
+ node.getRight());
}
/**
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index cb07974..059a074 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -15,7 +15,6 @@ 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;
@@ -91,6 +90,7 @@ public class Generator extends DepthFirstAdapter {
private void evalSpec() {
if (this.configFile.isInit() && this.configFile.isNext()
+ && B2TLAGlobals.isCheckltl()
&& machineContext.getLTLFormulas().size() > 0) {
this.configFile.setSpec();
}
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
index 9279f9b..3b2643e 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ b/src/main/java/de/b2tla/tlc/TLCOutput.java
@@ -22,7 +22,7 @@ public class TLCOutput {
String parseError;
public static enum TLCResult {
- Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
+ Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalPropertyError, WellDefinednessError
}
public long getRunningTime() {
@@ -33,7 +33,7 @@ public class TLCOutput {
public String getError() {
if (error == TLCResult.InvariantViolation) {
return "Invariant Violation";
- } else if (error == TLCResult.TemporalProperty) {
+ } else if (error == TLCResult.TemporalPropertyError) {
return "Temporal Property Violation";
}
return error.toString();
@@ -170,7 +170,7 @@ public class TLCOutput {
} else if (res[1].equals("Assumption")) {
return TLCResult.PropertiesError;
} else if (res[1].equals("Temporal")) {
- return TLCResult.TemporalProperty;
+ return TLCResult.TemporalPropertyError;
} else if (m.equals("Error: TLC threw an unexpected exception.")) {
return null;
} else if (m.startsWith("\"Error: Invalid function call to relation")) {
diff --git a/src/main/resources/standardModules/SequencesAsRelations.tla b/src/main/resources/standardModules/SequencesAsRelations.tla
new file mode 100644
index 0000000..b35a1bc
--- /dev/null
+++ b/src/main/resources/standardModules/SequencesAsRelations.tla
@@ -0,0 +1,57 @@
+------------------------ MODULE SequencesAsRelations ------------------------
+EXTENDS FiniteSets, Naturals, Relations, FunctionsAsRelations
+
+isRelSeq(x, S) == \A n \in 1..Cardinality(x): RelCall(x,n) \in S
+
+isRelSeq1(x, S) == x # {} /\ \A n \in 1..Cardinality(x): RelCall(x,n) \in S
+
+
+LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)}
+ : n \in 0..Cardinality(S)}
+
+RelISeq(S) == {{<<n, x[n]>>:n \in 1..Len(x)} :x \in ISeq(S)}
+
+RelISeq1(S) == RelISeq(S) \ {{}}
+
+RelSeqSize(S) == Cardinality(S)
+
+RelSeqConcat(a, b) == a \cup {<<x[1]+Cardinality(a), x[2]>> : x \in b}
+
+RelSeqPrepand(E, s) == {<<1,E>>} \cup {<<x[1]+1, x[2]>> : x \in s}
+
+RelSeqAppend(s, E) == s \cup {<<Cardinality(s)+ 1,E>>}
+
+RelSeqRev(s) == LET l == Cardinality(s)
+ IN {<<l-x[1]+1, x[2]>> : x \in s }
+RelSeqRev2(s) == LET l == Cardinality(s)
+ IN {<<i, RelCall(s,l-i+1)>>: i \in 1..l}
+
+RelSeqFirst(s) == RelCall(s, 1)
+
+RelSeqLast(s) == RelCall(s, Cardinality(s))
+
+RelSeqFront(s) == {x \in s : x[1] # Cardinality(s)}
+\*RelSeqFront2(s) == s \ {<<Cardinality(s), RelCall(s, Cardinality(s))>>}
+
+RelSeqTail(s) == {<<x[1]-1,x[2]>> :x \in {x \in s : x[1] # 1}}
+
+RECURSIVE RelSeqPerm(_)
+RelSeqPerm(S) == IF S = {}
+ THEN {{}}
+ ELSE LET ps == [x \in S |-> {RelSeqAppend(s, x): s \in RelSeqPerm(S\{x})}]
+ IN UNION {ps[x]: x \in S}
+
+
+RECURSIVE RelSeqConc(_)
+RelSeqConc(S) == IF S = {}
+ THEN {}
+ ELSE RelSeqConcat(RelSeqFirst(S), RelSeqConc(RelSeqTail(S)) )
+
+RelSeqTakeFirstElements(s, n) == IF Assert(n \in 0..Cardinality(s), "Well defineness condition of take-first-operator is violated")
+ THEN {x \in s: x[1] \leq n}
+ ELSE FALSE
+
+RelSeqDropFirstElements(s, n) == IF Assert(n \in 0..Cardinality(s), "Well defineness condition of drop-first-operator its violated")
+ THEN {<<x[1]-n,x[2]>> :x \in {x \in s: x[1] > n}}
+ ELSE FALSE
+=============================================================================
\ No newline at end of file
diff --git a/src/test/java/de/b2tla/prettyprint/ExpressionConstantTest.java b/src/test/java/de/b2tla/analysis/ExpressionConstantTest.java
similarity index 90%
rename from src/test/java/de/b2tla/prettyprint/ExpressionConstantTest.java
rename to src/test/java/de/b2tla/analysis/ExpressionConstantTest.java
index 39bbf6f..dfd6d8d 100644
--- a/src/test/java/de/b2tla/prettyprint/ExpressionConstantTest.java
+++ b/src/test/java/de/b2tla/analysis/ExpressionConstantTest.java
@@ -1,4 +1,4 @@
-package de.b2tla.prettyprint;
+package de.b2tla.analysis;
import static de.b2tla.util.TestUtil.compare;
@@ -50,7 +50,7 @@ public class ExpressionConstantTest {
String expected = "---- MODULE test----\n"
+ "EXTENDS Integers \n"
- + "ASSUME \\A x \\in Int, y \\in {1} : x = y => 1 = 1 \n"
+ + "ASSUME \\A x \\in (-1..4), y \\in {1} : x = y => 1 = 1 \n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java b/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
index 4a1f5f6..b956efd 100644
--- a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
@@ -80,7 +80,7 @@ public class TypeRestrictionsTest {
+ "PROPERTIES #x,y.(x = 1 & x = y) \n" + "END";
String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
- + "ASSUME \\E x \\in {1}, y \\in Int: x = y \n"
+ + "ASSUME \\E x \\in {1}, y \\in -1..4: x = y \n"
+ "======";
compare(expected, machine);
}
@@ -116,7 +116,19 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
+ "k == 1 \n"
- + "ASSUME \\E x \\in Int: \\E y \\in {x}: x = 1 \n"
+ + "ASSUME \\E x \\in {1} : (\\E y \\in {x} : TRUE) \n"
+ + "====";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testQuantificationsInSetComprehension() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {1} = {x| #y.(x = 1 & y = x) & 1=1}\n" + "END";
+
+ String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
+ + "k == 1 \n"
+ + "ASSUME {1} = {x \\in ({1}): (\\E y \\in {x} : TRUE) /\\ 1 = 1}\n"
+ "====";
compare(expected, machine);
}
@@ -193,7 +205,7 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers \n"
- + "ASSUME \\E x \\in {1}, y \\in Int : y = x \n"
+ + "ASSUME \\E x \\in {1}, y \\in -1..4 : y = x \n"
+ "====";
compare(expected, machine);
}
diff --git a/src/test/java/de/b2tla/prettyprint/FunctionTest.java b/src/test/java/de/b2tla/prettyprint/FunctionTest.java
index b032839..628841b 100644
--- a/src/test/java/de/b2tla/prettyprint/FunctionTest.java
+++ b/src/test/java/de/b2tla/prettyprint/FunctionTest.java
@@ -49,7 +49,7 @@ public class FunctionTest {
+ "END";
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers\n"
- + "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in (Int \\times Int) : a = b} |-> a + b][2, 2]\n"
+ + "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b} |-> a + b][2, 2]\n"
+ "====";
compare(expected, machine);
}
@@ -75,7 +75,7 @@ public class FunctionTest {
+ "END";
String expected = "---- MODULE test ----\n"
+ "EXTENDS Integers\n"
- + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in (Int \\times Int) : a = b}}\n"
+ + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b}}\n"
+ "====";
compare(expected, machine);
}
diff --git a/src/test/java/de/b2tla/prettyprint/NumbersTest.java b/src/test/java/de/b2tla/prettyprint/NumbersTest.java
index 5362a43..0f928f7 100644
--- a/src/test/java/de/b2tla/prettyprint/NumbersTest.java
+++ b/src/test/java/de/b2tla/prettyprint/NumbersTest.java
@@ -226,6 +226,41 @@ public class NumbersTest {
compare(expected, machine);
}
+ @Test
+ public void testMinInt() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES MININT = MININT \n"
+ + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Integers\n"
+ + "ASSUME -1 = -1\n"
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testMaxInt() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES MAXINT = MAXINT \n"
+ + "END";
+ String expected = "---- MODULE test----\n"
+ + "ASSUME 4 = 4\n"
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testSetComprehensionInt() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {x| 1=1 => x = 1} = {} \n"
+ + "END";
+ String expected = "---- MODULE test----\n"
+ + "EXTENDS Integers\n"
+ + "ASSUME {x \\in (-1..4): 1 = 1 => x = 1} = {}\n"
+ + "======";
+ compare(expected, machine);
+ }
+
}
diff --git a/src/test/java/de/b2tla/prettyprint/SequenceTest.java b/src/test/java/de/b2tla/prettyprint/SequenceTest.java
deleted file mode 100644
index 3161223..0000000
--- a/src/test/java/de/b2tla/prettyprint/SequenceTest.java
+++ /dev/null
@@ -1,20 +0,0 @@
-package de.b2tla.prettyprint;
-
-import static de.b2tla.util.TestUtil.compareEquals;
-
-import org.junit.Test;
-
-public class SequenceTest {
-
-
- @Test
- public void testConcatination() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES {(1,2)}^{(2,2)} = {(1,2),(1,3)} \n" + "END";
- String expected = "---- MODULE test ----\n"
- + "EXTENDS SequencesAsRelations\n"
- + "ASSUME {<<1, 2>>} \\o {<<2, 2>>} = {<<1, 2>>, <<1, 3>>}\n"
- + "====";
- compareEquals(expected, machine);
- }
-}
diff --git a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
index cc96847..ef8c75b 100644
--- a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
@@ -43,6 +43,7 @@ public class BasicsTest extends AbstractParseMachineTest{
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(NoError, "./src/test/resources/basics"));
+ list.add(new TestPair(NoError, "./src/test/resources/laws"));
return getConfiguration(list);
}
}
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
index dad6dd5..f52a434 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
@@ -65,4 +65,10 @@ public class ErrorTest {
assertEquals(AssertionError, B2TLA.test(a,true));
}
+ @Test
+ public void testTemporalPropertyError() throws Exception {
+ String[] a = new String[] { "./src/test/resources/errors/LTLError.mch" };
+ assertEquals(TemporalPropertyError, B2TLA.test(a,true));
+ }
+
}
diff --git a/src/test/resources/errors/LTLError.mch b/src/test/resources/errors/LTLError.mch
new file mode 100644
index 0000000..ac3acfc
--- /dev/null
+++ b/src/test/resources/errors/LTLError.mch
@@ -0,0 +1,11 @@
+MACHINE LTLError
+DEFINITIONS
+ASSERT_LTL_1 == "F {x = 11}"
+VARIABLES x
+INVARIANT
+ x : 1..10
+INITIALISATION x:=1
+OPERATIONS
+ Inc = PRE x < 10 THEN x:= x + 1 END;
+ Reset = PRE x = 10 THEN x := 1 END
+END
\ No newline at end of file
diff --git a/src/test/resources/laws/SequencesAsRelationsTest.mch b/src/test/resources/laws/SequencesAsRelationsTest.mch
index 2ab2f2f..ab473a9 100644
--- a/src/test/resources/laws/SequencesAsRelationsTest.mch
+++ b/src/test/resources/laws/SequencesAsRelationsTest.mch
@@ -1,23 +1,73 @@
MACHINE SequencesAsRelationsTest
-VARIABLES x
-INVARIANT x : 1..3
-INITIALISATION x := 1
-OPERATIONS
-foo = PRE 1 = 1 THEN x := 2 END
-ASSERTIONS
- {} = [];
- {(1,1)} = [1]
- /*[] /: seq1({1,2});
- iseq({1,2}) ={[], [1], [2], [1, 2], [2, 1]};
- [1] : iseq({1,2});
- iseq1({1,2}) ={[1], [2], [1, 2], [2, 1]};
- [1] : iseq1({1,2});
- perm({1,2}) = {[1,2], [2,1]};
- rev([1,2,3]) = [3,2,1];
- conc([[1,2],[3],[4,5]]) = [1,2,3,4,5];
- [1,2,3,4] /|\ 3 = [1,2,3];
- [1,2,3,4] \|/ 3 = [4];
- 1 -> [2,3] = [1,2,3];
- last([1,2]) = 2;
- front([1,2,3]) = [1,2]*/
+PROPERTIES
+ {} = []
+& {(1,1)} = [1]
+
+/* Set of injective Sequence */
+& iseq({}) = {{}}
+& iseq({1}) = {{},{(1,1)}}
+
+/* Set of non empty injective Sequence */
+& iseq1({}) = {}
+& iseq1({1}) = {{(1,1)}}
+
+/* Size */
+& size({}) = 0
+& size({(1,1),(2,2)}) = 2
+
+/* Concatenation */
+& {(1,1),(2,2)}^{(1,3)} = {(1,1),(2,2),(3,3)}
+& {(1,1),(2,2)}^{} = {(1,1),(2,2)}
+& {}^{(1,1),(2,2)} = {(1,1),(2,2)}
+& {}^{} = {}
+
+/* Prepand */
+& 1 -> {(1,2),(2,3)} = {(1,1),(2,2),(3,3)}
+& 1 -> {} = {(1,1)}
+
+/* Append */
+& {(1,1),(2,2)} <- 3 = {(1,1),(2,2),(3,3)}
+& {} <- 1 = {(1,1)}
+
+/* Front */
+& front({(1,1)}) = {}
+& front({(1,1),(2,2),(3,3)}) = {(1,1),(2,2)}
+
+/* First */
+& first({(1,1)}) = 1
+& first({(1,1),(2,2)}) = 1
+
+/* Tail */
+& tail({(1,1)}) = {}
+& tail({(1,1),(2,2),(3,3)}) = {(1,2),(2,3)}
+
+/* Last */
+& last({(1,1)}) = 1
+& last({(1,1),(2,2)}) = 2
+
+/* Reverse */
+& rev({}) = {}
+& rev({(1,1)}) = {(1,1)}
+& rev({(1,1),(2,2),(3,3)}) = {(1,3),(2,2),(3,1)}
+
+/* Generalized Concatenation */
+& conc({(1,{(1,1),(2,2)}),(2,{(1,3)})}) = {(1,1),(2,2),(3,3)}
+& conc({(1,{(1,1),(2,2)}),(2,{})}) = {(1,1),(2,2)}
+& conc({(1,{}), (2,{(1,1),(2,2)})}) = {(1,1),(2,2)}
+& conc({(1,{}),(2,{})}) = {}
+
+/* Perm */
+& perm({3,4}) = {{(1,3),(2,4)},{(1,4),(2,3)}}
+& perm({}) = {{}}
+
+/* Take first elements */
+& {(1,1),(2,2)} /|\ 1 = {(1,1)}
+& {(1,1),(2,2)} /|\ 2 = {(1,1),(2,2)}
+& {(1,1)} /|\ 0 = {}
+& {} /|\ 0 = {}
+
+& {(1,1),(2,2)} \|/ 1 = {(1,2)}
+& {(1,1),(2,2)} \|/ 0 = {(1,1),(2,2)}
+& {(1,1)} \|/ 1 = {}
+& {} \|/ 0 = {}
END
\ No newline at end of file
--
GitLab