Class BioPatternsTranslator

java.lang.Object
  BioPatternsTranslator

public class BioPatternsTranslator
extends java.lang.Object

The BioPatternsTranslator class translates a biological property from a natural language pattern into a temporal logic formula.

Patterns are high-level descriptions of frequently asked questions. In this context, they consist of structured natural language phrases, with placeholders for state descriptors. State descriptors may be (boolean combinations of) atomic propositions or temporal logic formulas defined on atomic propositions. The latter are restrictions on states describing, among other things, the concentration bounds of the regions and the trend of the variables inside a region.

Occurrence/Exclusion:
It is possible/not possible for a state P to occur

Consequence:
If a state P occurs, then it is possibly/necessarily followed by a state Q

Sequence:
A state Q is reachable and is possibly/necessarily preceded at some time/all the time by a state P

Invariance:
A state P can/must persist indefinitely

Field Summary

static int	ALL_THE_TIME Selection for all points in time, in the Sequence pattern.
static int	AT_SOME_TIME Selection for a given point in time, in the Sequence pattern.
static int	CAN Selection for possibility, in the Invariance pattern.
static int	CTL Selection for CTL (Computation Tree Logic).
static int	CTRL Selection for CTRL (Computation Tree Regular Logic).
static int	MU_CALCULUS Selection for mu-calculus temporal logic.
static int	MUST Selection for necessity, in the Invariance pattern.
static int	NECESSARILY Selection for necessity, in the Consequence and Sequence pattern.
static int	NOT_POSSIBLE Selection for exclusion, in the Occurrence/Exclusion pattern.
static int	POSSIBLE Selection for occurrence, in the Occurrence/Exclusion pattern.
static int	POSSIBLY Selection for possibility, in the Consequence and Sequence pattern.

Constructor Summary

BioPatternsTranslator(java.lang.String[] atomicPropositions)
Initializes a newly created BioPatternsTranslator object with a string array of names of atomic propositions.

Method Summary

java.lang.String	consequence(int logic, java.lang.String atomProp1, int possiblyOrNecessarily, java.lang.String atomProp2) Consequence pattern: "If a state atomProp1 occurs, then it is possibly/necessarily followed by a state atomProp2".
java.lang.String[]	getAtomicPropositions() The set of string names representing the atomic propositions.
java.lang.String	invariance(int logic, java.lang.String atomProp, int canMust) Invariance pattern: "A state atomProp can/must persist indefinitely".
java.lang.String	occurrence(int logic, int isItPossible, java.lang.String atomProp) Occurrence/Exclusion pattern: "It is possible/not possible for a state atomProp to occur".
java.lang.String	sequence(int logic, java.lang.String atomProp1, int possiblyOrNecessarily, int someAllTime, java.lang.String atomProp2) Sequence pattern: "A state atomProp1 is reachable and is possibly/necessarily preceded at some time/all the time by a state atomProp2".
void	setAtomicPropositions(java.lang.String[] saAtomProps) Initializes the set of atomic proposition names that are considered valid.

Methods inherited from class java.lang.Object

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

Field Detail

ALL_THE_TIME

public static final int ALL_THE_TIME

Selection for all points in time, in the Sequence pattern.

See Also:

Constant Field Values

AT_SOME_TIME

public static final int AT_SOME_TIME

Selection for a given point in time, in the Sequence pattern.

See Also:

Constant Field Values

CAN

public static final int CAN

Selection for possibility, in the Invariance pattern.

See Also:

Constant Field Values

CTL

public static final int CTL

Selection for CTL (Computation Tree Logic).

See Also:

Constant Field Values

CTRL

public static final int CTRL

Selection for CTRL (Computation Tree Regular Logic).

See Also:

Constant Field Values

MU_CALCULUS

public static final int MU_CALCULUS

Selection for mu-calculus temporal logic.

See Also:

Constant Field Values

MUST

public static final int MUST

Selection for necessity, in the Invariance pattern.

See Also:

Constant Field Values

NECESSARILY

public static final int NECESSARILY

Selection for necessity, in the Consequence and Sequence pattern.

See Also:

