Class M3CParser
- java.lang.Object
-
- net.automatalib.modelchecker.m3c.formula.parser.M3CParser
-
public final class M3CParser extends Object
This class can be used to parse formulas in CTL and the mu-calculus.-
CTL grammar:
f := true | false | AP | (f) | !f | f && f | f || f | f -> f | f <-> f | <>f | <ID>f | []f | [ID]f | AF f | AG f | A(f U f) | A(f W f) | EF f | EG f | E(f U f) | E(f W f)
-
mu-calculus grammar:
f := true | false | AP | (f) | !f | f && f | f || f | f -> f | f <-> f | <>f | <ID>f | []f | [ID]f | mu ID.(f) | nu ID.(f) | ID
AP := "arbitrary string not containing double quotation marks" | 'arbitrary string not containing single quotation marks' ID := ["a"-"z","A"-"Z"] (["a"-"z","A"-"Z"] | ["0"-"9"] | "_")*
-
CTL grammar:
-
-
Method Summary
All Methods Static Methods Concrete Methods Modifier and Type Method Description static FormulaNode<String,String>
parse(String formula)
Returns the abstract syntax tree of a given formula.static <L,AP>
FormulaNode<L,AP>parse(String formula, Function<String,L> labelParser, Function<String,AP> apParser)
Returns the abstract syntax tree of a given formula.
-
-
-
Method Detail
-
parse
public static FormulaNode<String,String> parse(String formula) throws ParseException
Returns the abstract syntax tree of a given formula. Each label is transformed to aString
. Each atomic proposition is transformed to aString
.- Parameters:
formula
- ctl or mu-calculus formula to be parsed- Returns:
formula
's abstract syntax tree.- Throws:
ParseException
- ifformula
is not a valid formula.
-
parse
public static <L,AP> FormulaNode<L,AP> parse(String formula, Function<String,L> labelParser, Function<String,AP> apParser) throws ParseException
Returns the abstract syntax tree of a given formula. Each label and atomic proposition is transformed according to the given parsers.- Type Parameters:
L
- edge label typeAP
- atomic proposition type- Parameters:
formula
- ctl or mu-calculus formula to be parsedlabelParser
- parser to transform the labels of the formulaapParser
- parser to transform the atomic propositions of the formula- Returns:
formula
's abstract syntax tree.- Throws:
ParseException
- ifformula
is not a valid formula.
-
-