0

私は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

私は朝食のためにそれが両方ではなく予約または無料であることができて、そして昼食と夕食で同じことを何か考えがあるという事実を置きたいですか？

4

1 に答える 1

1

まず、あなたが制約した方法breakfastfreeとbreakfastReservedそれは常に両方になります。使用する必要がありますlone（オブジェクトなしまたは1つ）：

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そして「無料」として扱います。その場合、それ以上の事実は必要ありません。

于 2011-11-14T08:28:05.387 に答える