Package eu.iv4xr.framework.extensions.ltl

Class LTL.WeakUntil<State>

java.lang.Object

eu.iv4xr.framework.extensions.ltl.SequencePredicate<State>

eu.iv4xr.framework.extensions.ltl.LTL<State>

eu.iv4xr.framework.extensions.ltl.LTL.WeakUntil<State>

Enclosing class:

LTL<State>

public static class LTL.WeakUntil<State>
extends LTL<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.

Nested Class Summary

Nested classes/interfaces inherited from class eu.iv4xr.framework.extensions.ltl.LTL

LTL.And<State>, LTL.LTLVerdictInfo, LTL.Next<State>, LTL.Not<State>, LTL.Now<State>, LTL.Or<State>, LTL.Until<State>, LTL.WeakUntil<State>

Field Summary

Fields

Modifier and Type	Field	Description
LTL<State>	phi1
LTL<State>	phi2

Fields inherited from class eu.iv4xr.framework.extensions.ltl.LTL

evals, fullyEvaluated

Constructor Summary

Constructors

Constructor	Description
WeakUntil()

Method Summary

Modifier and Type	Method	Description
(package private) void	evalAtomSat(State state)	Evaluate the atoms of this LTL formula on the given current state, and add the verdict at the end of LTL.evals of those atoms.
SATVerdict	sat()	Return the result of the checking whether this predicate holds on the last sequence given to it.
void	startChecking()	Invoke this first before start checking this LTL formula on an execution; this will rest the internal state of this formula, making it ready to check a new sequence.
String	toString()
LTL.WeakUntil<State>	treeClone()	Make a clone of this LTL formula.

Methods inherited from class eu.iv4xr.framework.extensions.ltl.LTL

always, always, checkNext, endChecking, eventually, eventually, implies, ltlAnd, ltlNot, ltlOr, next, next, now, now, until, until, weakUntil, weakUntil

Methods inherited from class eu.iv4xr.framework.extensions.ltl.SequencePredicate

sat

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Details

phi1

public LTL<State> phi1

phi2

public LTL<State> phi2

Constructor Details

WeakUntil

WeakUntil()

Method Details

startChecking

public void startChecking()

Description copied from class: LTL

Invoke this first before start checking this LTL formula on an execution; this will rest the internal state of this formula, making it ready to check a new sequence.

Overrides:

startChecking in class LTL<State>

sat

public SATVerdict sat()

Description copied from class: SequencePredicate

Return the result of the checking whether this predicate holds on the last sequence given to it. The the sequence was given one state at a time using checkNext(), sat() should be called after endChecking() was called.

• The method returns SAT if this predicate holds on the sequence (it is satisfied by the sequence):
• UNSAT if the sequence does not satisfy this predicate.
• UNKNOWN if neither SAT nor UNSAT can be decided.

Specified by:

sat in class SequencePredicate<State>

evalAtomSat

void evalAtomSat(State state)

Description copied from class: LTL

Evaluate the atoms of this LTL formula on the given current state, and add the verdict at the end of LTL.evals of those atoms.

Specified by:

evalAtomSat in class LTL<State>

treeClone

public LTL.WeakUntil<State> treeClone()

Description copied from class: LTL

Make a clone of this LTL formula. The structure will be cloned, but the under lying state predicates are not cloned.

Specified by:

treeClone in class LTL<State>

toString

public String toString()

Overrides:

toString in class Object