From 00b4d5e51d7129367d4d6d55daf2eb17091f25a0 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Jan 2024 08:57:21 -0800 Subject: [PATCH 1/3] Make Einstein work with Apalache Signed-off-by: Giuliano Losa --- specifications/EinsteinRiddle/Einstein.tla | 65 +++++++++++++--------- 1 file changed, 38 insertions(+), 27 deletions(-) diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index 0797ec70..cdf0659d 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -35,12 +35,14 @@ EXTENDS Naturals, FiniteSets +House == 1..5 + \* Note that TLC!Permutations has a Java module override and, thus, \* would be evaluated faster. However, TLC!Permutations equals a \* set of records whereas Permutation below equals a set of tuples/ \* sequences. Also, Permutation expects Cardinality(S) = 5. Permutation(S) == - { p \in [ 1..5 -> S ] : + { p \in [ House -> S ] : /\ p[2] \in S \ {p[1]} /\ p[3] \in S \ {p[1], p[2]} /\ p[4] \in S \ {p[1], p[2], p[3]} @@ -51,17 +53,22 @@ Permutation(S) == \* parameterization, the constants are replaced with constant-level \* operators. As a side-effect, TLC evaluates them eagerly at startup, \* and Apalache successfully determines their types. -NATIONALITIES == Permutation({ "brit", "swede", "dane", "norwegian", "german" }) -DRINKS == Permutation({ "beer", "coffee", "mylk", "tea", "water" }) -COLORS == Permutation({ "red", "white", "blue", "green", "yellow" }) -PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" }) -CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" }) +NATIONALITIES == Permutation({ "brit_OF_NATIONALITY", "swede_OF_NATIONALITY", "dane_OF_NATIONALITY", "norwegian_OF_NATIONALITY", "german_OF_NATIONALITY" }) +DRINKS == Permutation({ "beer_OF_DRINK", "coffee_OF_DRINK", "mylk_OF_DRINK", "tea_OF_DRINK", "water_OF_DRINK" }) +COLORS == Permutation({ "red_OF_COLOR", "white_OF_COLOR", "blue_OF_COLOR", "green_OF_COLOR", "yellow_OF_COLOR" }) +PETS == Permutation({ "bird_OF_PET", "cat_OF_PET", "dog_OF_PET", "fish_OF_PET", "horse_OF_PET" }) +CIGARS == Permutation({ "blend_OF_CIGAR", "bm_OF_CIGAR", "dh_OF_CIGAR", "pm_OF_CIGAR", "prince_OF_CIGAR" }) VARIABLES + \* @type: Int -> NATIONALITY; nationality, \* tuple of nationalities + \* @type: Int -> COLOR; colors, \* tuple of house colors + \* @type: Int -> PET; pets, \* tuple of pets + \* @type: Int -> CIGAR; cigars, \* tuple of cigars + \* @type: Int -> DRINK; drinks \* tuple of drinks ------------------------------------------------------------ @@ -70,44 +77,44 @@ VARIABLES (* Rules *) (*********) -BritLivesInTheRedHouse == \E i \in 2..5 : nationality[i] = "brit" /\ colors[i] = "red" +BritLivesInTheRedHouse == \E i \in 2..5 : nationality[i] = "brit_OF_NATIONALITY" /\ colors[i] = "red_OF_COLOR" -SwedeKeepsDogs == \E i \in 2..5 : nationality[i] = "swede" /\ pets[i] = "dog" +SwedeKeepsDogs == \E i \in 2..5 : nationality[i] = "swede_OF_NATIONALITY" /\ pets[i] = "dog_OF_PET" -DaneDrinksTea == \E i \in 2..5 : nationality[i] = "dane" /\ drinks[i] = "tea" +DaneDrinksTea == \E i \in 2..5 : nationality[i] = "dane_OF_NATIONALITY" /\ drinks[i] = "tea_OF_DRINK" -GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i + 1] = "white" +GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green_OF_COLOR" /\ colors[i + 1] = "white_OF_COLOR" -GreenOwnerDrinksCoffee == \E i \in 1..5 \ {3} : colors[i] = "green" /\ drinks[i] = "coffee" +GreenOwnerDrinksCoffee == \E i \in 1..5 \ {3} : colors[i] = "green_OF_COLOR" /\ drinks[i] = "coffee_OF_DRINK" -SmokesPallmallRearsBirds == \E i \in 1..5 : cigars[i] = "pm" /\ pets[i] = "bird" +SmokesPallmallRearsBirds == \E i \in 1..5 : cigars[i] = "pm_OF_CIGAR" /\ pets[i] = "bird_OF_PET" -YellowOwnerSmokesDunhill == \E i \in 1..5 : colors[i] = "yellow" /\ cigars[i] = "dh" +YellowOwnerSmokesDunhill == \E i \in 1..5 : colors[i] = "yellow_OF_COLOR" /\ cigars[i] = "dh_OF_CIGAR" -CenterDrinksMylk == drinks[3] = "mylk" +CenterDrinksMylk == drinks[3] = "mylk_OF_DRINK" -NorwegianFirstHouse == nationality[1] = "norwegian" +NorwegianFirstHouse == nationality[1] = "norwegian_OF_NATIONALITY" BlendSmokerLivesNextToCatOwner == \E i \in 1..4 : - \/ cigars[i] = "blend" /\ pets[i + 1] = "cat" - \/ pets[i] = "cat" /\ cigars[i + 1] = "blend" + \/ cigars[i] = "blend_OF_CIGAR" /\ pets[i + 1] = "cat_OF_PET" + \/ pets[i] = "cat_OF_PET" /\ cigars[i + 1] = "blend_OF_CIGAR" HorseKeeperLivesNextToDunhillSmoker == \E i \in 1..4 : - \/ cigars[i] = "dh" /\ pets[i + 1] = "horse" - \/ pets[i] = "horse" /\ cigars[i + 1] = "dh" + \/ cigars[i] = "dh_OF_CIGAR" /\ pets[i + 1] = "horse_OF_PET" + \/ pets[i] = "horse_OF_PET" /\ cigars[i + 1] = "dh_OF_CIGAR" -BluemasterSmokerDrinksBeer == \E i \in 1..5 : cigars[i] = "bm" /\ drinks[i] = "beer" +BluemasterSmokerDrinksBeer == \E i \in 1..5 : cigars[i] = "bm_OF_CIGAR" /\ drinks[i] = "beer_OF_DRINK" -GermanSmokesPrince == \E i \in 2..5 : nationality[i] = "german" /\ cigars[i] = "prince" +GermanSmokesPrince == \E i \in 2..5 : nationality[i] = "german_OF_NATIONALITY" /\ cigars[i] = "prince_OF_CIGAR" -NorwegianLivesNextToBlueHouse == colors[2] = "blue" \* since the norwegian lives in the first house +NorwegianLivesNextToBlueHouse == colors[2] = "blue_OF_COLOR" \* since the norwegian_OF_NATIONALITY lives in the first house BlendSmokerHasWaterDrinkingNeighbor == \E i \in 1..4 : - \/ cigars[i] = "blend" /\ drinks[i + 1] = "water" - \/ drinks[i] = "water" /\ cigars[i + 1] = "blend" + \/ cigars[i] = "blend_OF_CIGAR" /\ drinks[i + 1] = "water_OF_DRINK" + \/ drinks[i] = "water_OF_DRINK" /\ cigars[i + 1] = "blend_OF_CIGAR" ------------------------------------------------------------ @@ -116,9 +123,9 @@ BlendSmokerHasWaterDrinkingNeighbor == (************) 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" } + /\ drinks \in { p \in DRINKS : p[3] = "mylk_OF_DRINK" } + /\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian_OF_NATIONALITY" } + /\ colors \in { p \in COLORS : p[2] = "blue_OF_COLOR" } /\ pets \in PETS /\ cigars \in CIGARS @@ -146,4 +153,8 @@ Solution == FindSolution == ~Solution +\* To find the solution with the `^Apalache^' model-checker, run: +\* apalache-mc check --init=Init --inv=FindSolution --length=0 Einstein.tla +\* Then look for the file violation.tla in `^Apalache^' output directory. + ============================================================ From 575c1a035091a6ef54d1dc7674365ae6f58e928c Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Mon, 22 Jan 2024 10:52:02 -0800 Subject: [PATCH 2/3] Avoid _OF_TYPE postfixes by using type Str Signed-off-by: Giuliano Losa --- specifications/EinsteinRiddle/Einstein.tla | 71 +++++++++++----------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index cdf0659d..63ea1a0e 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -41,7 +41,7 @@ House == 1..5 \* would be evaluated faster. However, TLC!Permutations equals a \* set of records whereas Permutation below equals a set of tuples/ \* sequences. Also, Permutation expects Cardinality(S) = 5. -Permutation(S) == +Permutation(S) == { p \in [ House -> S ] : /\ p[2] \in S \ {p[1]} /\ p[3] \in S \ {p[1], p[2]} @@ -53,22 +53,22 @@ Permutation(S) == \* parameterization, the constants are replaced with constant-level \* operators. As a side-effect, TLC evaluates them eagerly at startup, \* and Apalache successfully determines their types. -NATIONALITIES == Permutation({ "brit_OF_NATIONALITY", "swede_OF_NATIONALITY", "dane_OF_NATIONALITY", "norwegian_OF_NATIONALITY", "german_OF_NATIONALITY" }) -DRINKS == Permutation({ "beer_OF_DRINK", "coffee_OF_DRINK", "mylk_OF_DRINK", "tea_OF_DRINK", "water_OF_DRINK" }) -COLORS == Permutation({ "red_OF_COLOR", "white_OF_COLOR", "blue_OF_COLOR", "green_OF_COLOR", "yellow_OF_COLOR" }) -PETS == Permutation({ "bird_OF_PET", "cat_OF_PET", "dog_OF_PET", "fish_OF_PET", "horse_OF_PET" }) -CIGARS == Permutation({ "blend_OF_CIGAR", "bm_OF_CIGAR", "dh_OF_CIGAR", "pm_OF_CIGAR", "prince_OF_CIGAR" }) +NATIONALITIES == Permutation({ "brit", "swede", "dane", "norwegian", "german" }) +DRINKS == Permutation({ "beer", "coffee", "mylk", "tea", "water" }) +COLORS == Permutation({ "red", "white", "blue", "green", "yellow" }) +PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" }) +CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" }) VARIABLES - \* @type: Int -> NATIONALITY; + \* @type: Int -> Str; nationality, \* tuple of nationalities - \* @type: Int -> COLOR; + \* @type: Int -> Str; colors, \* tuple of house colors - \* @type: Int -> PET; + \* @type: Int -> Str; pets, \* tuple of pets - \* @type: Int -> CIGAR; + \* @type: Int -> Str; cigars, \* tuple of cigars - \* @type: Int -> DRINK; + \* @type: Int -> Str; drinks \* tuple of drinks ------------------------------------------------------------ @@ -77,44 +77,44 @@ VARIABLES (* Rules *) (*********) -BritLivesInTheRedHouse == \E i \in 2..5 : nationality[i] = "brit_OF_NATIONALITY" /\ colors[i] = "red_OF_COLOR" +BritLivesInTheRedHouse == \E i \in 2..5 : nationality[i] = "brit" /\ colors[i] = "red" -SwedeKeepsDogs == \E i \in 2..5 : nationality[i] = "swede_OF_NATIONALITY" /\ pets[i] = "dog_OF_PET" +SwedeKeepsDogs == \E i \in 2..5 : nationality[i] = "swede" /\ pets[i] = "dog" -DaneDrinksTea == \E i \in 2..5 : nationality[i] = "dane_OF_NATIONALITY" /\ drinks[i] = "tea_OF_DRINK" +DaneDrinksTea == \E i \in 2..5 : nationality[i] = "dane" /\ drinks[i] = "tea" -GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green_OF_COLOR" /\ colors[i + 1] = "white_OF_COLOR" +GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i + 1] = "white" -GreenOwnerDrinksCoffee == \E i \in 1..5 \ {3} : colors[i] = "green_OF_COLOR" /\ drinks[i] = "coffee_OF_DRINK" +GreenOwnerDrinksCoffee == \E i \in 1..5 \ {3} : colors[i] = "green" /\ drinks[i] = "coffee" -SmokesPallmallRearsBirds == \E i \in 1..5 : cigars[i] = "pm_OF_CIGAR" /\ pets[i] = "bird_OF_PET" +SmokesPallmallRearsBirds == \E i \in 1..5 : cigars[i] = "pm" /\ pets[i] = "bird" -YellowOwnerSmokesDunhill == \E i \in 1..5 : colors[i] = "yellow_OF_COLOR" /\ cigars[i] = "dh_OF_CIGAR" +YellowOwnerSmokesDunhill == \E i \in 1..5 : colors[i] = "yellow" /\ cigars[i] = "dh" -CenterDrinksMylk == drinks[3] = "mylk_OF_DRINK" +CenterDrinksMylk == drinks[3] = "mylk" -NorwegianFirstHouse == nationality[1] = "norwegian_OF_NATIONALITY" +NorwegianFirstHouse == nationality[1] = "norwegian" BlendSmokerLivesNextToCatOwner == \E i \in 1..4 : - \/ cigars[i] = "blend_OF_CIGAR" /\ pets[i + 1] = "cat_OF_PET" - \/ pets[i] = "cat_OF_PET" /\ cigars[i + 1] = "blend_OF_CIGAR" + \/ cigars[i] = "blend" /\ pets[i + 1] = "cat" + \/ pets[i] = "cat" /\ cigars[i + 1] = "blend" HorseKeeperLivesNextToDunhillSmoker == \E i \in 1..4 : - \/ cigars[i] = "dh_OF_CIGAR" /\ pets[i + 1] = "horse_OF_PET" - \/ pets[i] = "horse_OF_PET" /\ cigars[i + 1] = "dh_OF_CIGAR" + \/ cigars[i] = "dh" /\ pets[i + 1] = "horse" + \/ pets[i] = "horse" /\ cigars[i + 1] = "dh" -BluemasterSmokerDrinksBeer == \E i \in 1..5 : cigars[i] = "bm_OF_CIGAR" /\ drinks[i] = "beer_OF_DRINK" +BluemasterSmokerDrinksBeer == \E i \in 1..5 : cigars[i] = "bm" /\ drinks[i] = "beer" -GermanSmokesPrince == \E i \in 2..5 : nationality[i] = "german_OF_NATIONALITY" /\ cigars[i] = "prince_OF_CIGAR" +GermanSmokesPrince == \E i \in 2..5 : nationality[i] = "german" /\ cigars[i] = "prince" -NorwegianLivesNextToBlueHouse == colors[2] = "blue_OF_COLOR" \* since the norwegian_OF_NATIONALITY lives in the first house +NorwegianLivesNextToBlueHouse == colors[2] = "blue" \* since the norwegian lives in the first house BlendSmokerHasWaterDrinkingNeighbor == \E i \in 1..4 : - \/ cigars[i] = "blend_OF_CIGAR" /\ drinks[i + 1] = "water_OF_DRINK" - \/ drinks[i] = "water_OF_DRINK" /\ cigars[i + 1] = "blend_OF_CIGAR" + \/ cigars[i] = "blend" /\ drinks[i + 1] = "water" + \/ drinks[i] = "water" /\ cigars[i + 1] = "blend" ------------------------------------------------------------ @@ -123,16 +123,19 @@ BlendSmokerHasWaterDrinkingNeighbor == (************) Init == - /\ drinks \in { p \in DRINKS : p[3] = "mylk_OF_DRINK" } - /\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian_OF_NATIONALITY" } - /\ colors \in { p \in COLORS : p[2] = "blue_OF_COLOR" } + /\ 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 +\* @type: Seq(Int -> Str); +vars == <> + Next == - UNCHANGED <> + UNCHANGED vars -Spec == Init /\ [][Next]_<> +Spec == Init /\ [][Next]_vars Solution == /\ BritLivesInTheRedHouse From 2f14b4dc0a2da0382bbe88ae837ea46c6fa57910 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sat, 27 Jan 2024 08:46:57 -0800 Subject: [PATCH 3/3] improve comments Signed-off-by: Giuliano Losa --- specifications/EinsteinRiddle/Einstein.tla | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index 63ea1a0e..e9ff0f68 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -129,6 +129,8 @@ Init == /\ pets \in PETS /\ cigars \in CIGARS +\* Apalache cannot infer the type of `vars' because it could be a sequence or a tuple. +\* So we explicitely tell Apalache that it is a sequence by adding the following annotation: \* @type: Seq(Int -> Str); vars == <> @@ -157,7 +159,7 @@ Solution == FindSolution == ~Solution \* To find the solution with the `^Apalache^' model-checker, run: -\* apalache-mc check --init=Init --inv=FindSolution --length=0 Einstein.tla -\* Then look for the file violation.tla in `^Apalache^' output directory. +\* `^apalache-mc check --init=Init --inv=FindSolution --length=0 --run-dir=./outout Einstein.tla^' +\* You will then find the solution in `^./output/violation.tla^'. ============================================================