From 6c89843756805e61e7761490120a181406e799d1 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Sun, 8 Sep 2024 10:08:34 +0200
Subject: [PATCH] move defs
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
Einstein/Einstein.tla | 25 +++++++++++++------------
1 file changed, 13 insertions(+), 12 deletions(-)
diff --git a/Einstein/Einstein.tla b/Einstein/Einstein.tla
index a523a4e..5038558 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>>
+
+
============================================================
--
GitLab