logic

Class ForAllAlways

java.lang.Object

logic.Formula

logic.ForAllAlways

public class ForAllAlways
extends Formula

This class represents a CTL formula that is the for-all always (box) of a formula.

Constructor Summary

Constructors

Constructor and Description
ForAllAlways(Formula formula) Initializes this CTL formula as the for-all always of the given formula.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object object) Tests whether this formula is equal to the given object.
int	hashCode() Returns the hashcode of this formula.
java.util.Set<java.lang.Integer>	sat(TransitionSystem system) Returns the set of states of the given transition system that satisfy this formula.
java.lang.String	toString() Returns a string representation of this for-all always formula.

Methods inherited from class logic.Formula

random, random

Methods inherited from class java.lang.Object

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

Constructor Detail

ForAllAlways

public ForAllAlways(Formula formula)

Initializes this CTL formula as the for-all always of the given formula.

Parameters:

formula - the subformula of this for-all always formula

Method Detail

hashCode

public int hashCode()

Description copied from class: Formula

Returns the hashcode of this formula.

Specified by:

hashCode in class Formula

Returns:

the hashcode of this formula

equals

public boolean equals(java.lang.Object object)

Description copied from class: Formula

Tests whether this formula is equal to the given object.

Specified by:

equals in class Formula

Parameters:

object - an object

Returns:

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

toString

public java.lang.String toString()

Returns a string representation of this for-all always formula. The string consists of "AG " followed by the string representation of the subformula.

Specified by:

toString in class Formula

Returns:

a string representation of this for-all always formula

sat

public java.util.Set<java.lang.Integer> sat(TransitionSystem system)

Description copied from class: Formula

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

Specified by:

sat in class Formula

Parameters:

system - a transition system

Returns:

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