| AbstractLTLRewriter |
This class provides a default implementation of LTLRewriter. |
| EH2000 |
This class implements the LTL formulae simplification described in [Kousha
Etessami, Gerard J.
|
| LTL |
This class provides common methods for LTL formulae.
|
| LTLAlways |
This class represents LTL formulae in "[] f" form.
|
| LTLAnd |
This class represents LTL formulae in "f ∧ g" form.
|
| LTLAtomic |
This class represents the atomic propositions in LTL.
|
| LTLBackto |
This class represents LTL formulae in "f B g" form.
|
| LTLBDD |
This class provides a BDD manager for LTL formulae.
|
| LTLBefore |
This class represents LTL formulae in "(~) f" form.
|
| LTLBinary |
This class represents LTL formulae formed by a binary operator, for example
"f U g", "f R g", "f S g", "f B g", "f T g", "f --> g", or
"f <--> g".
|
| LTLEquivalence |
This class represents LTL formulae in "(f <--> g)" form.
|
| LTLImplication |
This class represents LTL formulae in "(f --> g)" form.
|
| LTLNegation |
This class represents LTL formulae in "~ f" form.
|
| LTLNext |
This class represents LTL formulae in "() f" form.
|
| LTLOnce |
This class represents LTL formulae in "<-> f" form.
|
| LTLOr |
This class represents LTL formulae in "f1 ∨ f2 ∨ ...
|
| LTLParser |
An LTLParser can parse a string into an LTL object.
|
| LTLPastEvaluator |
This class provides a rewriter that can evaluate past formulae at the initial
position.
|
| LTLPastFutureSeparator |
This class provides an adaptation of the separation of past and future
operators in [Dov M.
|
| LTLPrevious |
This class represents LTL formulae in "(-) f" form.
|
| LTLRelease |
This class represents LTL formulae in "f R g" form.
|
| LTLRewritePattern |
An LTLRewritePattern object contains several syntactical rewrite
patterns represented as a map from the pattern to the replacement.
|
| LTLRewriterAdapter |
This class provides a rewriter that does not rewrite any LTL formula.
|
| LTLSet |
This class provides an implementation of sets of LTL formulae.
|
| LTLSimplifier |
This class provides a rewriter for simplifying LTL formulae by pattern
matching.
|
| LTLSince |
This class represents LTL formulae in "f S g" form.
|
| LTLSofar |
This class represents LTL formula in "[-] f" form.
|
| LTLSometime |
This class represents LTL formulae in "<> f" form.
|
| LTLTemporalHierarchy |
This class provides methods for checking syntactically if an LTL formula is a
standard κ-formula based on [Edward Y.
|
| LTLTrigger |
This class represents LTL formulae in "f T g" form.
|
| LTLUnary |
This class represents LTL formulae obtained by applying a unary operator to a
LTL formula, for example, "~ f", "() f", "<> f", "[] f", "(-) f",
"(~) f", "<-> f", and "[-] f".
|
| LTLUnifier |
An LTLUnifier can perform unification on two LTL formulae: source and
target.
|
| LTLUnless |
This class represents LTL formulae in "f W g" form.
|
| LTLUntil |
This class represents LTL formulae in "f U g" form.
|
| LTLUtil |
This class provides some useful methods for processing LTL formulae.
|
| RandomLTL |
This class can randomly generate LTL formulae.
|