有时候，当我想在合金使用递归，我发现我可以传递闭包，或序列度日。 例如，在上下文无关文法的模型： abstract sig Symbol {}
sig NT, T extends Symbol {}
// A grammar is a tuple(V, Sigma, Rules, Start)
one sig Grammar {
V : set NT,
Sigma :
我必须在大学项目的需求分析和规范文档中使用合金。我从简单的东西开始，只有签名和事实。这是我使用的签名： abstract sig Date{
year: one Int,
month: one Int,
day: one Int
}
abstract sig Time{
h: one Int,
m: one Int,
s: one
我试图使用拓扑排序来找到遵循它们的先决条件的两个不同的顺序计划。当我执行代码时，没有找到实例，我不知道为什么。这里是我的代码： open util/relation
abstract sig Course {
prereq: set Course, -- c->d in prereq if c is a prerequisite of d
s1, s2: set Cours
我有一个模型来指定任务之间的任务和关系。其实我有不同的关系，但为了让它更简单，我们假设只有一种。简单的代码如下： open util/ordering[Time]
sig Time {}
abstract sig State {}
lone sig Enabled extends State {}
lone sig Disabled extends State {}
sig Tas
我运行，涉及到寻找证人对某些existentials合金命令，像这样的： pred foo {
some x, y : E -> E |
baz[x,y] || qux[x,y]
}
合金来了一个模型，其中foo是真实的。我看着展示台中的模型，发现y恰好是空的关系。我想深入挖掘模型，看看baz或qux是否为真。所以我启动了Evaluator窗口并输入baz[$foo_x,