A E F G H L M N P R S T

A

And - Class in logic

This class represents a CTL formula that is a conjunction (and) of two formulas.

And(Formula, Formula) - Constructor for class logic.And

Initializes this CTL formula as the conjunction (and) of the given left and right subformulas.

AtomicProposition - Class in logic

This class represents the CTL state formula consisting of an atomic proposition.

AtomicProposition(String) - Constructor for class logic.AtomicProposition

Initializes this CTL formula as an atomic proposition with the given name.

E

equals(Object) - Method in class logic.And

equals(Object) - Method in class logic.AtomicProposition

equals(Object) - Method in class logic.ExistsEventually

equals(Object) - Method in class logic.ExistsNext

equals(Object) - Method in class logic.ForAllAlways

equals(Object) - Method in class logic.ForAllNext

equals(Object) - Method in class logic.Formula

Tests whether this formula is equal to the given object.

equals(Object) - Method in class logic.Not

equals(Object) - Method in class logic.True

equals(Object) - Method in class model.Transition

equals(Object) - Method in class model.TransitionSystem

ExistsEventually - Class in logic

This class represents a CTL formula that is the exists eventually (diamond) of a formula.

ExistsEventually(Formula) - Constructor for class logic.ExistsEventually

Initializes this CTL formula as the exists eventually of the given formula.

ExistsNext - Class in logic

This class represents a CTL formula that is the exists next of a formula.

ExistsNext(Formula) - Constructor for class logic.ExistsNext

Initializes this CTL formula as the exists next of the given formula.

F

ForAllAlways - Class in logic

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

ForAllAlways(Formula) - Constructor for class logic.ForAllAlways

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

ForAllNext - Class in logic

This class represents a CTL formula that is the for all next of a formula.

ForAllNext(Formula) - Constructor for class logic.ForAllNext

Initializes this CTL formula as the for all next of the given formula.

Formula - Class in logic

This class represents the CTL formula.

Formula() - Constructor for class logic.Formula

G

getStates() - Method in class model.TransitionSystem

Returns the number of states of this transition system.

H

hashCode() - Method in class logic.And

hashCode() - Method in class logic.AtomicProposition

hashCode() - Method in class logic.ExistsEventually

hashCode() - Method in class logic.ExistsNext

hashCode() - Method in class logic.ForAllAlways

hashCode() - Method in class logic.ForAllNext

hashCode() - Method in class logic.Formula

Returns the hashcode of this formula.

hashCode() - Method in class logic.Not

hashCode() - Method in class logic.True

hashCode() - Method in class model.Transition

hashCode() - Method in class model.TransitionSystem

hasLabel(int, String) - Method in class model.TransitionSystem

Tests whether the given state of this transition system has the given label.

L

logic - package logic

M

model - package model

N

Not - Class in logic

This class represents a CTL formula that is the negation (not) of a formula.

Not(Formula) - Constructor for class logic.Not

Initializes this CTL formula as the negation of the given formula.

P

post(int) - Method in class model.TransitionSystem

Returns the set of successor states of the given state.

R

random(int) - Static method in class logic.Formula

Returns a random formula of at most the given depth.

random() - Static method in class logic.Formula

Returns a random formula.

random(int) - Static method in class model.TransitionSystem

Returns a random transition system with the given number of states.

S

sat(TransitionSystem) - Method in class logic.And

sat(TransitionSystem) - Method in class logic.AtomicProposition

sat(TransitionSystem) - Method in class logic.ExistsEventually

sat(TransitionSystem) - Method in class logic.ExistsNext

sat(TransitionSystem) - Method in class logic.ForAllAlways

sat(TransitionSystem) - Method in class logic.ForAllNext

sat(TransitionSystem) - Method in class logic.Formula

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

sat(TransitionSystem) - Method in class logic.Not

sat(TransitionSystem) - Method in class logic.True

T

toDot() - Method in class model.Transition

Returns a dot representation of this transition.

toDot() - Method in class model.TransitionSystem

Returns a dot representation of this transition system.

toString() - Method in class logic.And

toString() - Method in class logic.AtomicProposition

toString() - Method in class logic.ExistsEventually

Returns a string representation of this exists eventually formula.

toString() - Method in class logic.ExistsNext

toString() - Method in class logic.ForAllAlways

Returns a string representation of this for-all always formula.

toString() - Method in class logic.ForAllNext

toString() - Method in class logic.Formula

Returns a string representation of this formula.

toString() - Method in class logic.Not

toString() - Method in class logic.True

toString() - Method in class model.Transition

toString() - Method in class model.TransitionSystem

Transition - Class in model

A transition of a transition system.

Transition(int, int) - Constructor for class model.Transition

Initializes this transition with the given source and target state.

TransitionSystem - Class in model

A transition system.

True - Class in logic

This class represents the CTL formula true.

True() - Constructor for class logic.True

Initializes this CTL formula as true.

A E F G H L M N P R S T