Alloy中的sig文字

Question

如何为Alloy中的信号写出文字？考虑下面的示例。

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

如果执行此操作，我会得到

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

在评估器中，我知道我可以使用Foo来引用Foo$0实例，但是如何编写表示相同值的文字？

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

Answer 1

atoms，因为该模型正在定义这些原子的所有可能值。但是，很多时候，您需要在

some原子上使用hands进行推理。也就是说，您希望能够name一些对象。

获得“常量”的最佳方法是创建一个从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可以利用它们。 （这将允许更快地求解，并且对于模型的测试案例非常有用。）但是，在讨论中，我介绍了该解决方案，并且不需要任何新语法。