使用所有已定义关系的子集

Question

module test

sig Foo {}

sig A {
    b: set B,
    foo: one Foo
}

sig B {
    foo: one Foo
}

assert foo {
    all s: (univ - Foo) | all rel: (univ - Foo) -> (univ - Foo) |
    s not in s.*rel
}

check foo for 2

假设我正在试图在一个断言中定义一个关系，该断言中说：“除了Foo以及包括Foo的关系之外，没有循环”（在这里通过检查是正确的）。

上面的断言创建了一些$foo_rel关系，这些关系最初并未在模型中定义。如何将其限制为仅在sig中指定的关系？

Answer 1

变量$foo_rel和$foo_s是由于简化而引入的，因为您要对2个元组进行量化。 （就我个人而言，到目前为止，我一直忽略了skolemization的细节，只讨厌它不起作用的时候。）

但是，我认为这不是您的问题。我运行的模型没有整数：

check foo for 2 but 0 int

这提供了以下解决方案：

---INSTANCE---
integers={}
univ={B$0, Foo$0}
Int={}
seq/Int={}
String={}
none={}
this/Foo={Foo$0}
this/A={}
this/A<:b={}
this/A<:foo={}
this/B={B$0}
this/B<:foo={B$0->Foo$0}
skolem $foo_s={B$0}
skolem $foo_rel={B$0->B$0}

[当我们去评估者时，我们可以逐步进行量化：

> univ-Foo
┌──┐
│B⁰│
└──┘
> (univ - Foo) -> (univ - Foo)
┌──┬──┐
│B⁰│B⁰│
└──┴──┘

很明显，如果您对all rel: (univ - Foo) -> (univ - Foo)进行量化，则将包括循环。

> B⁰.*((univ - Foo) -> (univ - Foo))
┌──┐
│B⁰│
└──┘

我认为合金模型的工作方式存在一些误解。我希望这有助于更好地探索这些模型？