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

Packages that use Buchi

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 Buchi in eu.iv4xr.framework.extensions.ltl

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

Modifier and Type	Method	Description
(package private) Buchi	Buchi.appendStateNames(String suffix)	Rename the states in this Buchi, by adding the given string as a suffix to each state-name.
static Buchi	LTL2Buchi.getBuchi(LTL<IExplorableState> phi)	Translate the given LTL formula to a Buchi automaton.
(package private) Buchi	Buchi.insertNewState(String st)	Insert a new state with the given name.
Buchi	Buchi.treeClone()	Construct a new Buchi that is a "clone" of this Buchi.
Buchi	Buchi.withInitialState(String sinit)	Set the initial state of this Buchi.
Buchi	Buchi.withNonOmegaAcceptance(String... NonOstates)	Set the set of non-omega-accepting states.
Buchi	Buchi.withOmegaAcceptance(String... Ostates)	Set the set of omega-accepting states.
Buchi	Buchi.withStates(String... stateNames)	Set the states of this Buchi to the given states.
Buchi	Buchi.withTransition(String from, String to, String transitionId, String transitionName, Predicate<IExplorableState> condition)	Add the given transition to this Buchi.
Buchi	Buchi.withTransition(String from, String to, String transitionId, Predicate<IExplorableState> condition)	The same as the other withTransition.

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

Modifier and Type	Method	Description
(package private) BasicModelChecker.Path<Pair<IExplorableState,Integer>>	BuchiModelChecker.dfsBuchi(Buchi buchi, BasicModelChecker.Path<Pair<IExplorableState,Integer>> pathSoFar, Set<Pair<IExplorableState,Integer>> statesInPathToStartOfPossibleCycle, Set<Pair<IExplorableState,Integer>> visitedStates, Pair<IExplorableState,Integer> state, int remainingDepth)	The worker of our LTL model-checking algorithm.
BasicModelChecker.Path<Pair<IExplorableState,String>>	BuchiModelChecker.find(Buchi buchi, int maxDepth)	Check if the target 'program' BuchiModelChecker.model can produce an infinite execution that would be accepted by the given Buchi automaton.
BasicModelChecker.Path<Pair<IExplorableState,String>>	BuchiModelChecker.findShortest(Buchi buchi, int maxDepth)	Similar to BuchiModelChecker.find(Buchi, int), but it will return the shortest execution (of the specified max-length) that satisfies the Buchi.
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.