[SOLVED] Alloy fact NOT both properties

Alloy fact NOT both properties

I have a piece of code in ALLOY I am trying to do a restaurant reservation system and I have this sig and relation between them.

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

I want to put a fact that for breakfast it can be reserved or free NOT BOTH and in lunch and dinner the same thing any ideas?

Solution

First, the way you've constrained breakfastfree and breakfastReserved it will always be both. You need to use lone (no object or one):

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

Then, you could write the fact:

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

or, simpler, just:

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

However, I'd suggest that you just go with something like

sig breakFast {
    breakfastReserved: lone Reserved
}

and treat no breakfastReserved as "free". You don't need any further facts then.