Найден неожиданный экземпляр для спецификации сплава - PullRequest
Новая
       28

Найден неожиданный экземпляр для спецификации сплава

0 голосов
/ 19 октября 2018

Я попробовал свои первые шаги в моделировании с Alloy и столкнулся с проблемой, которую я не могу понять.У меня есть следующая спецификация: 

module tour/AddressBook1

sig Name, Addr{}
sig Book {
    addr: Name->lone Addr
}

// operation: adds a (name, address) to the Book b, resulting in b'
pred add (b, b' : Book, n:Name, a:Addr) {
    b'.addr = b.addr + n->a
}

run add for 3 but 2 Book

Пока ничего особенного.Это буквально пример книги Дэниела Джексона «Абстракция программного обеспечения».

По сути, он моделирует книги, с которыми связаны (имя, адрес) пары.Предикат add должен захватить экземпляр Book b и создать из него еще один экземпляр Book b, добавив к нему (потенциально уже существующую) (name, address) -pair.

Первые нескольконайденные примеры просты и убедительны, но, нажимая кнопку «Далее», я получаю следующий пример (полный вид выше, эквивалентный прогноз по книгам ниже)

Found instance

Я вижу двакниги, стартовая книга Book0 с двумя парами (Name0, Addr2) и (Name1, Addr1).Из аннотаций также видно, что операция добавления собирается добавить новый дуэт (Name1, Addr2).Теперь, когда я смотрю на книгу результатов Book1, у меня есть {(Name0, Addr0), (Name1, Addr2)} вместо {(Name0, Addr2), (Name1, Addr1), (Name1, Addr2)}

Почему это считается юридической инстанцией?

(Alloy Analyzer 4.2, дата сборки 2012-09-25 15:54 EDT)

1 Ответ

0 голосов
/ 19 октября 2018

Здесь есть две запутанные вещи:

  1. Book0 не участвует в операции.Вместо этого Book1 играет роль b0 и b1.

  2. Добавление n->a в книгу не означает, что это новый адрес.В данном случае Book1 имеет этот адрес до и после add.Это связано с тем, что операция 

    b'.addr = b.addr + n->a

    использует set union .Ниже приведен более простой пример: 

    {1, 2} = {1} + {2}

    верно.Но 

    {1, 2} = {1, 2} + {2}

    тоже верно.Таким образом, в исходном примере нет ничего, что исключает n->a из того, чтобы уже быть частью b.addr.А Alloy Analyzer просто генерирует все экземпляры, которые соответствуют заданным ограничениям.

Вы можете улучшить этот пример, добавив утверждение в add: 

    b.addr[n] != a
...