uk.ac.man.cs.rainbow.wvmc.parser
Class SpecParse

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.wvmc.parser.SpecParse

All Implemented Interfaces:

Constants, uk.ac.man.cs.rainbow.wvmc.parser.SpecParseConstants

public class SpecParse

extends Object

implements Constants, uk.ac.man.cs.rainbow.wvmc.parser.SpecParseConstants

Parser for CTL* in negation-normal form and LTL. LTL formulæ are converted to negation-normal form CTL internally.

See Also:

parse(AutomataBuilder,String), parseLTL(AutomataBuilder,String), Recognised Grammar

Field Summary

static int	DECIMAL_NUMBER
static int	DEFAULT
static int	EOF
static int	HEX_NUMBER
Token	jj_nt
static int	NUMBER
static int	OCTAL_NUMBER
static int	SINGLE_LINE_COMMENT
Token	token
uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager	token_source
static String[]	tokenImage

Fields inherited from interface uk.ac.man.cs.rainbow.wvmc.Constants

A, AND, AU, AV, AX, BAD_LOOP, E, EU, EV, EX, Existential, Expand, False, GOOD_LOOP, LOOP_STATE, MAX_BUCHI_TABLE, MAX_TABLE, NEW_STATE, NO_MORE_SUCCS, NOT_LOOP, NUMOPS, OLD_STATE, opToName, OR, q_0, q_1, q_10, q_11, q_12, q_13, q_14, q_15, q_2, q_3, q_4, q_5, q_6, q_7, q_8, q_9, quantToName, True, U, Universal, V, X

Constructor Summary

SpecParse(CharStream stream)

SpecParse(uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager tm)

Method Summary

int	CtlBoolConnect() Parse either a CTL* and or or connective.
Formula	CtlComplexSpec() A complex CTL* formula fragment.
Formula	CtlFGQuant(boolean isAll, int i) A CTL* formula with a path quantifier and a sometime/always operator in front.
int	CtlPathQuant() Parse either a CTL* universal or existential path quantifier.
FormPair	CtlPrefix() A prefix proposition.
Formula	CtlQuantified(boolean isAll) A quantified CTL* formula.
Formula	CtlSimpleSpec() Simple components of a CTL* formula.
int	CtlSometimeAlways() Parse either a CTL* always or sometime operator.
Formula	CtlSpec() A CTL* formula.
FormPair	CtlSpecPair() A pair of CTL* formulę.
Formula	CtlStarSpec() Parse a CTL* formula, optionally followed by a ".".
int	CtlUntilRelease() Parse either a CTL* until or release operator.
Formula	CtlUNum() A proposition with underlines round it.
Formula	CtlUQuant(boolean isAll, Formula u) CTL* formula fragment.
Formula	CtlXQuant(boolean isAll) A CTL* formula with a path quantifier and a next operator in front.
void	disable_tracing()
void	enable_tracing()
ParseException	generateParseException()
Token	getNextToken()
Token	getToken(int index)
Formula	Ltl() Parse an LTL formula, optionally followed by a ".".
Formula	LtlAnd(boolean negated) Parse an LTL formula fragment consisting of a series of fragments separated by and operators.
Formula	LtlImplied(boolean negated) Parse an LTL formula fragment consisting of an optional implication between fragments.
Formula	LtlMonadic(boolean negated) Parse an LTL formula fragment consisting of a list of monadic operators and a proposition or parenthesized formula.
boolean	LtlMonop(boolean negated) Parse either an LTL always or sometime operator.
Formula	LtlOr(boolean negated) Parse an LTL formula fragment consisting of a series of fragments separated by or operators.
Formula	LtlUntil(boolean negated) Parse an LTL formula fragment consisting of a series of fragments separated by until operators.
Formula	LtlWhile(boolean negated) Parse an LTL formula fragment consisting of a series of fragments separated by while operators.
static Formula	parse(AutomataBuilder builder, String s) Parse the given string and build a formula with the given construction engine.
static Formula	parseLTL(AutomataBuilder builder, String s) Parse the given string and build an LTL formula with the given construction engine.
void	ReInit(CharStream stream)
void	ReInit(uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager tm)
int	TlProp() A basic proposition referent.