Constant Field Values

NOT_POSSIBLE

public static final int NOT_POSSIBLE

Selection for exclusion, in the Occurrence/Exclusion pattern.

See Also:

Constant Field Values

POSSIBLE

public static final int POSSIBLE

Selection for occurrence, in the Occurrence/Exclusion pattern.

See Also:

Constant Field Values

POSSIBLY

public static final int POSSIBLY

Selection for possibility, in the Consequence and Sequence pattern.

See Also:

Constant Field Values

Constructor Detail

BioPatternsTranslator

public BioPatternsTranslator(java.lang.String[] atomicPropositions)

Initializes a newly created BioPatternsTranslator object with a string array of names of atomic propositions.

Parameters:

atomicPropositions - a string array of names of atomic propositions.

Method Detail

consequence

public java.lang.String consequence(int logic,
                                    java.lang.String atomProp1,
                                    int possiblyOrNecessarily,
                                    java.lang.String atomProp2)
                             throws java.lang.Exception

Consequence pattern: "If a state atomProp1 occurs, then it is possibly/necessarily followed by a state atomProp2".

Parameters:

logic - selection of a given temporal logic from the supported ones (CTL, CTRL, MU_CALCULUS).

atomProp1 - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

possiblyOrNecessarily - selection between POSSIBLY or NECESSARILY.

atomProp2 - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

Returns:

a string containing the temporal logic formula corresponding to the pattern instantiated with the corresponding options.

Throws:

java.lang.Exception - if there is an invalid option, and exception is thrown with the specific error.

getAtomicPropositions

public java.lang.String[] getAtomicPropositions()

The set of string names representing the atomic propositions.

Returns:

a string array containing the names of the atomic propositions.

invariance

public java.lang.String invariance(int logic,
                                   java.lang.String atomProp,
                                   int canMust)
                            throws java.lang.Exception

Invariance pattern: "A state atomProp can/must persist indefinitely".

Parameters:

logic - selection of a given temporal logic from the supported ones (CTL, CTRL, MU_CALCULUS).

atomProp - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

canMust - selection between CAN or MUST.

Returns:

a string containing the temporal logic formula corresponding to the pattern instantiated with the corresponding options.

Throws:

java.lang.Exception - if there is an invalid option, and exception is thrown with the specific error.

occurrence

public java.lang.String occurrence(int logic,
                                   int isItPossible,
                                   java.lang.String atomProp)
                            throws java.lang.Exception

Occurrence/Exclusion pattern: "It is possible/not possible for a state atomProp to occur".

Parameters:

logic - selection of a given temporal logic from the supported ones (CTL, CTRL, MU_CALCULUS).

isItPossible - selection between POSSIBLE or NOT_POSSIBLE.

atomProp - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

Returns:

a string containing the temporal logic formula corresponding to the pattern instantiated with the corresponding options.

Throws:

java.lang.Exception - if there is an invalid option, and exception is thrown with the specific error.

sequence

public java.lang.String sequence(int logic,
                                 java.lang.String atomProp1,
                                 int possiblyOrNecessarily,
                                 int someAllTime,
                                 java.lang.String atomProp2)
                          throws java.lang.Exception

Sequence pattern: "A state atomProp1 is reachable and is possibly/necessarily preceded at some time/all the time by a state atomProp2".

Parameters:

logic - selection of a given temporal logic from the supported ones (CTL, CTRL, MU_CALCULUS).

atomProp1 - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

possiblyOrNecessarily - selection between POSSIBLY or NECESSARILY.

someAllTime - selection between AT_SOME_TIME or ALL_THE_TIME.

atomProp2 - an atomic proposition name to instantiate the pattern and that must be present in the string array of valid atomic proposition names.

Returns:

a string containing the temporal logic formula corresponding to the pattern instantiated with the corresponding options.

Throws:

java.lang.Exception - if there is an invalid option, and exception is thrown with the specific error.

setAtomicPropositions

public void setAtomicPropositions(java.lang.String[] saAtomProps)

Initializes the set of atomic proposition names that are considered valid.

Parameters:

saAtomProps - string array of atomic proposition names.