Interface StopOperator<StateT extends AbstractState<StateT>>

Type Parameters:
StateT - The type of the analyzed states.
All Known Implementing Classes:
StopAlwaysOperator, StopContainedOperator, StopJoinOperator, StopNeverOperator, StopSepOperator

public interface StopOperator<StateT extends AbstractState<StateT>>
The StopOperator decides if CpaAlgorithm should stop.
  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    stop(StateT abstractState, Collection<StateT> reachedAbstractStates, Precision precision)
    The operator may decide based on the (generalized under the given precision) convergence.
  • Method Details

    • stop

      boolean stop(StateT abstractState, Collection<StateT> reachedAbstractStates, Precision precision)
      The operator may decide based on the (generalized under the given precision) convergence. In this case it needs to look up the abstractState in the reachedAbstractStates. Otherwise, it can return true if sufficient information is collected, e.g., a safety property is violated.