public class LTLParser extends java.lang.Object implements LTLParserTreeConstants, LTLParserConstants
Modifier and Type | Field and Description |
---|---|
Token |
jj_nt |
protected org.processmining.plugins.ltlchecker.parser.JJTLTLParserState |
jjtree |
boolean |
lookingAhead |
Token |
token |
LTLParserTokenManager |
token_source |
JJTARG, JJTARGLIST, JJTATTRIBUTE, JJTATTRIBUTEDEFINITION, JJTBINARYPROPOSITION, JJTCOMPARISON, JJTCONCEPTSET, JJTDUMMYVAR, JJTEXPR, JJTFORMULACALL, JJTFORMULADEFINITION, JJTLITERAL, jjtNodeName, JJTPARSE, JJTPROPOSITION, JJTQUANTIFICATION, JJTRENAMING, JJTSTRINGLIST, JJTUNARYPROPOSITION, JJTVALUEATTRIBUTE, JJTVALUES
ASSIGN, ATEID, BAR, COLON, COMMA, DEFAULT, DESC_LITERAL, DIGIT, DOT, EOF, EQ, EXPONENT, GE, GT, ID, IDENTIFIER, IN_SINGLE_LINE_COMMENT, INTEGER_LITERAL, KAS, KATE, KDATE, KEXISTS, KFORALL, KFORMULA, KIN, KNUMBER, KPI, KRENAME, KSET, KSTRING, KSUBFORMULA, LALWAYS, LBRACE, LBRACKET, LE, LETTER, LEVENTUALLY, LNEXTTIME, LPAREN, LT, LUNTIL, MINUS, NE, PAND, PBIIMPLIES, PIID, PIMPLIES, PLUS, PNOT, POR, RBRACE, RBRACKET, REAL_LITERAL, REQ, RPAREN, SEMICOLON, SINGLE_LINE_COMMENT, SLASH, STAR, STARTLETTER, STRING_LITERAL, tokenImage, URI
Constructor and Description |
---|
LTLParser(java.io.InputStream stream) |
LTLParser(java.io.InputStream stream,
java.lang.String encoding) |
LTLParser(LTLParserTokenManager tm) |
LTLParser(java.io.Reader stream) |
Modifier and Type | Method and Description |
---|---|
FormulaParameter |
arg(java.util.List<FormulaParameter> localVars) |
java.util.List<FormulaParameter> |
argList() |
void |
attributeDefinition() |
Attribute |
attributeId(java.util.ArrayList localVars) |
SimpleNode |
binaryProp(java.util.ArrayList localVars,
java.lang.String formulaName) |
SimpleNode |
comparison(java.util.ArrayList localVars) |
java.util.List<java.lang.String> |
conceptSet() |
void |
deleteFormula(java.lang.String name) |
void |
disable_tracing() |
Attribute |
dummy(java.util.ArrayList localVars) |
static void |
dump(SimpleNode node,
java.lang.String prefix,
java.lang.StringBuffer result) |
void |
enable_tracing() |
boolean |
existsAttribute(java.lang.String id)
Does id exists as attribute or a renaming?
|
boolean |
existsFormula(java.lang.String id)
Does id exists as formula?
|
boolean |
existsId(java.lang.String id)
Does id exists as attribute, renaming or formula?
|
boolean |
existsRenaming(java.lang.String id)
Does id exists as a renaming?
|
SimpleNode |
expr(int type,
java.util.ArrayList localVars,
Attribute lefthandSideAttribute) |
SimpleNode |
formulaCall(java.util.ArrayList localVars,
java.lang.String formulaName) |
SimpleNode |
formulaDefinition() |
ParseException |
generateParseException() |
Attribute |
getAttribute(java.lang.String id)
Get the attribute linked with id.
|
java.util.ArrayList |
getAttributes()
Get the list with attributes.
|
java.lang.String |
getFilename() |
SimpleNode |
getFormula(java.lang.String id)
Get the formula linked with id.
|
Token |
getNextToken() |
java.util.List<FormulaParameter> |
getParameters(java.lang.String id)
Get the parameters linked with id.
|
Token |
getToken(int index) |
java.util.ArrayList |
getVisibleFormulaNames()
Get the names of the visible formulae, that is of all formula.
|
void |
init()
Construct a new LTLParser with new empty sets, before parsing, no
attributes, renamings or formulae are defined.
|
Attribute |
literal(Attribute param) |
static void |
main(java.lang.String[] args) |
void |
parse()
The grammar of the LTL language is defined below as production rules
decorated with some context checking in java.
|
static void |
parseFile(java.lang.String filename) |
static void |
parseFile(java.lang.String filename,
boolean verbose) |
SimpleNode |
props(java.util.ArrayList localVars,
java.lang.String formulaName) |
SimpleNode |
quantification(java.util.ArrayList localVars,
java.lang.String formulaName) |
void |
ReInit(java.io.InputStream stream) |
void |
ReInit(java.io.InputStream stream,
java.lang.String encoding) |
void |
ReInit(LTLParserTokenManager tm) |
void |
ReInit(java.io.Reader stream) |
void |
renaming() |
void |
setDefaultValues(java.lang.String formulaName,
java.util.Map<java.lang.String,java.lang.String> defaults) |
void |
setFilename(java.lang.String filename) |
java.util.TreeSet |
stringList() |
SimpleNode |
unaryProp(java.util.ArrayList localVars,
java.lang.String formulaName) |
Attribute |
valId(Attribute param,
java.util.ArrayList localVars) |
java.util.ArrayList |
valList(java.lang.String formula,
java.util.ArrayList localVars) |
void |
writeToFile(java.lang.String filename) |
void |
writeToFile(java.lang.String filename,
java.util.Set<java.lang.String> exportFormulas) |
protected org.processmining.plugins.ltlchecker.parser.JJTLTLParserState jjtree
public LTLParserTokenManager token_source
public Token token
public Token jj_nt
public boolean lookingAhead
public LTLParser(java.io.InputStream stream)
public LTLParser(java.io.InputStream stream, java.lang.String encoding)
public LTLParser(java.io.Reader stream)
public LTLParser(LTLParserTokenManager tm)
public static void main(java.lang.String[] args)
public static void dump(SimpleNode node, java.lang.String prefix, java.lang.StringBuffer result)
public void deleteFormula(java.lang.String name)
public void writeToFile(java.lang.String filename) throws java.io.IOException
java.io.IOException
public void writeToFile(java.lang.String filename, java.util.Set<java.lang.String> exportFormulas) throws java.io.IOException
java.io.IOException
public void setDefaultValues(java.lang.String formulaName, java.util.Map<java.lang.String,java.lang.String> defaults)
public static void parseFile(java.lang.String filename)
public void setFilename(java.lang.String filename)
public java.lang.String getFilename()
public static void parseFile(java.lang.String filename, boolean verbose)
public void init()
public boolean existsId(java.lang.String id)
id
- The string denoting the identifier to check.public boolean existsAttribute(java.lang.String id)
id
- The string denoting the identifier to check.public boolean existsRenaming(java.lang.String id)
id
- The string denoting the identifier to check.public boolean existsFormula(java.lang.String id)
id
- The string denoting the identifier to check.public java.util.ArrayList getAttributes()
The
- list with attributes.public Attribute getAttribute(java.lang.String id)
id
- The string denoting the identifier to finf the attribute of.
THis id is already checked to be an attributeId.public SimpleNode getFormula(java.lang.String id)
id
- The id to get the formula for. Id is already checked to
contain an formula.public java.util.List<FormulaParameter> getParameters(java.lang.String id)
id
- The id to get the parameters for. Id is already checked to
contain a formula, and hencefort a parameterlist, which may be
empty.public java.util.ArrayList getVisibleFormulaNames()
public final void parse() throws ParseException
ParseException
public final void attributeDefinition() throws ParseException
ParseException
public final void renaming() throws ParseException
ParseException
public final SimpleNode formulaDefinition() throws ParseException
ParseException
public final java.util.List<FormulaParameter> argList() throws ParseException
ParseException
public final FormulaParameter arg(java.util.List<FormulaParameter> localVars) throws ParseException
ParseException
public final SimpleNode props(java.util.ArrayList localVars, java.lang.String formulaName) throws ParseException
ParseException
public final SimpleNode unaryProp(java.util.ArrayList localVars, java.lang.String formulaName) throws ParseException
ParseException
public final SimpleNode binaryProp(java.util.ArrayList localVars, java.lang.String formulaName) throws ParseException
ParseException
public final SimpleNode quantification(java.util.ArrayList localVars, java.lang.String formulaName) throws ParseException
ParseException
public final Attribute dummy(java.util.ArrayList localVars) throws ParseException
ParseException
public final SimpleNode comparison(java.util.ArrayList localVars) throws ParseException
ParseException
public final SimpleNode formulaCall(java.util.ArrayList localVars, java.lang.String formulaName) throws ParseException
ParseException
public final java.util.ArrayList valList(java.lang.String formula, java.util.ArrayList localVars) throws ParseException
ParseException
public final java.util.TreeSet stringList() throws ParseException
ParseException
public final java.util.List<java.lang.String> conceptSet() throws ParseException
ParseException
public final Attribute attributeId(java.util.ArrayList localVars) throws ParseException
ParseException
public final Attribute valId(Attribute param, java.util.ArrayList localVars) throws ParseException
ParseException
public final Attribute literal(Attribute param) throws ParseException
ParseException
public final SimpleNode expr(int type, java.util.ArrayList localVars, Attribute lefthandSideAttribute) throws ParseException
ParseException
public void ReInit(java.io.InputStream stream)
public void ReInit(java.io.InputStream stream, java.lang.String encoding)
public void ReInit(java.io.Reader stream)
public void ReInit(LTLParserTokenManager tm)
public final Token getNextToken()
public final Token getToken(int index)
public ParseException generateParseException()
public final void enable_tracing()
public final void disable_tracing()