Package eu.iv4xr.framework.extensions.ltl

Class BasicModelChecker

java.lang.Object
eu.iv4xr.framework.extensions.ltl.BasicModelChecker
public class BasicModelChecker extends Object
Provide an explicit-state bounded and lazy model checker that can be used to check if a model contains a reachable state (within a given maximum depth) satisfying some predicate q. If one can be found, a witness in the form of an execution/path in the model that reaches such a state can be obtained. Note that failing to find such a witness means that ~q holds globally on all states within the maximum depth from the model's initial state.

The model checker can be used to target any 'program' or 'model of program' that implements the interface ITargetModel.

Additional functionalities are provided e.g. to find a minimum length witness and to produce a test-suite that covers all states of the model.

Author:
Wish

  • Field Details

    • model

      public ITargetModel model
      The 'program' or 'model of a program' that we want to target in model-checking.

    • stats

      public BasicModelChecker.MCStatistics stats
      Hold some basic statistics over the last model-checking run.

  • Constructor Details

    • BasicModelChecker

      public BasicModelChecker​(ITargetModel model)
      Create an instance of a model checker.
      Parameters:
      model - The 'program' to be model-checked.

  • Method Details

    • sat

      public SATVerdict sat​(Predicate<IExplorableState> q)
      Check if the target program has an finite execution that ends in a state satisfying the predicate q. If so, it returns SAT, and else UNSAT. Be careful that this method may not terminate if the target program has an infinite state space. Use sat(Predicate, int) instead.

    • sat

      public SATVerdict 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. If so, it returns SAT, and else UNSAT.

    • find

      public BasicModelChecker.Path<IExplorableState> 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. If so, it returns this execution, and else null.

    • findShortest

      public BasicModelChecker.Path<IExplorableState> findShortest​(Predicate<IExplorableState> q, int maxDepth)
      Similar to find(Predicate, int), but it will return the shortest execution (of the specified max-length) that ends in q.

    • dfs

      BasicModelChecker.Path<IExplorableState> 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. It is actually a Depth First Search (DFS) algorithm. We don't do double DSF because we only want to check state reachability.
      Parameters:
      whatToFind - predicate characterizing the state whose reachability is to be checked.
      pathSoFar - the path that leads to the parameter state given below.
      visitedStates - the set of all states visited so far by this DFS.
      state - the next state to explore.
      remainingDepth - speaks for itself :)
      Returns:

    • testSuite

      public <CoverageItem> BasicModelChecker.TestSuite<CoverageItem> testSuite​(List<CoverageItem> itemsToCover, Function<IExplorableState,​CoverageItem> coverageFunction, int maxLength, boolean minimizeLength)
      Return a test suite that tries to cover the specified coverage targets. Although the model-checking procedure is exhaustive up to the given maximum depth/length, note that it may not be possible to cover all the given targets. The returned test suite give a suite that would cover as much as possible.
      Type Parameters:
      CoverageItem - The type of coverage-targets.
      Parameters:
      itemsToCover - A list of targets to cover.
      coverageFunction - A function that maps the state of the target 'program' to a coverage target. Given a state s, this function maps s to a target. E.g. is s can be though to have some int variable x, this function can map s to 0 if s.x is 0 or less, and to 1 if s.x is 1, and to 2 if s.x is 2 or larger. So, implicitly this means that we would then have three possible coverage targets, namely 0,1,2.
      maxLength - The maximum length of the test-cases. The model checker will not try to find test-cases that are longer than this specified length.
      minimizeLength - If true, the model checker will also to minimize the length of each test-case. Note that the minimization is performed per test-case. This does not guarantee that the resulting test-suite would be minimal in the total number of steps. Minimizing the whole test-suite would be very expensive.
      Returns:
      The resulting test-suite.