Re: [tlaplus] TLA+ Specification for Einsteins Riddle

[Christian Barthel <bch@xxxxxxxxx>]

Hi Isaac,

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
> counterexample.

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.