合金中的 sig 文字答案

【问题标题】：sig literals in Alloy合金中的 sig 文字
【发布时间】：2020-01-03 14:30:56
【问题描述】：

如何在 Alloy 中为 sig 写出文字？考虑下面的例子。

sig Foo { a: Int }
fact { #Foo = 1 }

如果我执行这个，我会得到

| this/Foo | a |
|----------|---|
| Foo⁰     | 7 |

在求值器中，我知道我可以使用Foo$0 获得对Foo 实例的引用，但我如何编写表示相同值的文字？

我试过{a: 7}，但这不等于Foo$0。这故意是一个微不足道的例子，但我正在调试一个更复杂的模型，我需要能够写出具有多个字段的 sig 文字。

【问题讨论】：

标签： alloy

【解决方案1】：

啊，这是隐藏得很好的秘密之一！ :-) 很明显，在您的模型中，您不能引用 atoms，因为该模型正在定义这些原子的所有可能值。然而，很多时候你需要你的手在一些原子上来推理它。也就是说，您希望能够命名一些对象。

获得“常量”的最佳方法是创建一个从run 子句调用的谓词。在这个谓词中，您为要讨论的原子定义名称。你只需要确保这个谓词是true。

pred collision[ car1, car2 : Car, road : Road ] {
   // here you can reason about car1 and car2
}
run collision for 10

另一种方法是在您需要一些命名对象时创建量化：

run  {
   some car1, car2 : Car, road : Road {
      // here you can reason about car1 and car2 and road
   }
} for 10

有一个recent discussion 将这些实例添加到语言中，以便Kodkod 可以利用它们。（这将允许更快的求解，并且对于模型的测试用例非常有用。）但是，在讨论期间，我提出的这个解决方案出现了，它不需要任何新的语法。

【讨论】：

在求值器中，我已经可以引用已经创建的常量了。但我的问题是我想构造模型不直接定义的常量。在上面的示例中，假设我想构造一个a 值为6 的Foo 实例。如果不修改模型就没有办法做到这一点吗？如果我每次都需要更改模型，这将使调试变得相当具有挑战性。
您可以使用特定的调试谓词来做到这一点。您可以将您的模型包含在 debug 模型中，这样这些测试/调试谓词就不会污染您的模型。但是，恕我直言，它们可能是您模型中对新手最感兴趣的部分。
我不明白这将如何解决我的问题。假设在我的示例中，我想要一个 Foo 实例，其中 a 为 6。我将如何编写调试谓词来获取这样的实例，以便将其传递给函数？
如果我事先知道我想要a=6，但这并没有真正的交互帮助。

【解决方案2】：

尝试在“运行”命令中限制“整数”。我的意思是：

sig Foo {a : Int}
fact{ #Foo = 1}

pred show {}
run show for 1 Foo, 2 Int

【讨论】：