Find solution to Einstein's riddle with Apalache #113
Conversation
Signed-off-by: Giuliano Losa <giuliano@losa.fr>
|
I tried annotating all variables with the type |
| 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" }) |
There was a problem hiding this comment.
| NATIONALITIES == Permutation({ "brit_OF_NATIONALITY", "swede_OF_NATIONALITY", "dane_OF_NATIONALITY", "norwegian_OF_NATIONALITY", "german_OF_NATIONALITY" }) | |
| BRIT == "brit_OF_NATIONALITY" | |
| SWEDE == "swede_OF_NATIONALITY" | |
| DANE == "dane_OF_NATIONALITY" | |
| NORWEGIAN == "norwegian_OF_NATIONALITY" | |
| GERMAN == "german_OF_NATIONALITY" | |
| NATIONALITIES == Permutation({ BRIT, SWEDE, DANE, NORWEGIAN, GERMAN }) |
Here is my suggestion on how to avoid specifying the type all the time.
|
Yeah, this looks like a lot of literals that are just screaming their types all the time. What you could do is to define a value for each literal and refer to that value. It will increase the size of the spec, but that's the easiest thing that comes to my mind: https://github.com/tlaplus/Examples/pull/113/files#r1461491804 |
| @@ -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) == | |||
There was a problem hiding this comment.
Just by looking at the set of constraints, I think you could define Permutation for the general case too:
Permutation(S) ==
{ p \in [ House -> S ]:
\A h1 \in House:
\A h2 \in House:
h2 /= h1 => p[h2] /= p[h1]
}You could even replace House with S, and it should still work in Apalache, as long as S is a finite set. Of course, this definition would produce really a lot of constraints, something like
@konnov is this a bug I should report? |
Signed-off-by: Giuliano Losa <giuliano@losa.fr>
|
Now using |
Yes, perhaps, something was missing in the annotations. |
|
@lemmy is it acceptable to add type annotations to this spec or should they go into a separate file |
|
The specification might be easier to read if type annotations are placed in a separate file. Alternatively, enhanced IDE tools and pretty-printers could be used to minimize the visual impact of type annotations in comments, thereby preserving readability. |
|
I'm not sure it will not be possible to move the annotation on |
|
I don't think this spec is useful without being checked by Apalache (since TLC just times out on the initial state iirc) so it seems okay to me to modify the spec itself. |
| \* 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. |
There was a problem hiding this comment.
In case it is helpful, you can use the --run-dir flag to put the output (including the violation) in a known location:
apalache-mc --help | grep 'run-dir'
--run-dir : additional directory wherein output files for this run will be written directly, default: none (overrides envvar RUN_DIR)
|
Is this ready to be evaluated & merged or is it a draft pull request? |
Signed-off-by: Giuliano Losa <giuliano@losa.fr>
Yes this is ready to be evaluated and merged. |
Make Einstein work with Apalache Signed-off-by: Giuliano Losa <giuliano@losa.fr>
As you can see it does not look as good as before. The string constants now all have the _OF_TYPE prefix. I'm not sure how to do better. @konnov any suggestion?