Package org.svvrl.goal.core.tran.tester

Class SystemVariable

java.lang.Object

org.svvrl.goal.core.tran.tester.SystemVariable

public class SystemVariable
extends java.lang.Object

This class stands for System Variable. It consists of auxiliary variables and vocabularies of the formula.

Author:

Wen-Chin Chan

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
(package private) class	SystemVariable.LTLComparator

Field Summary

Fields

Modifier and Type	Field	Description
static int	TYPE_AND
static int	TYPE_EQUIVALENCE
static int	TYPE_ERROR
static int	TYPE_IMPLICATION
static int	TYPE_NEGATION
static int	TYPE_OR
static int	TYPE_STATE
static int	TYPE_TEMPORAL

Constructor Summary

Constructors

Constructor	Description
SystemVariable(LTL qptl)	Constructs this class via LTL.

Method Summary

Modifier and Type	Method	Description
java.util.Set<LTL>	computeAuxVarSet(LTL qptl)	This method compute the Auxiliary Variable Set corresponding the input LTL.
java.util.Set<LTL>	computePropSet(LTL qptl)	This method is used to compute the Proposition Variable of the corresponding formula.
static LTL	decompose(LTL qptl)	This method used to maps every sub-formula of phi into an assertion over Vphi.
java.util.Set<LTL>	getAuxVarSet()	Returns the set of auxiliary variables.
java.util.Set<LTL>	getPropSet()	Returns the propositions.
java.util.SortedSet<LTL>	getSortedPropSet()	Returns the sorted propositions.

Methods inherited from class java.lang.Object

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

Field Details

TYPE_STATE

public static final int TYPE_STATE

See Also:

Constant Field Values

TYPE_NEGATION

public static final int TYPE_NEGATION

See Also:

Constant Field Values

TYPE_OR

public static final int TYPE_OR

See Also:

Constant Field Values

TYPE_TEMPORAL

public static final int TYPE_TEMPORAL

See Also:

Constant Field Values

TYPE_AND

public static final int TYPE_AND

See Also:

Constant Field Values

TYPE_IMPLICATION

public static final int TYPE_IMPLICATION

See Also:

Constant Field Values

TYPE_EQUIVALENCE

public static final int TYPE_EQUIVALENCE

See Also:

Constant Field Values

TYPE_ERROR

public static final int TYPE_ERROR

See Also:

Constant Field Values

Constructor Details

SystemVariable

public SystemVariable(LTL qptl)

Constructs this class via LTL.

Parameters:

qptl - an LTL formula

Method Details

getSortedPropSet

public java.util.SortedSet<LTL> getSortedPropSet()

Returns the sorted propositions.

Returns:

the sorted propositions

getPropSet

public java.util.Set<LTL> getPropSet()

Returns the propositions.

Returns:

the propositions

getAuxVarSet

public java.util.Set<LTL> getAuxVarSet()

Returns the set of auxiliary variables.

Returns:

the set of auxiliary variables

computePropSet

public java.util.Set<LTL> computePropSet(LTL qptl)

This method is used to compute the Proposition Variable of the corresponding formula.

Parameters:

qptl - an LTL formula

Returns:

set the propositions occur in qptl

computeAuxVarSet

public java.util.Set<LTL> computeAuxVarSet(LTL qptl)

This method compute the Auxiliary Variable Set corresponding the input LTL.

Parameters:

qptl - an LTL formula

Returns:

set the auxiliary variable set for qptl

decompose

public static LTL decompose(LTL qptl)

This method used to maps every sub-formula of phi into an assertion over Vphi.

Parameters:

qptl - an LTL formula

Returns:

qptl a decomposed formula