Package edu.luc.cs.trull.tl

Provides an implementation of temporal logic expressions in Java.

See:
Description

Interface Summary

Visitor

A visitor for temporal logic expressions.

Class Summary

AllPast	The formula always p specifies that p must have been true for the entire past history of this system run.
And	The formula l /\ r specifies that both l and r must be true in the current time unit.
Assert	An item-selectable component that wraps around a temporal logic assertion.
BackTo	The formula p backto q specifies that either p since q is true or always p is true.
Expr	The class Expr is the common abstract superclass for all temporal logic formula classes.
FringeVisitor	A visitor that walks along the fringe of a temporal logic expression.
Implies	The formula p => q is defined as (!
Leaf	The formula leaf l specifies that the current label is l.
Not	The formula !
Once	The formula once p specifies that p must have been true sometime in the history of this system run.
Or	The formula p \/ q specifies that either p or q or both are true in the current time unit.
Previous	The formula previous p specifies that p must have been true in the time unit immediately preceding the current one.
PrintVisitor	A visitor for converting a temporal logic expression to a String.
Since	The formula p since q specifies that q must have been true sometime in the past history of this system run, and that p must have been true in every time unit since the last time q was true.
UniformVisitor	A visitor that applies the same visit method to its argument without further traversal.
VisitorAdapter	An empty visitor implementation.

Package edu.luc.cs.trull.tl Description

Provides an implementation of temporal logic expressions in Java.

It includes an abstract superclass called Expr (for atomic expressions or events in the system) and a set of classes Not, And, etc., each corresponding to a temporal logic formula, which may be built on top of other formulas.

For instance, to create a formula such as: F: A => Prev B, do this:

Expr B = new Expr();
Previous Aux0 = new Previous(B);
Expr A = new Expr();
Implies F = new Implies(A, Aux0);

(For convenience, arguments of constructors of the subclasses of Expr can be either expressions of type Expr or event labels of type Object.)

To evaluate this formula over time, you typically do this:

F.reset();
for each tick:
    A.set(some bool value);
    B.set(some other bool value);
    boolean v = F.eval();
    /* use v, or F.check() repeatedly */
end for

Note that it is possible to use a formula more than once in building new formulas, even if it has "internal state", formulas are evaluated *exactly* once per each eval() to top-level formulas.