Methods inherited from class java.lang.Object

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

Field Detail

token_source

public uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager token_source

token

public Token token

jj_nt

public Token jj_nt

EOF

public static final int EOF

SINGLE_LINE_COMMENT

public static final int SINGLE_LINE_COMMENT

NUMBER

public static final int NUMBER

DECIMAL_NUMBER

public static final int DECIMAL_NUMBER

OCTAL_NUMBER

public static final int OCTAL_NUMBER

HEX_NUMBER

public static final int HEX_NUMBER

DEFAULT

public static final int DEFAULT

tokenImage

public static final String[] tokenImage

Constructor Detail

SpecParse

public SpecParse(CharStream stream)

SpecParse

public SpecParse(uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager tm)

Method Detail

parse

public static Formula parse(AutomataBuilder builder,
                            String s)
                     throws ParseException

Parse the given string and build a formula with the given construction engine.

Parameters:

builder - CTL* formula construction engine.

s - String to parse.

Returns:

The parsed formula.

Throws:

ParseException - If the string does not contain validly-formatted CTL* in negation-normal form.

parseLTL

public static Formula parseLTL(AutomataBuilder builder,
                               String s)
                        throws ParseException

Parse the given string and build an LTL formula with the given construction engine. The string need not be in negation normal form. Note that the construction is done using the CTL fragment of CTL*.

Parameters:

builder - CTL* formula construction engine.

s - String to parse.

Returns:

The parsed formula.

Throws:

ParseException - If the string does not contain validly-formatted LTL.

See Also:

Ltl()

Ltl

public final Formula Ltl()
                  throws ParseException

Parse an LTL formula, optionally followed by a ".".

See Also:

LtlUntil()

LtlUntil

public final Formula LtlUntil(boolean negated)
                       throws ParseException

Parse an LTL formula fragment consisting of a series of fragments separated by until operators.

   LtlWhile ( U LtlWhile )*
 

LtlWhile

public final Formula LtlWhile(boolean negated)
                       throws ParseException

Parse an LTL formula fragment consisting of a series of fragments separated by while operators.

   LtlImplied ( W LtlImplied )*
 

LtlImplied

public final Formula LtlImplied(boolean negated)
                         throws ParseException

Parse an LTL formula fragment consisting of an optional implication between fragments. Note that this is backwards w.r.t. the normal way of writing implication so as to make parsing much easier...

   LtlOr ( >= LtlOr )?
 

LtlOr

public final Formula LtlOr(boolean negated)
                    throws ParseException

Parse an LTL formula fragment consisting of a series of fragments separated by or operators.

   LtlAnd ( \/ LtlAnd )*
 

LtlAnd

public final Formula LtlAnd(boolean negated)
                     throws ParseException

Parse an LTL formula fragment consisting of a series of fragments separated by and operators.

   LtlMonadic ( /\ LtlMonadic )*
 

LtlMonop

public final boolean LtlMonop(boolean negated)
                       throws ParseException

Parse either an LTL always or sometime operator.

   [] | <>
 

LtlMonadic

public final Formula LtlMonadic(boolean negated)
                         throws ParseException

Parse an LTL formula fragment consisting of a list of monadic operators and a proposition or parenthesized formula.

     ( LtlUntil )
   | [] LtlMonadic
   | <> LtlMonadic
   | O  LtlMonadic
   | !  LtlMonadic
   | ~  LtlMonadic
   | ¬  LtlMonadic
   | TlProp
 

See Also:

LtlMonop(boolean)

CtlStarSpec

public final Formula CtlStarSpec()
                          throws ParseException

Parse a CTL* formula, optionally followed by a ".".

See Also:

CtlSpec()

CtlSpec

