接口 StopOperator<StateT extends AbstractState<StateT>>

类型参数:
StateT - The type of the analyzed states.
所有已知实现类:
StopAlwaysOperator, StopContainedOperator, StopJoinOperator, StopNeverOperator, StopSepOperator

public interface StopOperator<StateT extends AbstractState<StateT>>
The StopOperator decides if CpaAlgorithm should stop.
  • 方法概要

    修饰符和类型
    方法
    说明
    boolean
    stop(StateT abstractState, Collection<StateT> reachedAbstractStates, Precision precision)
    The operator may decide based on the (generalized under the given precision) convergence.
  • 方法详细资料

    • 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.