Uses of Class
eu.iv4xr.framework.extensions.ltl.LTL

Packages that use LTL

Package	Description
eu.iv4xr.framework.extensions.ltl	This package provides the following features: The classes LTL and BoundedLTL implementing Linear Temporal Logic formulas, and the bounded variation of them.
eu.iv4xr.framework.mainConcepts

Uses of LTL in eu.iv4xr.framework.extensions.ltl

Subclasses of LTL in eu.iv4xr.framework.extensions.ltl

Modifier and Type	Class	Description
static class	LTL.And<State>
static class	LTL.Next<State>
static class	LTL.Not<State>
static class	LTL.Now<State>
static class	LTL.Or<State>	For representing "phi || psi".
static class	LTL.Until<State>
static class	LTL.WeakUntil<State>	Weak-until is not primitive in LTL-sense, but we add it as a separate class so that we can structurally recognize that a formula is a weak-until formula.

Fields in eu.iv4xr.framework.extensions.ltl declared as LTL

Modifier and Type	Field	Description
LTL<State>[]	LTL.And.conjuncts
LTL<State>[]	LTL.Or.disjuncts
(package private) LTL<IState>	BoundedLTL.ltl
LTL<State>	LTL.Next.phi
LTL<State>	LTL.Not.phi
LTL<State>	LTL.Until.phi1
LTL<State>	LTL.WeakUntil.phi1
LTL<State>	LTL.Until.phi2
LTL<State>	LTL.WeakUntil.phi2

Methods in eu.iv4xr.framework.extensions.ltl that return LTL

Modifier and Type	Method	Description
static <State> LTL<State>	LTL.always(LTL<State> phi)	always(phi) constructs the LTL formula "G phi" (also written "[] phi").
static <State> LTL<State>	LTL.always(Predicate<State> phi)	If p is a state-predicate, always(phi) constructs the LTL formula "G now(p)" (also written "[] now(p)").
static <State> LTL<State>	LTL2Buchi.andRewrite(LTL<State> f)	Normalize an LTL formula by rewriting conjunctions.
static <State> LTL<State>	LTL2Buchi.arg(LTL<State> phi)
static <State> LTL<State>	LTL2Buchi.argL(LTL<State> phi)
static <State> LTL<State>	LTL2Buchi.argR(LTL<State> phi)
LTL<State>	LTL.implies(LTL<State> psi)	phi.implies(psi) constructs the LTL formula "phi --> psi".
static <State> LTL<State>	LTL2Buchi.isNotPhi(LTL<State> phi)	To recognize and destruct "not(phi)" pattern, where phi is non-atomic.
static <State> LTL<State>	LTL2Buchi.pushNegations(LTL<State> f)	Normalize an LTL formula by rewriting it, so that negations are recursively pushed as far as possible inside.
abstract LTL<State>	LTL.treeClone()	Make a clone of this LTL formula.
LTL<State>	LTL.until(Predicate<State> psi)

Methods in eu.iv4xr.framework.extensions.ltl with parameters of type LTL

