de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderVariable

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
      de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderVariable

All Implemented Interfaces:

Serializable

public final class FirstOrderVariable
extends Variable

A class representing first order variables in the monadic second order logic.

Author:

Hendrik Maryns

See Also:

Serialized Form

Field Summary

Fields inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable

name

Method Summary

Dominance	dominates(FirstOrderVariable that) Return the formula that says this variable dominates that variable.
FirstOrderExistentialQuantification	exists(Formula form) Returns the existential quantification of the given formula over this variable.
FirstOrderUniversalQuantification	forAll(Formula form) Returns the universal quantification of the given formula over this variable.
static FirstOrderVariable	getInstance(String name) Factory method to get a variable.
ImmediateDominance	immediatelyDominates(FirstOrderVariable that) Return the formula that says this variable immediately dominates that variable.
Inclusion	in(SetDenotator that) Return the formula that says this variable is an element of that set.
FirstOrderEquality	logicalEquals(FirstOrderVariable that) Return the formula that says this variable is equal to that variable.
Precedence	precedes(FirstOrderVariable that) Return the formula that says this variable precedes that variable.
ProperDominance	properlyDominates(FirstOrderVariable that) Return the formula that says this variable immediately dominates that variable.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable

getName, toString

Methods inherited from class java.lang.Object

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

Method Detail

getInstance

public static FirstOrderVariable getInstance(String name)

Factory method to get a variable. If a variable with the given name already exists, it is returned.

Parameters:

name - The name of the variable.

Returns:

The unique variable with the given name. If the name is not effective, a variable with a random name is returned. | if ( name != null ) | then result.getName() == name

forAll

public FirstOrderUniversalQuantification forAll(Formula form)

Returns the universal quantification of the given formula over this variable.

Parameters:

form - The formula to be quantified.

Preconditions:

The given formula should be effective. | form != null

This variable has to be free in the given formula. | !form.containsVariable(this) || form.isFreeVariable(this);

Returns:

The universal quantification of the given formula over this variable. | result.getBoundVariable() == this && | result.getArgument() == form

exists

public FirstOrderExistentialQuantification exists(Formula form)

Returns the existential quantification of the given formula over this variable.

Parameters:

form - The formula to be quantified.

Preconditions:

The given formula should be effective. | form != null

This variable has to be free in the given formula. | !form.containsVariable(this) || form.isFreeVariable(this);

Returns:

The existential quantification of the given formula over this variable. | result.getBoundVariable() == this && | result.getArgument() == form

logicalEquals

public FirstOrderEquality logicalEquals(FirstOrderVariable that)

Return the formula that says this variable is equal to that variable.

Parameters:

that - The other variable. That is a mnemonic for this.logicalEquals(that).

Returns:

The atomic formula claiming this variable is equal to that variable. | result.getFirstVariable() == this && | result.getSecondVariable() == that

in

public Inclusion in(SetDenotator that)

Return the formula that says this variable is an element of that set.

Parameters:

that - The other variable. That is a mnemonic for this.in(that).

Returns:

The atomic formula claiming this variable is an element of that set. | result.getIncludedVariable() == this && | result.getContainingVariable() == that

dominates

public Dominance dominates(FirstOrderVariable that)

Return the formula that says this variable dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.dominates(that).

Returns:

The atomic formula claiming this variable dominates that variable. | result.getDominatingVariable() == this && | result.getDominatedVariable() == that

immediatelyDominates

public ImmediateDominance immediatelyDominates(FirstOrderVariable that)

Return the formula that says this variable immediately dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.immediatelyDominates(that).

Returns:

The atomic formula claiming this variable immediately dominates that variable. | result.getDominatingVariable() == this && | result.getDominatedVariable() == that

properlyDominates

public ProperDominance properlyDominates(FirstOrderVariable that)

Return the formula that says this variable immediately dominates that variable.

Parameters:

that - The other variable. That is a mnemonic for this.immediatelyDominates(that).

Returns:

The atomic formula claiming this variable immediately dominates that variable. | result.getDominatingVariable() == this && | result.getDominatedVariable() == that

precedes

public Precedence precedes(FirstOrderVariable that)

Return the formula that says this variable precedes that variable.

Parameters:

that - The other variable. That is a mnemonic for this.precedes(that).

Returns:

The atomic formula claiming this variable precedes that variable. | result.getPrecedingVariable() == this && | result.getPrecededVariable() == that