Факт сплава НЕ оба свойства - PullRequest
Новая
       62

Факт сплава НЕ оба свойства

0 голосов
/ 13 ноября 2011

У меня есть фрагмент кода в ALLOY. Я пытаюсь создать систему бронирования в ресторанах, и у меня есть этот сигнал и связь между ними. 

abstract sig Table{
breakfast: one breakFast,
lunch: one Lunch,
dinner: one Dinner
}

sig Free{

}

sig Reserved{

}

sig breakFast {
breakfastfree:one Free,
breakfastReserved:one Reserved
}

sig Lunch {
Lunchfree:one Free,
LunchReserved:one Reserved

} 

sig Dinner  {
Dinnerfree:one Free,
 DinnertReserved:one Reserved
}


fact{
all t1,t2 : Table | t1 != t2 => t1.breakfast != t2.breakfast
all t1,t2 : Table | t1 != t2 => t1.lunch != t2.lunch
all t1,t2 : Table | t1 != t2 => t1.dinner != t2.dinner

 }

 pred RealismConstraints []{

 #Table = 4

 }
  run RealismConstraints for 20

Хочу привести факт, что на завтрак его можно зарезервировать или бесплатно НЕ ОБА, а на обед и ужин одно и то же, есть идеи?

1 Ответ

1 голос
/ 14 ноября 2011

Во-первых, то, как вы ограничили breakfastfree и breakfastReserved, всегда будет и тем и другим.Вам нужно использовать lone (без объекта или объекта): 

sig breakFast {
  breakfastfree:lone Free,
  breakfastReserved:lone Reserved
}

Затем вы можете написать факт: 

fact{
  all t: Table | let breakf = t.breakfast |
    #(breakf.breakfastfree+breakf.breakfastReserved) = 1
}

или, проще, просто: 

sig breakFast {
  breakfastfree: lone Free,
  breakfastReserved: lone Reserved
}
{
  #(breakfastfree+breakfastReserved) = 1
}

Тем не менее, я бы посоветовал вам использовать что-то вроде 

sig breakFast {
    breakfastReserved: lone Reserved
}

и относиться к no breakfastReserved как к «свободному».Тебе больше не нужны никакие факты.

...