Skip to content
Snippets Groups Projects
Commit dd2cb7fa authored by hansen's avatar hansen
Browse files

added support for the deterministic operator (LTL operator)

parent 20fbf7e2
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 768 additions and 792 deletions
src/main/java/de/tlc4b/TLC4BGlobals.java
+ 0
− 1
View file @ dd2cb7fa
...@@ -69,7 +69,6 @@ public class TLC4BGlobals { ...@@ -69,7 +69,6 @@ public class TLC4BGlobals {
runTestscript = false; runTestscript = false;
testingMode = false; testingMode = false;
createTraceFile = true; createTraceFile = true;
} }
public static boolean isCreateTraceFile() { public static boolean isCreateTraceFile() {
......
src/main/java/de/tlc4b/Translator.java
+ 7
− 0
View file @ dd2cb7fa
...@@ -41,6 +41,7 @@ public class Translator { ...@@ -41,6 +41,7 @@ public class Translator {
private PPredicate constantsSetup; private PPredicate constantsSetup;
private ArrayList<STANDARD_MODULES> usedStandardModules; private ArrayList<STANDARD_MODULES> usedStandardModules;
private TLCOutputInfo tlcOutputInfo; private TLCOutputInfo tlcOutputInfo;
private String translatedLTLFormula;
public Translator(String machineString) throws BException { public Translator(String machineString) throws BException {
this.machineString = machineString; this.machineString = machineString;
...@@ -158,6 +159,7 @@ public class Translator { ...@@ -158,6 +159,7 @@ public class Translator {
printer.start(); printer.start();
moduleString = printer.getStringbuilder().toString(); moduleString = printer.getStringbuilder().toString();
configString = printer.getConfigString().toString(); configString = printer.getConfigString().toString();
translatedLTLFormula = printer.geTranslatedLTLFormula();
tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker, tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker,
generator.getTlaModule(), generator.getConfigFile()); generator.getTlaModule(), generator.getConfigFile());
...@@ -195,4 +197,9 @@ public class Translator { ...@@ -195,4 +197,9 @@ public class Translator {
return usedStandardModules; return usedStandardModules;
} }
public String getTranslatedLTLFormula(){
return translatedLTLFormula;
}
} }
src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+ 43
− 19
View file @ dd2cb7fa
package de.tlc4b.ltl; package de.tlc4b.ltl;
import java.util.ArrayList;
import java.util.List;
import de.be4.classicalb.core.parser.node.APredicateParseUnit; import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.Node; import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start; import de.be4.classicalb.core.parser.node.Start;
...@@ -7,6 +10,7 @@ import de.be4.ltl.core.parser.analysis.DepthFirstAdapter; ...@@ -7,6 +10,7 @@ import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
import de.be4.ltl.core.parser.node.AAndFair1Ltl; import de.be4.ltl.core.parser.node.AAndFair1Ltl;
import de.be4.ltl.core.parser.node.AAndFair2Ltl; import de.be4.ltl.core.parser.node.AAndFair2Ltl;
import de.be4.ltl.core.parser.node.AAndLtl; import de.be4.ltl.core.parser.node.AAndLtl;
import de.be4.ltl.core.parser.node.ADetLtl;
import de.be4.ltl.core.parser.node.AEnabledLtl; import de.be4.ltl.core.parser.node.AEnabledLtl;
import de.be4.ltl.core.parser.node.AExistsLtl; import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AFairnessImplicationLtl; import de.be4.ltl.core.parser.node.AFairnessImplicationLtl;
...@@ -16,11 +20,13 @@ import de.be4.ltl.core.parser.node.AForallLtl; ...@@ -16,11 +20,13 @@ import de.be4.ltl.core.parser.node.AForallLtl;
import de.be4.ltl.core.parser.node.AGloballyLtl; import de.be4.ltl.core.parser.node.AGloballyLtl;
import de.be4.ltl.core.parser.node.AImpliesLtl; import de.be4.ltl.core.parser.node.AImpliesLtl;
import de.be4.ltl.core.parser.node.ANotLtl; import de.be4.ltl.core.parser.node.ANotLtl;
import de.be4.ltl.core.parser.node.AOpActions;
import de.be4.ltl.core.parser.node.AOrLtl; import de.be4.ltl.core.parser.node.AOrLtl;
import de.be4.ltl.core.parser.node.AStrongFairLtl; import de.be4.ltl.core.parser.node.AStrongFairLtl;
import de.be4.ltl.core.parser.node.ATrueLtl; import de.be4.ltl.core.parser.node.ATrueLtl;
import de.be4.ltl.core.parser.node.AUnparsedLtl; import de.be4.ltl.core.parser.node.AUnparsedLtl;
import de.be4.ltl.core.parser.node.AWeakFairLtl; import de.be4.ltl.core.parser.node.AWeakFairLtl;
import de.be4.ltl.core.parser.node.PActions;
import de.tlc4b.analysis.typerestriction.TypeRestrictor; import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.prettyprint.TLAPrinter; import de.tlc4b.prettyprint.TLAPrinter;
...@@ -36,9 +42,7 @@ public class LTLFormulaPrinter extends DepthFirstAdapter { ...@@ -36,9 +42,7 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
this.tlaPrinter = tlaPrinter; this.tlaPrinter = tlaPrinter;
this.typeRestrictor = typeRestrictor; this.typeRestrictor = typeRestrictor;
ltlFormulaVisitor.getLTLFormulaStart().apply(this); ltlFormulaVisitor.getLTLFormulaStart().apply(this);
} }
@Override @Override
...@@ -78,16 +82,14 @@ public class LTLFormulaPrinter extends DepthFirstAdapter { ...@@ -78,16 +82,14 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
} }
@Override @Override
public void caseAAndFair1Ltl(AAndFair1Ltl node) public void caseAAndFair1Ltl(AAndFair1Ltl node) {
{
node.getLeft().apply(this); node.getLeft().apply(this);
tlaPrinter.moduleStringAppend(" /\\ "); tlaPrinter.moduleStringAppend(" /\\ ");
node.getRight().apply(this); node.getRight().apply(this);
} }
@Override @Override
public void caseAAndFair2Ltl(AAndFair2Ltl node) public void caseAAndFair2Ltl(AAndFair2Ltl node) {
{
node.getLeft().apply(this); node.getLeft().apply(this);
tlaPrinter.moduleStringAppend(" /\\ "); tlaPrinter.moduleStringAppend(" /\\ ");
node.getRight().apply(this); node.getRight().apply(this);
...@@ -130,7 +132,8 @@ public class LTLFormulaPrinter extends DepthFirstAdapter { ...@@ -130,7 +132,8 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
@Override @Override
public void caseAWeakFairLtl(AWeakFairLtl node) { public void caseAWeakFairLtl(AWeakFairLtl node) {
tlaPrinter.printWeakFairnessWithParameter(node.getOperation().getText()); tlaPrinter
.printWeakFairnessWithParameter(node.getOperation().getText());
} }
@Override @Override
...@@ -174,4 +177,25 @@ public class LTLFormulaPrinter extends DepthFirstAdapter { ...@@ -174,4 +177,25 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
node.getLtl().apply(this); node.getLtl().apply(this);
} }
@Override
public void caseADetLtl(ADetLtl node) {
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)){
tlaPrinter.moduleStringAppend(" /\\ ");
}
tlaPrinter.moduleStringAppend("\\neg(ENABLED(");
tlaPrinter.moduleStringAppend(action1.getOperation().getText());
tlaPrinter.moduleStringAppend("), ENABLED(");
AOpActions action2 = (AOpActions) copy.get(j);
tlaPrinter.moduleStringAppend(action2.getOperation().getText());
tlaPrinter.moduleStringAppend("))");
}
}
}
} }
src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+ 17
− 0
View file @ dd2cb7fa
...@@ -21,6 +21,7 @@ import de.be4.ltl.core.parser.internal.LtlLexer; ...@@ -21,6 +21,7 @@ import de.be4.ltl.core.parser.internal.LtlLexer;
import de.be4.ltl.core.parser.lexer.Lexer; import de.be4.ltl.core.parser.lexer.Lexer;
import de.be4.ltl.core.parser.lexer.LexerException; import de.be4.ltl.core.parser.lexer.LexerException;
import de.be4.ltl.core.parser.node.AActionLtl; import de.be4.ltl.core.parser.node.AActionLtl;
import de.be4.ltl.core.parser.node.AAndLtl;
import de.be4.ltl.core.parser.node.AEnabledLtl; import de.be4.ltl.core.parser.node.AEnabledLtl;
import de.be4.ltl.core.parser.node.AExistsLtl; import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl; import de.be4.ltl.core.parser.node.AForallLtl;
...@@ -293,4 +294,20 @@ public class LTLFormulaVisitor extends DepthFirstAdapter { ...@@ -293,4 +294,20 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
"The '[...]' operator is not supported by TLC."); "The '[...]' operator is not supported by TLC.");
} }
@Override
public void caseAAndLtl(AAndLtl node)
{
inAAndLtl(node);
if(node.getLeft() != null)
{
node.getLeft().apply(this);
}
if(node.getRight() != null)
{
node.getRight().apply(this);
System.out.println(node.getRight().getClass());
}
outAAndLtl(node);
}
} }
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+ 608
− 594
View file @ dd2cb7fa
This diff is collapsed.
src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+ 86
− 173
View file @ dd2cb7fa
...@@ -2,17 +2,25 @@ package de.tlc4b.ltl; ...@@ -2,17 +2,25 @@ package de.tlc4b.ltl;
import static de.tlc4b.util.TestUtil.compareEqualsConfig; import static de.tlc4b.util.TestUtil.compareEqualsConfig;
import static de.tlc4b.util.TestUtil.compareLTL; import static de.tlc4b.util.TestUtil.compareLTLFormula;
import org.junit.BeforeClass;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.exceptions.LTLParseException;
import de.tlc4b.exceptions.ScopeException; import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.exceptions.TypeErrorException; import de.tlc4b.exceptions.TypeErrorException;
public class LtlFormulaTest { public class LtlFormulaTest {
@BeforeClass
public static void setUp(){
TLC4BGlobals.setTestingMode(true);
}
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testScopeException() throws Exception { public void testScopeException() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
...@@ -21,7 +29,7 @@ public class LtlFormulaTest { ...@@ -21,7 +29,7 @@ public class LtlFormulaTest {
+ "INITIALISATION x := 1\n" + "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1" + "OPERATIONS foo = x := 1"
+ "END"; + "END";
compareLTL("", machine, "G{y = 1}"); compareLTLFormula("", machine, "G{y = 1}");
} }
@Test (expected = TypeErrorException.class) @Test (expected = TypeErrorException.class)
...@@ -32,234 +40,164 @@ public class LtlFormulaTest { ...@@ -32,234 +40,164 @@ public class LtlFormulaTest {
+ "INITIALISATION x := 1\n" + "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1" + "OPERATIONS foo = x := 1"
+ "END"; + "END";
compareLTL("", machine, "G{x = FALSE}"); compareLTLFormula("", machine, "G{x = FALSE}");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testUnkownOperation() throws Exception { public void testUnkownOperation() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "END"; + "END";
compareLTL("", machine, "e(foo)"); compareLTLFormula("", machine, "e(foo)");
} }
@Ignore
@Test @Test
public void testGobally() throws Exception { public void testGobally() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "VARIABLES x\n" compareLTLFormula("[](1 = 1)", machine, "G{1 = 1}");
+ "INVARIANT x = 1\n"
+ "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1"
+ "END";
String expected = "---- MODULE test ----\n"
+ "VARIABLES x\n"
+ "Invariant == x = 1\n"
+ "Init == x = 1\n"
+ "foo == x' = 1\n\n"
+ "Next == \\/ foo\n"
+ "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ "ltl == [](x = 1)\n"
+ "====";
compareLTL(expected, machine, "G{x = 1}");
} }
@Ignore
@Test @Test
public void testFinally() throws Exception { public void testFinally() throws Exception {
String machine = "MACHINE test END";
compareLTLFormula("<>(1=1)", machine, "F{1 = 1}");
}
@Test
public void testEnabled() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "VARIABLES x\n" + "OPERATIONS foo = skip \n"
+ "INVARIANT x = 1\n"
+ "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1"
+ "END"; + "END";
compareLTLFormula("ENABLED(foo)", machine, "e(foo)");
}
String expected = "---- MODULE test ----\n" @Test (expected = ScopeException.class)
+ "VARIABLES x\n" public void testEnabledUnknownOperation() throws Exception {
+ "Invariant == x = 1\n" String machine = "MACHINE test END";
+ "Init == x = 1\n" compareLTLFormula("ENABLED(foo)", machine, "e(foo)");
+ "foo == x' = 1\n\n"
+ "Next == \\/ foo\n"
+ "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ "ltl == <>(x = 1)\n"
+ "====";
compareLTL(expected, machine, "F{x = 1}");
} }
@Test @Test
public void testTrue() throws Exception { public void testTrue() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("TRUE", machine, "true");
String expected = "---- MODULE test ----\n"
+ "ltl == TRUE\n"
+ "====";
compareLTL(expected, machine, "true");
} }
@Test @Test
public void testFalse() throws Exception { public void testFalse() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("FALSE", machine, "false");
String expected = "---- MODULE test ----\n"
+ "ltl == FALSE\n"
+ "====";
compareLTL(expected, machine, "false");
} }
@Test @Test
public void testImplication() throws Exception { public void testImplication() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("FALSE => TRUE", machine, "false => true");
String expected = "---- MODULE test ----\n"
+ "ltl == FALSE => TRUE\n"
+ "====";
compareLTL(expected, machine, "false => true");
} }
@Test @Test
public void testAnd() throws Exception { public void testAnd() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("TRUE /\\ FALSE", machine, "true & false");
String expected = "---- MODULE test ----\n"
+ "ltl == TRUE /\\ FALSE\n"
+ "====";
compareLTL(expected, machine, "true & false");
} }
@Test @Test
public void testOr() throws Exception { public void testOr() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("TRUE \\/ FALSE", machine, "true or false");
String expected = "---- MODULE test ----\n"
+ "ltl == TRUE \\/ FALSE\n"
+ "====";
compareLTL(expected, machine, "true or false");
} }
@Test @Test
public void testNegation() throws Exception { public void testNegation() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("\\neg(TRUE)", machine, "not(true)");
String expected = "---- MODULE test ----\n"
+ "ltl == \\neg(TRUE)\n"
+ "====";
compareLTL(expected, machine, "not(true)");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testUntil() throws Exception { public void testUntil() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "true U false");
compareLTL("", machine, "true U false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testWeakUntil() throws Exception { public void testWeakUntil() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "true W false");
compareLTL("", machine, "true W false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testRelease() throws Exception { public void testRelease() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "true R false");
compareLTL("", machine, "true R false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testHistory() throws Exception { public void testHistory() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "H false");
compareLTL("", machine, "H false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testOnce() throws Exception { public void testOnce() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "O false");
compareLTL("", machine, "O false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testYesterday() throws Exception { public void testYesterday() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "Y false");
compareLTL("", machine, "Y false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testSince() throws Exception { public void testSince() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "true S false");
compareLTL("", machine, "true S false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testTrigger() throws Exception { public void testTrigger() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("", machine, "true T false");
compareLTL("", machine, "true T false");
} }
@Test (expected = ScopeException.class) @Test (expected = ScopeException.class)
public void testAction() throws Exception { public void testAction() throws Exception {
String machine = "MACHINE test END";
compareLTLFormula("", machine, "[foo]");
}
@Test (expected = LTLParseException.class)
public void testWeakFairnessParseError() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "OPERATIONS foo = skip\n"
+ "END"; + "END";
compareLTL("", machine, "[foo]"); compareLTLFormula("", machine, "WF(foo)");
} }
@Ignore
@Test @Test
public void testEnabled() throws Exception { public void testDeterministic() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "VARIABLES x\n" + "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
+ "INVARIANT x = 1\n"
+ "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1"
+ "END"; + "END";
String expected = "\\neg(ENABLED(foo),ENABLED(bar))/\\ \\neg(ENABLED(foo),ENABLED(bazz))/\\ \\neg(ENABLED(bar),ENABLED(bazz))";
String expected = "---- MODULE test ----\n" compareLTLFormula(expected, machine, "deterministic(foo,bar,bazz)");
+ "VARIABLES x\n"
+ "Invariant == x = 1\n"
+ "Init == x = 1\n"
+ "foo == x' = 1\n\n"
+ "Next == \\/ foo\n"
+ "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ "ltl == ENABLED(foo)\n"
+ "====";
compareLTL(expected, machine, "e(foo)");
} }
@Ignore
@Test @Test
public void testWeakFairness() throws Exception { public void testWeakFairness() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "VARIABLES x\n" + "VARIABLES x\n"
+ "INVARIANT x = 1\n" + "INVARIANT x = 1\n"
+ "INITIALISATION x := 1\n" + "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1" + "OPERATIONS foo = skip\n"
+ "END"; + "END";
String expected = "([]<><<foo>>_vars\\/[]<>~ENABLED(foo)\\/[]<>ENABLED(foo/\\x'=x))=>TRUE";
String expected = "---- MODULE test ----\n" compareLTLFormula(expected, machine, "WF(foo) => true");
+ "VARIABLES x\n"
+ "Invariant == x = 1\n"
+ "Init == x = 1\n"
+ "foo == x' = 1\n\n"
+ "Next == \\/ foo\n"
+ "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ "ltl == ENABLED(foo)\n"
+ "====";
compareLTL(expected, machine, "WF(foo)");
} }
@Ignore
@Test @Test
public void testStrongFairness() throws Exception { public void testStrongFairness() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
...@@ -268,57 +206,32 @@ public class LtlFormulaTest { ...@@ -268,57 +206,32 @@ public class LtlFormulaTest {
+ "INITIALISATION x := 1\n" + "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1" + "OPERATIONS foo = x := 1"
+ "END"; + "END";
String expected = "([]<><<foo>>_vars\\/<>[]~ENABLED(foo)\\/[]<>ENABLED(foo/\\x'=x))=>TRUE";
String expected = "---- MODULE test ----\n" compareLTLFormula(expected, machine, "SF(foo) => true");
+ "VARIABLES x\n"
+ "Invariant == x = 1\n"
+ "Init == x = 1\n"
+ "foo == x' = 1\n\n"
+ "Next == \\/ foo\n"
+ "Spec == Init /\\ [][Next]_<<x>> /\\ WF_<<x>>(Next)\n"
+ "ltl == ENABLED(foo)\n"
+ "====";
compareLTL(expected, machine, "SF(foo)");
} }
@Test @Test
public void testExistentialQuantification() throws Exception { public void testExistentialQuantification() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula(" \\E p \\in {1}: p = 1", machine, "#p.({p=1} & {p = 1})");
String expected = "---- MODULE test ----\n"
+ "ltl == \\E p \\in {1}: p = 1\n"
+ "====";
compareLTL(expected, machine, "#p.({p=1} & {p = 1})");
} }
@Test @Test
public void testExistentialQuantification2() throws Exception { public void testExistentialQuantification2() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("\\E p \\in {1}: 1 = 1 /\\ p = 1", machine, "#p.({p=1 & 1 = 1} & {p = 1})");
String expected = "---- MODULE test ----\n"
+ "ltl == \\E p \\in {1}: 1 = 1 /\\ p = 1\n"
+ "====";
compareLTL(expected, machine, "#p.({p=1 & 1 = 1} & {p = 1})");
} }
@Test @Test
public void testForallQuantification() throws Exception { public void testForallQuantification() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("\\A p \\in {1}: p = 1", machine, "!p.({p=1} => {p = 1})");
String expected = "---- MODULE test ----\n"
+ "ltl == \\A p \\in {1}: p = 1\n"
+ "====";
compareLTL(expected, machine, "!p.({p=1} => {p = 1})");
} }
@Test @Test
public void testForallQuantification2() throws Exception { public void testForallQuantification2() throws Exception {
String machine = "MACHINE test\n" String machine = "MACHINE test END";
+ "END"; compareLTLFormula("\\A p \\in {1}: 1 = 1 => p = 1", machine, "!p.({p=1 & 1=1 } => {p = 1})");
String expected = "---- MODULE test ----\n"
+ "ltl == \\A p \\in {1}: 1 = 1 => p = 1\n"
+ "====";
compareLTL(expected, machine, "!p.({p=1 & 1=1 } => {p = 1})");
} }
@Ignore @Ignore
......
src/test/java/de/tlc4b/util/TestUtil.java
+ 7
− 5
View file @ dd2cb7fa
...@@ -64,15 +64,17 @@ public class TestUtil { ...@@ -64,15 +64,17 @@ public class TestUtil {
tlaString, configString); tlaString, configString);
} }
public static void compareLTL(String expectedModule, String machine,
public static void compareLTLFormula(String expected, String machine,
String ltlFormula) throws Exception { String ltlFormula) throws Exception {
Translator b2tlaTranslator = new Translator(machine, ltlFormula); Translator b2tlaTranslator = new Translator(machine, ltlFormula);
b2tlaTranslator.translate(); b2tlaTranslator.translate();
String translatedLTLFormula = b2tlaTranslator.getTranslatedLTLFormula();
translatedLTLFormula = translatedLTLFormula.replaceAll("\\s", "");
expected = expected.replaceAll("\\s", "");
System.out.println(translatedLTLFormula);
System.out.println(b2tlaTranslator.getModuleString()); System.out.println(b2tlaTranslator.getModuleString());
// String name = b2tlaTranslator.getMachineName(); assertEquals(expected, translatedLTLFormula);
// de.tla2b.translation.Tla2BTranslator.translateString(name,
// b2tlaTranslator.getModuleString(), null);
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
} }
public static void checkMachine(String machine) throws Exception { public static void checkMachine(String machine) throws Exception {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment