From 7050476a83e7f804d02e2c0e1051770641ccc927 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 19 May 2015 13:06:36 +0200
Subject: [PATCH] added deadlock operator
---
.../java/de/tlc4b/ltl/LTLFormulaPrinter.java | 26 +++++++++++++++++--
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 8 ++++--
.../java/de/tlc4b/ltl/LtlFormulaTest.java | 18 +++++++++++++
3 files changed, 48 insertions(+), 4 deletions(-)
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index 0f5546f..564bcfd 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -1,15 +1,18 @@
package de.tlc4b.ltl;
import java.util.ArrayList;
+import java.util.Iterator;
import java.util.List;
import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.POperation;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
import de.be4.ltl.core.parser.node.AAndFair1Ltl;
import de.be4.ltl.core.parser.node.AAndFair2Ltl;
import de.be4.ltl.core.parser.node.AAndLtl;
+import de.be4.ltl.core.parser.node.ADeadlockLtl;
import de.be4.ltl.core.parser.node.ADetLtl;
import de.be4.ltl.core.parser.node.AEnabledLtl;
import de.be4.ltl.core.parser.node.AExistsLtl;
@@ -194,8 +197,27 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
tlaPrinter.moduleStringAppend("))");
}
}
-
-
}
+
+ @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(")");
+ }
+
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 1b60e57..9903b94 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");
}
- private void printOperationCall(Node operation) {
+ public void printOperationCall(Node operation) {
AOperation op = (AOperation) operation;
List<PExpression> newList = new ArrayList<PExpression>();
newList.addAll(op.getParameters());
@@ -2908,7 +2908,11 @@ public class TLAPrinter extends DepthFirstAdapter {
}
public String geTranslatedLTLFormula() {
- return translatedLTLFormula.toString();
+ return this.translatedLTLFormula.toString();
}
+ public TLAModule getTLAModule(){
+ return this.tlaModule;
+ }
+
}
diff --git a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
index 35465bd..5647ff5 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -186,6 +186,24 @@ public class LtlFormulaTest {
compareLTLFormula(expected, machine, "deterministic(foo,bar,bazz)");
}
+ @Test
+ public void testDeadlock() throws Exception {
+ String machine = "MACHINE test\n"
+ + "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
+ + "END";
+ String expected = "\\neg(ENABLED(foo) \\/ ENABLED(bar) \\/ ENABLED(bazz))";
+ compareLTLFormula(expected, machine, "deadlock");
+ }
+
+ @Test
+ public void testDeadlockOperationParameter() throws Exception {
+ 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)))";
+ compareLTLFormula(expected, machine, "deadlock");
+ }
+
@Test
public void testWeakFairness() throws Exception {
String machine = "MACHINE test\n"
--
GitLab