From 62a0cd454f41c1711c892f300e36c5542033a927 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 19 May 2015 14:24:32 +0200
Subject: [PATCH] shortened the translation of the deadlock operator
---
src/main/java/de/tlc4b/TLC4B.java | 4 +++
.../java/de/tlc4b/ltl/LTLFormulaPrinter.java | 30 ++++-------------
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 2 +-
src/main/java/de/tlc4b/tlc/TLCResults.java | 33 ++++++++++++++-----
.../java/de/tlc4b/ltl/LtlFormulaTest.java | 4 +--
5 files changed, 38 insertions(+), 35 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 025dccb..d95d1da 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -110,6 +110,10 @@ public class TLC4B {
System.out.println("Transitions fired: "
+ results.getNumberOfTransitions());
System.out.println("Result: " + results.getResultString());
+ String violatedDefinition = results.getViolatedDefinition();
+ if (violatedDefinition != null) {
+ System.out.print("Violated Definition: " + violatedDefinition);
+ }
if (results.hasTrace() && createTraceFile) {
String trace = results.getTrace();
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index 564bcfd..25d8404 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -185,8 +185,8 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
List<PActions> copy = new ArrayList<PActions>(node.getArgs());
for (int i = 0; i < copy.size(); i++) {
AOpActions action1 = (AOpActions) copy.get(i);
- for (int j = i+1; j < copy.size(); j++) {
- if(! (i == 0 && j == 1)){
+ for (int j = i + 1; j < copy.size(); j++) {
+ if (!(i == 0 && j == 1)) {
tlaPrinter.moduleStringAppend(" /\\ ");
}
tlaPrinter.moduleStringAppend("\\neg(ENABLED(");
@@ -199,25 +199,9 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
}
}
-
- @Override
- public void caseADeadlockLtl(ADeadlockLtl node)
- {
- tlaPrinter.moduleStringAppend("\\neg(");
-
-
- Iterator<POperation> itr = this.tlaPrinter.getTLAModule().getOperations().iterator();
- while (itr.hasNext()) {
- Node operation = itr.next();
- tlaPrinter.moduleStringAppend("ENABLED(");
- tlaPrinter.printOperationCall(operation);
- tlaPrinter.moduleStringAppend(")");
- if (itr.hasNext()) {
- tlaPrinter.moduleStringAppend(" \\/ ");
- }
- }
-
- tlaPrinter.moduleStringAppend(")");
- }
-
+ @Override
+ public void caseADeadlockLtl(ADeadlockLtl node) {
+ tlaPrinter.moduleStringAppend("\\neg(ENABLED(Next))");
+ }
+
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 9903b94..f5a381b 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -523,7 +523,7 @@ public class TLAPrinter extends DepthFirstAdapter {
moduleStringAppend("\n");
}
- public void printOperationCall(Node operation) {
+ private void printOperationCall(Node operation) {
AOperation op = (AOperation) operation;
List<PExpression> newList = new ArrayList<PExpression>();
newList.addAll(op.getParameters());
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 62bb3fa..a2d4ad2 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -14,6 +14,7 @@ import tlc2.tool.TLCStateInfo;
public class TLCResults {
private TLCResult tlcResult;
+ private String violatedDefinition;
private Date startTime;
private Date endTime;
@@ -46,12 +47,16 @@ public class TLCResults {
return traceString;
}
+ public String getViolatedDefinition() {
+ return violatedDefinition;
+ }
+
public int getNumberOfTransitions() {
return numberOfTransitions;
}
public int getModelCheckingTime() {
- if(endTime == null || startTime == null){
+ if (endTime == null || startTime == null) {
return -1;
}
return (int) (endTime.getTime() - startTime.getTime()) / 1000;
@@ -149,12 +154,14 @@ public class TLCResults {
}
private void evalErrorMessage(Message m) {
-// System.out.println(------------------);
-// System.out.print(m.getMessageCode() + " " + m.getParameters().length);
-// for (int i = 0; i < m.getParameters().length; i++) {
-// System.out.print(" " + m.getParameters()[i]);
-// }
-// System.out.println();
+ // System.out.println(------------------);
+ // System.out.print(m.getMessageCode() + " " +
+ // m.getParameters().length);
+ // for (int i = 0; i < m.getParameters().length; i++) {
+ // System.out.print(" " + m.getParameters()[i]);
+ // }
+ // System.out.println();
+
switch (m.getMessageCode()) {
case EC.TLC_INVARIANT_VIOLATED_INITIAL:
case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR:
@@ -162,15 +169,20 @@ public class TLCResults {
tlcResult = AssertionError;
} else if (m.getParameters()[0].equals("NotGoal")) {
tlcResult = Goal;
+ } else if (m.getParameters()[0].startsWith("ASSERT_LTL")) {
+ tlcResult = TemporalPropertyViolation;
} else {
- tlcResult = TLCResult.InvariantViolation;
+ tlcResult = InvariantViolation;
+ }
+ if (m.getParameters().length > 0) {
+ violatedDefinition = m.getParameters()[0];
}
break;
case EC.TLC_INITIAL_STATE: {
String arg1 = m.getParameters()[0];
if (arg1.contains("Attempted to compute the number of elements in the overridden")) {
-
+ // TODO
}
tlcResult = EnumerationError;
return;
@@ -186,6 +198,9 @@ public class TLCResults {
case EC.TLC_TEMPORAL_PROPERTY_VIOLATED:
tlcResult = TLCResult.TemporalPropertyViolation;
+ if (m.getParameters().length > 0) {
+ violatedDefinition = m.getParameters()[0];
+ }
break;
case EC.TLC_ASSUMPTION_EVALUATION_ERROR:
diff --git a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
index 5647ff5..a8c982b 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -191,7 +191,7 @@ public class LtlFormulaTest {
String machine = "MACHINE test\n"
+ "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
+ "END";
- String expected = "\\neg(ENABLED(foo) \\/ ENABLED(bar) \\/ ENABLED(bazz))";
+ String expected = "\\neg(ENABLED(Next))";
compareLTLFormula(expected, machine, "deadlock");
}
@@ -200,7 +200,7 @@ public class LtlFormulaTest {
String machine = "MACHINE test\n"
+ "OPERATIONS foo(a) = SELECT a : 1..3 THEN skip END\n"
+ "END";
- String expected = "\\neg(ENABLED(\\E a \\in (1 .. 3) : foo(a)))";
+ String expected = "\\neg(ENABLED(Next))";
compareLTLFormula(expected, machine, "deadlock");
}
--
GitLab