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.ExistsNext

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.TransitionSystem

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

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.

getStatesWithLabel(String) - Method in class model.TransitionSystem

Returns the states of this transition system with the given label.

H

hashCode() - Method in class logic.And

hashCode() - Method in class logic.AtomicProposition

hashCode() - Method in class logic.ExistsNext

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.TransitionSystem

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.ExistsNext

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

toString() - Method in class logic.And

toString() - Method in class logic.AtomicProposition

toString() - Method in class logic.ExistsNext

Returns a string representation of this exists next formula.

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.TransitionSystem

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