Есть объект в том или ином наборе, но не в обоих?

Это домашнее задание, и у меня много проблем с ним. Я использую Alloy для моделирования библиотеки. Вот определения объектов:

sig Library {
    patrons : set Person,
    on_shelves : set Book,
}

sig Book {
    authors : set Person,
    loaned_to : set Person,
}

sig Person{}

Тогда нам нужно иметь факт, который гласит, что каждая книга либо на полке, либо достается покупателю. Однако они не могут быть в обоих местах.

// Every book must either be loaned to a patron or
// on the shelves.
fact AllBooksLoanedOrOnShelves {}

Я пробовал это...

fact AllBooksLoanedOrOnShelves {
    some b : Book {
        one b.loaned_to =>
            no (b & Library.on_shelves)
        else
            b in Library.on_shelves
    }
}

Но не получается... книги всегда на полках. хочется сказать: «Для каждой книги, если она не выдается напрокат, она стоит на полке. В противном случае она отсутствует».

Исправления, примеры и подсказки приветствуются.


alloy
person Ethan Mick    schedule 17.09.2011    source источник
comment
Почему бы не начать с двух утверждений? Для всех книг книга находится на полке или (xor) отсутствует. Для всех книг фраза «книга взята во временное пользование» означает, что она отсутствует. Кажется, что если вы начнете с этого, вам будет над чем работать, если вы хотите составить составное утверждение.   -  person ccoakley    schedule 15.11.2011

Ответы (5)


arrow_upward
1
arrow_downward

Ваш fact неверен. Вы хотите сказать что-то обо всех книгах (не «некоторых»). И это что-то в основном XOR.

Вот тот, который работает:

fact AllBooksLoanedOrOnShelves{
  all b : Book|
    (b in Library.on_shelves and no p:Person | p in b.loaned_to)
    or
    (not b in Library.on_shelves and one p:Person | p in b.loaned_to)
}
person Michalis Famelis    schedule 29.07.2012
comment
Честно говоря, этот вопрос так далек от моих мыслей, я не уверен, правильно это или нет, но я дам его вам. - person Ethan Mick; 26.12.2012

arrow_upward
4
arrow_downward

Если каждая книга должна быть либо отдана кому-то взаймы, либо стоять на полках, то (а) ни одна книга не будет находиться одновременно взаймы и на полках (при условии, что вы имеете в виду, что «или» является исключительным), поэтому пересечение предоставленного взаймы множества и набор на полке будет пустым, и (b) набор книг будет равен объединению наборов на полке и в аренде.

Набор книг, взятых напрокат в любое время, является доменом отношения loaned_to. Набор книг на полке в данной библиотеке L равен значению L.onshelves; набор книг на полках во всех известных библиотеках равен Library.onshelves.

Так что вы могли бы сказать

fact in_or_out_not_both {
  no Library.onshelves & loaned_to.Person 
}
fact all_books_in_or_out {
  Book = Library.onshelves + loaned_to.Person
}

Или вам может понадобиться сказать немного разные вещи, в зависимости от того, что вы имеете в виду. Обратите внимание, что эти ограничения не говорят о том, что книга взаймы должна быть предоставлена ​​взаймы одному заемщику.

person C. M. Sperberg-McQueen    schedule 16.08.2012

arrow_upward
1
arrow_downward

Хорошо, поправьте меня, если я ошибаюсь, но я считаю, что это тот факт, который вам нужен:

fact {
  disj[Library.on_shelves, Person.~loaned_to]
}

И небольшое пояснение. Library.on_shelves — это набор книг в правой части отношения on_shelves, т. е. все книги, находящиеся на полках. ~loaned_to — это отношение, обратное типу Person -> Book, а Person.~loaned_to — это набор книг, предоставленных любому лицу.

Предикат disj объявляет, что два множества не имеют общих атомов (непересекающихся множеств).

person Aviad P.    schedule 13.11.2012

arrow_upward
0
arrow_downward

Я не очень хорошо знаком с Alloy. Но я думаю, что это или что-то подобное будет работать.

Каждая книга либо стоит на полках, либо одолжена покровителю.

fact AllBooksLoanedOrOnShelves {
all b: Book | b in Library.on_shelves || b.loaned_to in Library.patrons
}
person Appleman1234    schedule 10.02.2012

arrow_upward
0
arrow_downward

Этому вопросу уже 6 лет, но я изучаю Alloy и хотел предложить свое решение.

fact AllBooksLoanedOrOnShelves {
    no (Library.on_shelves & loaned_to.Person)
}

Это можно прочитать как «пересечение множества книг, стоящих на полках, и множества книг, которые выдаются напрокат, пусто».

person rreillo    schedule 27.03.2018