CPA的编写

CPA的编写主要是三个文件：CPA.java，State.java，TransferRelations.java，以Mytest为例。

首先编写MyTestState.java

MyTestState主要是通过继承AbstractState来实现，可以根据需要添加自己所需要的属性等，这里仅仅简单添加了一个depth变量来记录路径深度。

package org.sosy_lab.cpachecker.cpa.mytest;

import org.sosy_lab.cpachecker.core.interfaces.AbstractState;

public class MyTestState implements AbstractState {
  //继承自AbstractState类
  private int depth;                //可以自己添加所需要的属性等

  public MyTestState(int depth) {   //构造函数
    this.depth = depth;
  }

  @Override
  public int hashCode() {          //AbstractState中的方法，用于equal等方法的判断
    // TODO Auto-generated method stub
    return depth;
  }

  @Override
  public boolean equals(Object pObj) {
    // 对象相等判断
    if (!(pObj instanceof MyTestState)) {
      return false;
    }
    MyTestState ts = (MyTestState) pObj;
    return this.depth == ts.depth;
  }

  public int getDepth() {
    //自己定义的方法等
    return depth;
  }

  @Override
  public String toString() {
    return "depth:" + depth;
  }

}

然后编写MyTestTransferRelation.java

这个类主要是用来实现状态之间迁移相关的内容，可以继承SingleEdgeTransferRelation等类，实现的方法主要是获取后继抽象状态，例如getAbstractsuccessorsForEdge。

package org.sosy_lab.cpachecker.cpa.mytest;

import com.google.common.collect.Sets;
import java.util.Collection;
import org.sosy_lab.cpachecker.cfa.model.CFAEdge;
import org.sosy_lab.cpachecker.core.defaults.SingleEdgeTransferRelation;
import org.sosy_lab.cpachecker.core.interfaces.AbstractState;
import org.sosy_lab.cpachecker.core.interfaces.Precision;
import org.sosy_lab.cpachecker.exceptions.CPATransferException;


public class MyTestTransferRelation extends SingleEdgeTransferRelation {
  @Override
  public Collection<? extends AbstractState>
      getAbstractSuccessorsForEdge(AbstractState pState, Precision pPrecision, CFAEdge pCfaEdge)
          throws CPATransferException, InterruptedException {
    // TODO Auto-generated method stub
    MyTestState currentState = (MyTestState) pState;  ///将传入的抽象状态进行强制转换称自己定义的类
    System.out.println("NextState:" + (currentState.getDepth() + 1));    //用于打印深度相关的信息
    System.out.println(pCfaEdge);  //打印与边有关的信息

    return Sets.newHashSet(new MyTestState(currentState.getDepth() + 1));  //返回的是继承AbstractState类的子类的实例的集合，与返回值类型相对应。
  }

}

最后编写MyTestCPA.java

这里现在只使用了一个获取初始状态的方法，用来获取初始状态。

package org.sosy_lab.cpachecker.cpa.mytest;

import java.util.logging.Level;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.cpachecker.cfa.CFA;
import org.sosy_lab.cpachecker.cfa.model.CFANode;
import org.sosy_lab.cpachecker.core.defaults.AbstractCPA;
import org.sosy_lab.cpachecker.core.defaults.AutomaticCPAFactory;
import org.sosy_lab.cpachecker.core.interfaces.AbstractState;
import org.sosy_lab.cpachecker.core.interfaces.CPAFactory;
import org.sosy_lab.cpachecker.core.interfaces.StateSpacePartition;

public class MyTestCPA extends AbstractCPA {      //继承自AbstractCPA类
  public MyTestCPA(Configuration pConfig, LogManager pLogger, CFA pCfa)
      throws InvalidConfigurationException {
    super("sep", "sep", new MyTestTransferRelation());
    pLogger.log(
        Level.INFO,
        "When verifying concurrent programs, please keep the parameters of LocationsCPA consistent with those of ThreadingCPA!");
  }
  public static CPAFactory factory() {      //相当于注册函数，一定要有，直接复制就行
    return AutomaticCPAFactory.forType(MyTestCPA.class);
  }

  @Override
  public AbstractState getInitialState(CFANode pNode, StateSpacePartition pPartition)
      throws InterruptedException {
    // TODO Auto-generated method stub
    return new MyTestState(0);      //根据自己编写的MyTestState类来具体返回初始状态
  }

}

编写CPA时，首先在cpa目录下添加一个名为mytest的包，然后在包中分别编写三个文件。
在运行示例时候，需要配置特定的config文件，如果用到自己的CPA，那么需要在config文件中进行修改。记得在修改文件之后重新编译一下。

CPA的编写

原文：https://www.cnblogs.com/mujueke/p/14773722.html