Использование подмножества всех определенных отношений - PullRequest
Новая
       15

Использование подмножества всех определенных отношений

0 голосов
/ 28 января 2020 
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 s?

1 Ответ

0 голосов
/ 29 января 2020

Переменные $foo_rel и $foo_s введены из-за сколемизации, так как вы выполняете количественную оценку по кортежу arity 2. (Лично я до сих пор игнорировал детали сколемизации и ненавижу ее только тогда, когда она не работает.)

Однако я не думаю, что это ваша проблема. Я запустил модель без целых чисел: 

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}

Когда мы go оцениваем, мы можем выполнить ваши количественные измерения шаг за шагом: 

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

Понятно, что при количественном определении по all rel: (univ - Foo) -> (univ - Foo) это будет включать циклы. 

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

Я думаю, что существует некоторое недопонимание того, как работают модели Alloy. Надеюсь, это поможет немного лучше изучить эти модели?

...