logic

Class Formula

java.lang.Object

logic.Formula

Direct Known Subclasses:

And, AtomicProposition, ExistsNext, Not, True

public abstract class Formula
extends java.lang.Object

This class represents the CTL formula.

Constructor Summary

Constructors

Constructor and Description
Formula()

Method Summary

Modifier and Type	Method and Description
abstract boolean	equals(java.lang.Object object) Tests whether this formula is equal to the given object.
abstract int	hashCode() Returns the hashcode of this formula.
static Formula	random() Returns a random formula.
static Formula	random(int depth) Returns a random formula of at most the given depth.
abstract java.util.BitSet	sat(TransitionSystem system) Returns the set of states of the given transition system that satisfy this formula.
abstract java.lang.String	toString() Returns a string representation of this formula.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

Formula

public Formula()

Method Detail

random

public static Formula random(int depth)

Returns a random formula of at most the given depth.

Parameters:

depth - the maximum depth of the formula

Returns:

a random formula of at most the given depth

random

public static Formula random()

Returns a random formula.

Returns:

a random formula

hashCode

public abstract int hashCode()

Returns the hashcode of this formula.

Overrides:

hashCode in class java.lang.Object

Returns:

the hashcode of this formula

equals

public abstract boolean equals(java.lang.Object object)

Tests whether this formula is equal to the given object.

Overrides:

equals in class java.lang.Object

Parameters:

object - an object

Returns:

true if this formula is equal to the given object, false otherwise

toString

public abstract java.lang.String toString()

Returns a string representation of this formula.

Overrides:

toString in class java.lang.Object

Returns:

a string representation of this formula

sat

public abstract java.util.BitSet sat(TransitionSystem system)

Returns the set of states of the given transition system that satisfy this formula.

Parameters:

system - a transition system

Returns:

the set of states of the given transition system that satisfy this formula