Modifier and Type	Method	Description
static <State> LTL<State>	LTL.always(LTL<State> phi)	always(phi) constructs the LTL formula "G phi" (also written "[] phi").
static <State> LTL<State>	LTL2Buchi.andRewrite(LTL<State> f)	Normalize an LTL formula by rewriting conjunctions.
static <State> LTL<State>	LTL2Buchi.arg(LTL<State> phi)
static <State> LTL<State>	LTL2Buchi.argL(LTL<State> phi)
static <State> LTL<State>	LTL2Buchi.argR(LTL<State> phi)
(package private) static String	LTL2Buchi.atomName(LTL ltl)
(package private) static <State> Predicate<State>	LTL2Buchi.atomPred(LTL<State> ltl)
static <State> LTL.Until<State>	LTL.eventually(LTL<State> phi)	evenatually(phi) constructs the LTL formula "F phi" (also written "diamond phi").
BasicModelChecker.Path<Pair<IExplorableState,String>>	BuchiModelChecker.find(LTL<IExplorableState> phi, int maxDepth)	The same as BuchiModelChecker.find(Buchi, int), but it takes an LTL formula for specifying the pattern of the execution to find.
BasicModelChecker.Path<Pair<IExplorableState,String>>	BuchiModelChecker.findShortest(LTL<IExplorableState> phi, int maxDepth)	Similar to BuchiModelChecker.find(LTL, int), but it will return the shortest execution (of the specified max-length) that satisfies the given LTL.
static Buchi	LTL2Buchi.getBuchi(LTL<IExplorableState> phi)	Translate the given LTL formula to a Buchi automaton.
LTL<State>	LTL.implies(LTL<State> psi)	phi.implies(psi) constructs the LTL formula "phi --> psi".
static <State> boolean	LTL2Buchi.isAtom(LTL<State> phi)
static <State> LTL.And<State>	LTL2Buchi.isNotAnd(LTL<State> psi)	Recognize "not(p ∧ ...
static <State> boolean	LTL2Buchi.isNotAtom(LTL<State> phi)
static <State> LTL.Next<State>	LTL2Buchi.isNotNext(LTL<State> psi)	Recognize "not(next(psi))".
static <State> LTL.Not<State>	LTL2Buchi.isNotNot(LTL<State> psi)	Recognize "not(not(phi))".
static <State> LTL.Now<State>	LTL2Buchi.isNotNow(LTL<State> phi)	To recognize and destruct "not(now p)".
static <State> LTL.Or<State>	LTL2Buchi.isNotOr(LTL<State> psi)	Recognize "not(p || ...
static <State> LTL<State>	LTL2Buchi.isNotPhi(LTL<State> phi)	To recognize and destruct "not(phi)" pattern, where phi is non-atomic.
static <State> LTL.Until<State>	LTL2Buchi.isNotUntil(LTL<State> psi)	Recognize "not(p U q)" .
static <State> LTL.WeakUntil<State>	LTL2Buchi.isNotWeakUntil(LTL<State> psi)	Recognize "not(p W q)" .
static <State> Predicate<State>	LTL2Buchi.isNow(LTL<State> phi)	To recognize and destruct "now p".
static <State> LTL.And<State>	LTL.ltlAnd(LTL<State>... phis)	ltlAnd(phi1, ..., phin ) constructs the LTL formula "phi1 ∧ phi2 ...
static <State> LTL.Not<State>	LTL.ltlNot(LTL<State> phi)	ltlNot(phi) constructs the LTL formula "not phi".
static <State> LTL.Or<State>	LTL.ltlOr(LTL<State>... phis)	ltlOr(phi1, ..., phin ) constructs the LTL formula "phi1 || phi2 ...
static <State> LTL.Next<State>	LTL.next(LTL<State> phi)	If p is a state-predicate, next(p) constructs the LTL formula "X now(p)".
static <State> LTL<State>	LTL2Buchi.pushNegations(LTL<State> f)	Normalize an LTL formula by rewriting it, so that negations are recursively pushed as far as possible inside.
SATVerdict	BuchiModelChecker.sat(LTL<IExplorableState> phi)	Check if the target 'program' BuchiModelChecker.model can produce an infinite execution that would satisfy the given LTL formula.
SATVerdict	BuchiModelChecker.sat(LTL<IExplorableState> phi, int maxDepth)	Check if the target program has an finite execution of the specified maximum length that would witness the given LTL formula.
BoundedLTL	BoundedLTL.thereIs(LTL<IState> F)
LTL.Until<State>	LTL.until(LTL<State> psi)	phi.Until(psi) constructs the LTL formula "phi U psi".
LTL.WeakUntil<State>	LTL.weakUntil(LTL<State> psi)	phi.weakUntil(psi) constructs the LTL formula "phi W psi".

Uses of LTL in eu.iv4xr.framework.mainConcepts

Fields in eu.iv4xr.framework.mainConcepts with type parameters of type LTL

Modifier and Type	Field	Description
List<LTL<SimpleState>>	TestAgent.ltls

Methods in eu.iv4xr.framework.mainConcepts with parameters of type LTL

Modifier and Type	Method	Description
TestAgent	TestAgent.addLTL(LTL<SimpleState>... ltlsToAdd)	Add one or more LTL-properties that would be checked as the agent runs.