diff --git a/Einstein/Einstein.tla b/Einstein/Einstein.tla index a523a4e6ec240f2e9cc18089a621b4d519c63931..50385584e4510ede4a944882082fef0d3386e905 100644 --- a/Einstein/Einstein.tla +++ b/Einstein/Einstein.tla @@ -127,18 +127,6 @@ BlendSmokerHasWaterDrinkingNeighbor == (* Solution *) (************) -Init == - /\ drinks \in { p \in DRINKS : p[3] = "mylk" } - /\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian" } - /\ colors \in { p \in COLORS : p[2] = "blue" } - /\ pets \in PETS - /\ cigars \in CIGARS - -Next == - UNCHANGED <<nationality, colors, cigars, pets, drinks>> - -Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>> - Solution == /\ BritLivesInTheRedHouse /\ SwedeKeepsDogs @@ -158,4 +146,17 @@ Solution == FindSolution == ~Solution +Init == + /\ drinks \in { p \in DRINKS : p[3] = "mylk" } + /\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian" } + /\ colors \in { p \in COLORS : p[2] = "blue" } + /\ pets \in PETS + /\ cigars \in CIGARS + +Next == + UNCHANGED <<nationality, colors, cigars, pets, drinks>> + +Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>> + + ============================================================