Uses of Interface
eu.iv4xr.framework.extensions.ltl.IExplorableState

Packages that use IExplorableState

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.extensions.ltl.gameworldmodel	Provide a class, GameWorldModel, that can be used as a model of a "computer game".

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

Fields in eu.iv4xr.framework.extensions.ltl with type parameters of type IExplorableState

Modifier and Type	Field	Description
Predicate<IExplorableState>	Buchi.BuchiTransition.condition	The predicate that guard the transition.

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

Modifier and Type	Method	Description
IExplorableState	IExplorableState.clone()
IExplorableState	ITargetModel.getCurrentState()

Methods in eu.iv4xr.framework.extensions.ltl that return types with arguments of type IExplorableState

Modifier and Type	Method	Description
(package private) BasicModelChecker.Path<IExplorableState>	BasicModelChecker.dfs(Predicate<IExplorableState> whatToFind, BasicModelChecker.Path<IExplorableState> pathSoFar, Collection<IExplorableState> visitedStates, IExplorableState state, int remainingDepth)	Implement the 'lazy model checking' algorithm similar to what is used by the SPIN model checker.
(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<IExplorableState>	BasicModelChecker.find(Predicate<IExplorableState> q, int maxDepth)	Do model-checking to find a finite execution (of the given max-length) of the target program that ends in a state satisfying the predicate q.
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.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<IExplorableState>	BasicModelChecker.findShortest(Predicate<IExplorableState> q, int maxDepth)	Similar to BasicModelChecker.find(Predicate, int), but it will return the shortest execution (of the specified max-length) that ends in q.
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.
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.

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

Modifier and Type	Method	Description
(package private) BasicModelChecker.Path<IExplorableState>	BasicModelChecker.dfs(Predicate<IExplorableState> whatToFind, BasicModelChecker.Path<IExplorableState> pathSoFar, Collection<IExplorableState> visitedStates, IExplorableState state, int remainingDepth)	Implement the 'lazy model checking' algorithm similar to what is used by the SPIN model checker.
List<Pair<Buchi.BuchiTransition,Integer>>	Buchi.getEnabledTransitions(IExplorableState state)	Check which of transitions of this Buchi, that go from from it current state, would be semantically possible/enabled given the concrete state of the environment with which this Buchi is executed.

Method parameters in eu.iv4xr.framework.extensions.ltl with type arguments of type IExplorableState

Modifier and Type	Method	Description
(package private) BasicModelChecker.Path<IExplorableState>	BasicModelChecker.dfs(Predicate<IExplorableState> whatToFind, BasicModelChecker.Path<IExplorableState> pathSoFar, Collection<IExplorableState> visitedStates, IExplorableState state, int remainingDepth)	Implement the 'lazy model checking' algorithm similar to what is used by the SPIN model checker.
(package private) BasicModelChecker.Path<IExplorableState>	BasicModelChecker.dfs(Predicate<IExplorableState> whatToFind, BasicModelChecker.Path<IExplorableState> pathSoFar, Collection<IExplorableState> visitedStates, IExplorableState state, int remainingDepth)	Implement the 'lazy model checking' algorithm similar to what is used by the SPIN model checker.
(package private) BasicModelChecker.Path<IExplorableState>	BasicModelChecker.dfs(Predicate<IExplorableState> whatToFind, BasicModelChecker.Path<IExplorableState> pathSoFar, Collection<IExplorableState> visitedStates, IExplorableState state, int remainingDepth)	Implement the 'lazy model checking' algorithm similar to what is used by the SPIN model checker.
(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.
(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.
(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<IExplorableState>	BasicModelChecker.find(Predicate<IExplorableState> q, int maxDepth)	Do model-checking to find a finite execution (of the given max-length) of the target program that ends in a state satisfying the predicate q.
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<IExplorableState>	BasicModelChecker.findShortest(Predicate<IExplorableState> q, int maxDepth)	Similar to BasicModelChecker.find(Predicate, int), but it will return the shortest execution (of the specified max-length) that ends in q.
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.
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	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.
<CoverageItem> BasicModelChecker.TestSuite<CoverageItem>	BasicModelChecker.testSuite(List<CoverageItem> itemsToCover, Function<IExplorableState,CoverageItem> coverageFunction, int maxLength, boolean minimizeLength)	Return a test suite that tries to cover the specified coverage targets.
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.

Uses of IExplorableState in eu.iv4xr.framework.extensions.ltl.gameworldmodel

Classes in eu.iv4xr.framework.extensions.ltl.gameworldmodel that implement IExplorableState

Modifier and Type	Class	Description
class	GWState	Representing the state of the game-world; or more precisely a state in GameWorldModel.

Methods in eu.iv4xr.framework.extensions.ltl.gameworldmodel that return IExplorableState

Modifier and Type	Method	Description
IExplorableState	GWState.clone()