Package net.automatalib.modelchecker.m3c.formula.parser

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"] | "_")*
 

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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 a String. Each atomic proposition is transformed to a String.

Parameters:

formula - ctl or mu-calculus formula to be parsed

Returns:

formula's abstract syntax tree.

Throws:

ParseException - if formula 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 type

AP - atomic proposition type

Parameters:

formula - ctl or mu-calculus formula to be parsed

labelParser - parser to transform the labels of the formula

apParser - parser to transform the atomic propositions of the formula

Returns:

formula's abstract syntax tree.

Throws:

ParseException - if formula is not a valid formula.