verification - 合金映射关系

Question

我几乎开始研究合金来做一些验证。我正在尝试练习制作一些代表编程语言的简单结构。

映射实体具有程序和依赖关系

程序具有功能

函数有几行代码

依赖关系是一个实体，将程序中某个函数中的两行代码相互映射

这是我尝试做的，但输出图显示了一行代码，它链接到依赖元组但与函数不匹配。我需要所有代码行都在一个函数中，它们可以是依赖关系，也可以不是......

abstract sig mapping{}

sig Dependency extends mapping {dep0,dep1: one line}

one sig Program extends mapping{ F: some function, D: some Dependency }

//mapping entity is composed of Dependency pairs 2 lines of code 
//and one program which has functions and dependency pairs

sig function { Line : some line}
//Function is made of line of code

abstract sig line{}

run {}

Answer 1

您应该添加一些事实来强制执行您为模型考虑的约束。

例如，要强制每一行都有相应的功能，您可以编写类似的内容

fact LinesBelongToFunctions {
  all ln: line | 
    one f: function | 
      ln in f.Line
}

这一事实表明，对于每一行，都ln存在一个f包含f.Linesline的函数ln。