Uses of Class
eu.iv4xr.framework.extensions.ltl.BasicModelChecker.Path
Package
Description
This package provides the following features:
The classes
LTL
and BoundedLTL
implementing Linear Temporal Logic
formulas, and the bounded variation of them.-
Uses of BasicModelChecker.Path in eu.iv4xr.framework.extensions.ltl
Modifier and TypeFieldDescriptionBasicModelChecker.TestSuite.tests
The test-cases that constitute this test suite.Modifier and TypeMethodDescription(package private) BasicModelChecker.Path<State>
BasicModelChecker.Path.copy()
(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.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.Check if the target 'program'BuchiModelChecker.model
can produce an infinite execution that would be accepted by the given Buchi automaton.BuchiModelChecker.find(LTL<IExplorableState> phi, int maxDepth)
The same asBuchiModelChecker.find(Buchi, int)
, but it takes an LTL formula for specifying the pattern of the execution to find.BasicModelChecker.findShortest(Predicate<IExplorableState> q, int maxDepth)
Similar toBasicModelChecker.find(Predicate, int)
, but it will return the shortest execution (of the specified max-length) that ends in q.BuchiModelChecker.findShortest(Buchi buchi, int maxDepth)
Similar toBuchiModelChecker.find(Buchi, int)
, but it will return the shortest execution (of the specified max-length) that satisfies the Buchi.BuchiModelChecker.findShortest(LTL<IExplorableState> phi, int maxDepth)
Similar toBuchiModelChecker.find(LTL, int)
, but it will return the shortest execution (of the specified max-length) that satisfies the given LTL.Modifier and TypeMethodDescription(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.