predicate - 合金事实不是两种特性

Question

我在 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

我想说明一个事实，早餐可以预订或免费，午餐和晚餐都一样，有什么想法吗？

Answer 1

首先，你限制的方式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视为“免费”。那你就不需要更多的事实了。