Uses of Enum
eu.iv4xr.framework.extensions.ltl.SATVerdict

Packages that use SATVerdict

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.

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

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

Modifier and Type	Field	Description
SATVerdict	LTL.LTLVerdictInfo.verdict

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

Modifier and Type	Method	Description
SATVerdict	BasicModelChecker.sat(Predicate<IExplorableState> q)	Check if the target program has an finite execution that ends in a state satisfying the predicate q.
SATVerdict	BasicModelChecker.sat(Predicate<IExplorableState> q, int maxDepth)	Check if the target program has an finite execution of the specified maximum length, that ends in a state satisfying the predicate q.
SATVerdict	BoundedLTL.sat()	Return the verdict of the last sat-checking.
SATVerdict	BoundedLTL.sat(List<Pair<ITransition,IState>> sequence)	This checks this BLTL formula on the given execution (list of pairs transition-state).
SATVerdict	BuchiModelChecker.sat(Buchi buchi)	Check if the target 'program' BuchiModelChecker.model can produce an infinite execution that would be accepted by the given Buchi automaton.
SATVerdict	BuchiModelChecker.sat(Buchi buchi, int maxDepth)	Check if the target program has an finite execution of the specified maximum length, that ends in a state satisfying the predicate q.
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.
SATVerdict	LTL.And.sat()
SATVerdict	LTL.Next.sat()
SATVerdict	LTL.Not.sat()
SATVerdict	LTL.Now.sat()
SATVerdict	LTL.Or.sat()
SATVerdict	LTL.Until.sat()
SATVerdict	LTL.WeakUntil.sat()
abstract SATVerdict	SequencePredicate.sat()	Return the result of the checking whether this predicate holds on the last sequence given to it.
SATVerdict	SequencePredicate.sat(List<State> sequenceOfStates)	Check is the given sequence of states (representing some execution) satisfies this LTL formula.
static SATVerdict	SATVerdict.valueOf(String name)	Returns the enum constant of this type with the specified name.
static SATVerdict[]	SATVerdict.values()	Returns an array containing the constants of this enum type, in the order they are declared.

Constructors in eu.iv4xr.framework.extensions.ltl with parameters of type SATVerdict

Modifier	Constructor	Description
(package private)	LTLVerdictInfo(SATVerdict v)