Package eu.iv4xr.framework.extensions.ltl

Class LTL.Now<State>

java.lang.Object

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

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

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

Enclosing class:

LTL<State>

public static class LTL.Now<State>
extends LTL<State>

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
String	name
Predicate<State>	p

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

evals, fullyEvaluated

Constructor Summary

Constructors

Constructor	Description
Now()

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.
String	toString()
LTL.Now<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, startChecking, 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

p

public Predicate<State> p

name

public String name

Constructor Details

Now

Now()

Method Details

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>

toString

public String toString()

Overrides:

toString in class Object

treeClone

public LTL.Now<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>