使用Alloy API为合金分析仪提供自定义实例

1 回答

• 2

  使用Alloy java API，您可以轻松地计算实例中的表达式 .

  • 使用CompUtil类的一种方法获取生成实例的模块 .

  • 然后检索您感兴趣的实例（之前保存在xml文件中），如下所示： A4SolutionReader.read(module.getAllReachableSigs(), new XMLNode(new File("full/path/to/yourInstance.xml"))) ;

  • 最后使用刚刚获得的A4Solution对象的eval（ExprVar e）方法来评估实例中的表达式 . （您需要使用computil类中的方法parseOneExpression_fromString从String中获取ExprVar对象 . ）

  如果您不愿意使用API，还有另一种方法可以单独使用分析器执行您想要执行的操作 . 它是对您的原始模型进行过度约束，以便只有您感兴趣的实例才能符合它 . 然后你只需检查你对这个模型的断言 .

  关于如何约束模型的一个小例子：

  假设你有一个模型：

  sig A{
  } 
  sig B{
    a:A
  }
  sig C{}
  

  并且您对该实例感兴趣：

  A:{A$0,A$1}
  B:{B$0} 
  a:> (B$0,A$0)
  C:{}
  

  然后你过度约束的模型将是：

  //=== model ====
  abstract sig A{
  } 
  abstract sig B{
    a:A
  }
  abstract sig C{}
  
  //==== instance ===
  one sig A_0,A_1 extends A{}
  one sig B_0 extends B{
  }{ 
     a=A_0
  }
  
  fact {
    no C // should be specified explicitly as the Alloy analyzer will instantiate abstract signatures if they are not inherited.   
  }
  

  回复于 2024-04-19T10:00:22+08:00