Skip to content

Commit

Permalink
m3c: allow tokens as action labels
Browse files Browse the repository at this point in the history 
Closes #70.
  • Loading branch information
@mtf90
mtf90 committed Feb 8, 2024
1 parent 63210a8 commit e96f7ec
Show file tree
Hide file tree
Showing 3 changed files with 65 additions and 10 deletions.
28 changes: 25 additions & 3 deletions modelchecking/m3c/src/main/javacc/M3C.jj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ PARSER_END(InternalM3CParser)
| < IMPLICATION: "->" >
| < ID: ["a"-"z","A"-"Z"] (["a"-"z","A"-"Z"] | ["0"-"9"] | "_")* >
| < STRING_LITERAL: ("'" (~["'", "\\"])* (("\\\'" | "\\\\") (~["'", "\\"])*)* "'")
| ("\"" (~["\"", "\\"])* (("\\\"" | "\\\\") (~["\"", "\\"])*)* "\"")>
| ("\"" (~["\"", "\\"])* (("\\\"" | "\\\\") (~["\"", "\\"])*)* "\"")>
}

FormulaNode<L, AP> parse(Function<String, L> labelParser, Function<String, AP> apParser):
Expand Down Expand Up @@ -213,8 +213,8 @@ private FormulaNode<L, AP> unary():
| <AG> child=unary() {return new AGNode<L, AP>(child);}
| <EF> child=unary() {return new EFNode<L, AP>(child);}
| <EG> child=unary() {return new EGNode<L, AP>(child);}
| <LABRACKET> (action=<ID>)? <RABRACKET> child=unary() {return new DiamondNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
| <LBRACKET> (action=<ID>)? <RBRACKET> child=unary() {return new BoxNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
| <LABRACKET> (action=action())? <RABRACKET> child=unary() {return new DiamondNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
| <LBRACKET> (action=action())? <RBRACKET> child=unary() {return new BoxNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
| child=element() {return child;}
}

Expand Down Expand Up @@ -260,3 +260,25 @@ private FormulaNode<L, AP> element():
| <FALSE> {return new FalseNode<L, AP>();}
| <LPAREN> node=formula() <RPAREN> {return node;}
}

/*
* We cannot parse <ID> only, because the input may have been greedily parsed as a different token before.
*/
private Token action():
{
Token action;
}
{
(action=<ALL>
| action=<EXISTS>
| action=<AF>
| action=<AG>
| action=<EF>
| action=<EG>
| action=<UNTIL>
| action=<WUNTIL>
| action=<NU>
| action=<MU>
| action=<ID>) { return action; }
}

34 changes: 27 additions & 7 deletions ...king/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserCTLTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,12 +71,24 @@ public void baseCasesTest() throws ParseException {
assertEquals("[c]true", new BoxNode<>("c", new TrueNode<>()));
}

private void assertEquals(String ctlFormula, FormulaNode<String, String> expectedAST) throws ParseException {
FormulaNode<String, String> actualAST = M3CParser.parse(ctlFormula);
Assert.assertEquals(actualAST, expectedAST);
Assert.assertEquals(actualAST.hashCode(), expectedAST.hashCode());

this.formulas.add(actualAST);
@Test
public void tokensAsActionsTest() throws ParseException {
assertEquals("<A>true", new DiamondNode<>("A", new TrueNode<>()));
assertEquals("<AF>true", new DiamondNode<>("AF", new TrueNode<>()));
assertEquals("<AG>true", new DiamondNode<>("AG", new TrueNode<>()));
assertEquals("<E>true", new DiamondNode<>("E", new TrueNode<>()));
assertEquals("<EF>true", new DiamondNode<>("EF", new TrueNode<>()));
assertEquals("<EG>true", new DiamondNode<>("EG", new TrueNode<>()));
assertEquals("<U>true", new DiamondNode<>("U", new TrueNode<>()));
assertEquals("<W>true", new DiamondNode<>("W", new TrueNode<>()));
assertEquals("[A]true", new BoxNode<>("A", new TrueNode<>()));
assertEquals("[AF]true", new BoxNode<>("AF", new TrueNode<>()));
assertEquals("[AG]true", new BoxNode<>("AG", new TrueNode<>()));
assertEquals("[E]true", new BoxNode<>("E", new TrueNode<>()));
assertEquals("[EF]true", new BoxNode<>("EF", new TrueNode<>()));
assertEquals("[EG]true", new BoxNode<>("EG", new TrueNode<>()));
assertEquals("[U]true", new BoxNode<>("U", new TrueNode<>()));
assertEquals("[W]true", new BoxNode<>("W", new TrueNode<>()));
}

@Test
Expand All @@ -86,7 +98,7 @@ public void nestedFormulasTest() throws ParseException {
new AndNode<>(new FalseNode<>(), new FalseNode<>())));
}

@Test(dependsOnMethods = {"baseCasesTest", "nestedFormulasTest"})
@Test(dependsOnMethods = {"baseCasesTest", "tokensAsActionsTest", "nestedFormulasTest"})
public void testEqualities() {
for (FormulaNode<String, String> n1 : formulas) {
for (FormulaNode<String, String> n2 : formulas) {
Expand All @@ -104,6 +116,14 @@ public void testIllegalFormulas() {
assertIllegal("(mu X.(<b> true || <>X) || (AF true)");
}

private void assertEquals(String ctlFormula, FormulaNode<String, String> expectedAST) throws ParseException {
FormulaNode<String, String> actualAST = M3CParser.parse(ctlFormula);
Assert.assertEquals(actualAST, expectedAST);
Assert.assertEquals(actualAST.hashCode(), expectedAST.hashCode());

this.formulas.add(actualAST);
}

private void assertIllegal(String formula) {
Assert.assertThrows(ParseException.class, () -> M3CParser.parse(formula));
}
Expand Down
13 changes: 13 additions & 0 deletions ...g/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserMuCalcTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,19 @@ public void testBaseCases() throws ParseException {
new LfpNode<>("XY", new OrNode<>(new VariableNode<>("XY"), new FalseNode<>())));
assertEquals("nu ZY.(ZY || false)",
new GfpNode<>("ZY", new OrNode<>(new VariableNode<>("ZY"), new FalseNode<>())));
// allow CTL tokens as variable names as well
assertEquals("mu E.(E || false)",
new LfpNode<>("E", new OrNode<>(new VariableNode<>("E"), new FalseNode<>())));
assertEquals("nu AF.(AF || false)",
new GfpNode<>("AF", new OrNode<>(new VariableNode<>("AF"), new FalseNode<>())));
}

@Test
public void tokensAsActionsTest() throws ParseException {
assertEquals("<mu>true", new DiamondNode<>("mu", new TrueNode<>()));
assertEquals("<nu>true", new DiamondNode<>("nu", new TrueNode<>()));
assertEquals("[mu]true", new BoxNode<>("mu", new TrueNode<>()));
assertEquals("[nu]true", new BoxNode<>("nu", new TrueNode<>()));
}

@Test
Expand Down

0 comments on commit e96f7ec

Please sign in to comment.