From 8c8485b7734ebcc55951ae51cd43bbc37f12cd8f Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Sat, 31 May 2014 18:05:27 +0200
Subject: [PATCH] Added predicate for constant setup to trace file
---
.../de/tlc4b/analysis/MachineContext.java | 12 +++----
.../de/tlc4b/analysis/StandardMadules.java | 2 ++
.../tlc4b/analysis/UsedStandardModules.java | 13 +++++---
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 31 +++++++++++++------
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 2 +-
.../standardModules/SequencesAsRelations.tla | 13 ++++++++
6 files changed, 53 insertions(+), 20 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 8376419..7e4b87c 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -81,7 +81,7 @@ public class MachineContext extends DepthFirstAdapter {
private final ArrayList<LTLFormulaVisitor> ltlVisitors;
private final PPredicate constantsSetup;
- private boolean originallyHadConstants = false;
+ private boolean constantSetupInTraceFile = false;
// machine identifier
private final LinkedHashMap<String, Node> setParameter;
private final LinkedHashMap<String, Node> scalarParameter;
@@ -476,7 +476,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- originallyHadConstants = true;
+ constantSetupInTraceFile = true;
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
@@ -490,7 +490,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAbstractConstantsMachineClause(
AAbstractConstantsMachineClause node) {
- originallyHadConstants = true;
+ constantSetupInTraceFile = true;
List<PExpression> copy = new ArrayList<PExpression>(
node.getIdentifiers());
for (PExpression e : copy) {
@@ -593,7 +593,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
-
+ constantSetupInTraceFile = true;
/**
* check identifier scope in properties clauses
*/
@@ -1109,8 +1109,8 @@ public class MachineContext extends DepthFirstAdapter {
return constantsSetup;
}
- public boolean originallyHadConstants() {
- return originallyHadConstants;
+ public boolean constantSetupInTraceFile() {
+ return constantSetupInTraceFile;
}
}
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 1eefd12..5d8ae04 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -148,7 +148,9 @@ public final class StandardMadules {
public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
public static final String REL_SEQUENCE_1_SET = "RelSeqSet1";
public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";
+ public static final String REL_INJECTIVE_SEQUENCE_ELEMENT_OF = "RelISeqEleOf";
public static final String REL_INJECTIVE_SEQUENCE_1 = "RelISeq1";
+ public static final String REL_INJECTIVE_SEQUENCE_1_ELEMENT_OF = "RelISeq1EleOf";
public static final String REL_SEQUENCE_Concat = "RelSeqConcat";
public static final String REL_SEQUENCE_PREPAND = "RelSeqPrepand";
public static final String REL_SEQUENCE_APPEND = "RelSeqAppend";
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 6ae2ca1..19497f2 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -532,11 +532,16 @@ public class UsedStandardModules extends DepthFirstAdapter {
*/
public void inASeqExpression(ASeqExpression node) {
- evalSequenceOrRelation(node);
+ SetType type = (SetType) typechecker.getType(node);
+ if (type.getSubtype() instanceof FunctionType) {
+ usedStandardModules.add(STANDARD_MODULES.Sequences);
+ } else {
+ usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+ }
}
public void inASizeExpression(ASizeExpression node) {
- evalSequenceOrRelation(node);
+ evalSequenceOrRelation(node.getExpression());
}
public void inAConcatExpression(AConcatExpression node) {
@@ -553,11 +558,11 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
public void inAFirstExpression(AFirstExpression node) {
- evalSequenceOrRelation(node);
+ evalSequenceOrRelation(node.getExpression());
}
public void inATailExpression(ATailExpression node) {
- evalSequenceOrRelation(node);
+ evalSequenceOrRelation(node.getExpression());
}
/**
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index e0e5b6e..f07ed67 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -173,11 +173,13 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printLTLFormulas() {
ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
- for (int i = 0; i < visitors.size(); i++) {
- LTLFormulaVisitor visitor = visitors.get(i);
- tlaModuleString.append(visitor.getName() + " == ");
- visitor.printLTLFormula(this, typeRestrictor);
- tlaModuleString.append("\n");
+ if (TLC4BGlobals.isCheckltl()) {
+ for (int i = 0; i < visitors.size(); i++) {
+ LTLFormulaVisitor visitor = visitors.get(i);
+ tlaModuleString.append(visitor.getName() + " == ");
+ visitor.printLTLFormula(this, typeRestrictor);
+ tlaModuleString.append("\n");
+ }
}
}
@@ -304,7 +306,7 @@ public class TLAPrinter extends DepthFirstAdapter {
ArrayList<Node> list = this.tlaModule.getAssume();
if (list.size() == 0)
return;
-
+
for (int i = 0; i < list.size(); i++) {
tlaModuleString.append("ASSUME ");
list.get(i).apply(this);
@@ -1716,7 +1718,8 @@ public class TLAPrinter extends DepthFirstAdapter {
} else {
if (node.parent() instanceof AMemberPredicate
&& !typeRestrictor.isARemovedNode(node.parent())
- && !this.tlaModule.getInitPredicates().contains(node.parent())) {
+ && !this.tlaModule.getInitPredicates().contains(
+ node.parent())) {
tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
} else {
tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -2537,7 +2540,12 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAIseqExpression(AIseqExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.isARemovedNode(node.parent())) {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE_ELEMENT_OF);
+ } else {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
+ }
} else {
if (node.parent() instanceof AMemberPredicate
&& !typeRestrictor.isARemovedNode(node.parent())) {
@@ -2555,7 +2563,12 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAIseq1Expression(AIseq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
- tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
+ if (node.parent() instanceof AMemberPredicate
+ && !typeRestrictor.isARemovedNode(node.parent())) {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1_ELEMENT_OF);
+ } else {
+ tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
+ }
} else {
if (node.parent() instanceof AMemberPredicate
&& !typeRestrictor.isARemovedNode(node.parent())) {
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 6be0cea..1e3932f 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -55,7 +55,7 @@ public class TLCOutputInfo {
this.constants = machineContext.getConstants().keySet();
this.hasInit = tlaModule.getInitPredicates().size() > 0;
- if (machineContext.originallyHadConstants()) {
+ if (machineContext.constantSetupInTraceFile()) {
this.constantSetup = true;
}
diff --git a/src/main/resources/standardModules/SequencesAsRelations.tla b/src/main/resources/standardModules/SequencesAsRelations.tla
index e97b035..af607c3 100644
--- a/src/main/resources/standardModules/SequencesAsRelations.tla
+++ b/src/main/resources/standardModules/SequencesAsRelations.tla
@@ -28,10 +28,23 @@ LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinali
RelISeq(S) == {{<<n, x[n]>>:n \in 1..Len(x)} :x \in ISeq(S)}
\* The set of all injective sequences with elements of S
+
+RelISeqEleOf(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
+ IN /\ Cardinality(p) = Cardinality(d)
+ /\ d = 1..Cardinality(d)
+ /\ Cardinality(p) = Cardinality(RelRange(p))}
RelISeq1(S) == RelISeq(S) \ {{}}
\* The set of all non-empty injective sequences with elements of S
+RelISeq1EleOf(S) == {p \in SUBSET(Nat \times S):
+ LET d == {q[1] : q \in p}
+ IN /\ Cardinality(p) > 0
+ /\ Cardinality(p) = Cardinality(d)
+ /\ d = 1..Cardinality(d)
+ /\ Cardinality(p) = Cardinality(RelRange(p))}
+
LOCAL SeqTest(s) == RelDomain(s) = 1..Cardinality(s)
\* Testing if s is a sequence
--
GitLab