合金映射关系

Question

我非常开始研究合金做一些验证。我正在尝试为表示编程语言的简单结构做些事情。

一个变换实体具有程序和依赖关系

一个程序具有以下功能：

函数具有的代码行

依赖关系是，2行代码映射在一些功能的实体在程序彼此之间

这是我试图做的，但输出图显示是链接到依赖元组但与该函数不匹配的一行代码。我需要的所有代码行是在一个功能，他们可以在依赖或不...

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.Lines包含行ln。