/* Portia's Casket The Merchant of Venice, Act II, Scene VII: MOROCCO The first, of gold, who this inscription bears, 'Who chooseth me shall gain what many men desire;' The second, silver, which this promise carries, 'Who chooseth me shall get as much as he deserves;' This third, dull lead, with warning all as blunt, 'Who chooseth me must give and hazard all he hath.' How shall I know if I do choose the right? PORTIA The one of them contains my picture, prince: If you choose that, then I am yours withal. The following is a variation on this Shakespearian puzzle. The story goes that Portia is looking for a worthy husband, so a puzzle is created as a test. In this a variation she has the same three caskets, but with the following inscriptions: Gold: The portrait is in here. Silver: The portrait is in here. Lead: At least two of the inscriptions is false. */ /*Authors: Juergen Dingel, Queens University Glenn Robbins, Royal Military College of Canada Nov 2003 */ module portia open std/ord /*Define objects in the puzzle. Three types of objects; portrait, casket, and inscription. */ //Define a portrait sig Portrait{} //Define a casket that can contain 0 or 1 portrait sig Casket{ contents: lone Portrait} //Create the individual caskets sig gold extends Casket{} sig silver extends Casket{} sig lead extends Casket{} //Caskets are disjoint fact Disjoint{ (no gold & silver) && (no gold & lead) && (no silver & lead) } //Define inscriptions sig TrueInscriptions{ contents: set Casket} //Define the facts of the inscriptions on the caskets fact {all t: TrueInscriptions | (gold in t.contents <=> gold.contents = Portrait) && (silver in t.contents <=> silver.contents = Portrait) && (lead in t.contents <=> ((!gold in t.contents && !silver in t.contents) || (!silver in t.contents && !lead in t.contents) || (!gold in t.contents && !lead in t.contents) || (!gold in t.contents && !silver in t.contents && !lead in t.contents)))} //There is only one portrait, and one of each casket fact {one Portrait} fact {one gold && one silver && one lead} //There are no other caskets besides gold, silver and lead fact {all c:Casket| c=gold || c=silver || c=lead} //The protrait is in exactly one casket fact {all p:Portrait | one c:Casket | c.contents = p} /*The program will only return one possible solution each time it is executed. So, after a test has been executed, the following constraints can be incorporated to ensure that the portrait can't be in either of the other caskets. Uncomment one at a time.*/ //fact {gold.contents = Portrait} //fact {silver.contents = Portrait} //fact {lead.contents = Portrait} //Find solution fun show (){} run show for 3