public final Formula CtlSpec()
                      throws ParseException

A CTL* formula.

     CtlComplexSpec
   | CtlSimpleSpec
 

CtlComplexSpec

public final Formula CtlComplexSpec()
                             throws ParseException

A complex CTL* formula fragment. (i.e. one that starts with a temporal operator.)

     X CtlSpec
   | U ( CtlSpec , CtlSpec )
   | V ( CtlSpec , CtlSpec )
   | F CtlSpec
   | G CtlSpec
   | A CtlQuantified
   | E CtlQuantified
 

See Also:

CtlPathQuant(), CtlSometimeAlways(), CtlSpecPair(), CtlUntilRelease()

CtlUQuant

public final Formula CtlUQuant(boolean isAll,
                               Formula u)
                        throws ParseException

CTL* formula fragment.

     X CtlSpec
   | F CtlSpec
   | G CtlSpec
 

See Also:

CtlSometimeAlways()

CtlXQuant

public final Formula CtlXQuant(boolean isAll)
                        throws ParseException

A CTL* formula with a path quantifier and a next operator in front.

     _ { TlProp } _ CtlSpec
   | CtlSpec
 

See Also:

CtlPrefix()

CtlFGQuant

public final Formula CtlFGQuant(boolean isAll,
                                int i)
                         throws ParseException

A CTL* formula with a path quantifier and a sometime/always operator in front.

     _ { TlProp } _ CtlSpec
   | CtlSpec
 

See Also:

CtlPrefix()

CtlQuantified

public final Formula CtlQuantified(boolean isAll)
                            throws ParseException

A quantified CTL* formula.

     _ TlProp _ CtlUQuant
   | X CtlXQuant
   | U ( CtlSpec , CtlSpec )
   | V ( CtlSpec , CtlSpec )
   | F CtlFGQuant
   | G CtlFGQuant
   | CtlSimpleSpec
 

See Also:

CtlSometimeAlways(), CtlSpecPair(), CtlUntilRelease(), CtlUNum()

CtlSimpleSpec

public final Formula CtlSimpleSpec()
                            throws ParseException

Simple components of a CTL* formula.

     ( CtlSpec )
   | ~ TlProp
   | prop
   | t
   | f
   | & ( CtlSpec , CtlSpec )
   | | ( CtlSpec , CtlSpec )
 

See Also:

CtlBoolConnect(), CtlSpecPair()

CtlSpecPair

public final FormPair CtlSpecPair()
                           throws ParseException

A pair of CTL* formulę.

   ( CtlSpec , CtlSpec )
 

CtlPrefix

public final FormPair CtlPrefix()
                         throws ParseException

A prefix proposition.

   _ { TlProp } _
 

CtlSometimeAlways

public final int CtlSometimeAlways()
                            throws ParseException

Parse either a CTL* always or sometime operator.

   F | G
 

CtlUntilRelease

public final int CtlUntilRelease()
                          throws ParseException

Parse either a CTL* until or release operator.

   U | V
 

CtlBoolConnect

public final int CtlBoolConnect()
                         throws ParseException

Parse either a CTL* and or or connective.

   & | |
 

CtlPathQuant

public final int CtlPathQuant()
                       throws ParseException

Parse either a CTL* universal or existential path quantifier.

   A | E
 

CtlUNum

public final Formula CtlUNum()
                      throws ParseException

A proposition with underlines round it. (I'm not sure what this actually means at all...)

   _ TlProp _
 

TlProp

public final int TlProp()
                 throws ParseException

A basic proposition referent.

( p )? NUMBER

ReInit

public void ReInit(CharStream stream)

ReInit

public void ReInit(uk.ac.man.cs.rainbow.wvmc.parser.SpecParseTokenManager tm)

getNextToken

public final Token getNextToken()

getToken

public final Token getToken(int index)

generateParseException

public final ParseException generateParseException()

enable_tracing

public final void enable_tracing()

disable_tracing

public final void disable_tracing()