[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ Specification for Einsteins Riddle
- From: Christian Barthel <bch@xxxxxxxxx>
- Date: Wed, 10 Mar 2021 20:23:40 +0100
- Ironport-hdrordr: A9a23:hTnC7aqnXB9rYFG12iXb/ewaV5ujLNV00zAX/kB9WHVpW+SivYSHgOkb2RjoiDwYRXEnnpS6NLOdRG7HnKQYkPEsFJ+Ydk3DtHGzJI9vqbHjzTrpBjHk+odmuNYYT4FXM/e1N1RziK/BinjfL/8Lxt6b/Ke0wdrP1nsFd3AcV4hMzSdcTjyaHEp/WRVcCfMCe6a0y8Jbq1ObCAQqR+uhAH1tZZm+m/Tqk9bcbQcCF1ob7mC1/EKVwZv7CQXd9gwVUjNRzd4ZgC34uin4/Ljmkv2/03bnpi3uxrFXgsak6vYrPr3DtuExKi/wzj+vfpkJYczAgBkRoPuzrGosisXGuR06P89+gkmhOl2dhTvI903e3C0163nkoGXo9UfLhcT4QTI8BY5FhZhFGyGppHYImN1nyqpE0ya4mvNsfGD9tR3n69LFWh1snEbcmwtvrccpg3ZSUZQTZdZqxOR1jScla+Z8IAvA5IoqEPZjAYXn3dk+SyLhU1njsmZi29CqVHgody32MHQqgcCN1igToXYR9TpU+OUkknAM+IlVcfh5zt7ZOadlnqwmdL5pUYtBAo46MLSKI1DWTQmJGGyfJkmPLtBzB1v977X67LIJ5e2wdPUzvf4PsaWEflcdkWIpYUrhBYm1wZVX/nn2IFmVbHDCzMdR4pQ8l5/dYP7QMSOFQE0ziMfImZsiK/yedfC0NpdbR9H5K3f2XaZFtjeOG6V6GD0xVssav9p+YVaSu4bwLJHwvOCzSoexGJPdVRA+Wm3+BXMHGBDuOcRN6V2qUHfkgB7XH0jgYFD74IgYKtmRw8EjjK4XNoNNtQARzW604cyGMlR5w+cLVXo7Gajgjau0vy2X0A/znhNUEysYNUpe7LX+X34in35pQiTJWIdGgcyWfSR53XeMJBNzC+PQVCBFoUhvkJjHbqC49GQZEtqidk2eh3V7ngPCc74s3pGioeH4Z9cWDpM6VLdrGR/WEgFu8Dwa4Ft+VA==
- References: <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org> <CAM3xQxH0xATFyk6Rg+kdxr9J6=1e3Sf_NVXyv4hjdpzqLjxTOA@mail.gmail.com>
- User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (berkeley-unix)
thanks for sharing your solution as well.
Isaac DeFrain <isaacdefrain@xxxxxxxxx> writes:
> Hey Christian,
> The nice thing about the brute force approach is that you don't even have
> to define any actions (I used *Next == FALSE* to disable Next actions,
> there is probably a better way). The most natural way for me to think about
> the problem was to simply define the *FindSolution *predicate, enumerate
> all possible (initial) states, and wait for TLC to give the expected
Yes, that looks like a very reasonable choice as well. I think I
already was in the mindset where I thought "I need actions".
Anyway, I think it is good to see different approaches and how to
describe them with TLA+.
> I made all simplifications I could think of, including making each of the
> variables a 5-tuple and treating the first entry of each tuple as the
> attributes of the first house, second entries for the second house, etc.
> TLC ultimately enumerated 134217728 initial states (maybe you can do
> better, but this pretty good IMO) and took 53min 34s on a server using 4096
> workers on 64 cores with 27305MB heap and 64MB offheap memory (Linux
> 5.3.0-26-generic amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet,
> DiskStateQueue). (I'm not sure what MSBDiskFPSet and DiskStateQueue mean,
> maybe someone can say a few words about these?)
I'd be interested in those numbers as well.
Mine took almost 7 hours (as can be seen by the log/trace) on a 2
Core, 4 GB RAM machine virtual machine (Linux/Ubuntu).
>> 4465456701 states generated, 100524188 distinct states found, 55869621
I guess that the inital states are all distinct states. The
ballpark figure seems to be roughly the same as your number on
initial states (134217728).
Christian Barthel <bch@xxxxxxxxx>
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87czw6ols3.fsf%40x230a3.onfire.org.