Re: [tlaplus] TLA+ Specification for Einsteins Riddle

[Christian Barthel <bch@xxxxxxxxx>]

Hillel,
Markus,

thanks for your answers and giving me some advice (and good tips)
where to look next.  I am going to try this now and improve my
specification. 

Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> writes:

> On 03.03.21 13:56, Hillel Wayne wrote:
[..]
>> That's the report number. Progress(8) means it's the 8th time it's
>> reporting statistics.
>
>
> TLC reports statistics, i.e., Progress every minute. At the beginning
> of model-checking, the number N in "Progress(N)" indeed correlates
> with TLC's reporting. However, N actually is what the Toolbox reports
> as "diameter", which is the length of the longest behavior found so
> far (remember, breadth-first search). Usually, after a while, the
> diameter stagnates for extended periods before TLC starts to generate
> the next longer behavior.

OK thanks for the insights!  I guess, that also explains why the
number doesn't start with "1".

>> CONSTANTS
>>   univ_colors = {"red", "white", "blue", "green", "yellow", "none" }
>>   univ_pets = {"bird", "cat", "dog", "fish", "horse", "none"}
>>   univ_cigars = {"blend", "bm", "dunhill", "pm", "prince", "none"}
>>   univ_drinks = {"beer", "coffee", "milk", "tea", "water", "none"}
>>   univ_nations = {"brit", "swede", "dane", "norwegian", "german", "none"}
>
>
> Try to reduce the size of these sets to keep the state-space explosion
> at bay, assuming that the small model/scope hypothesis applies to this 
> riddle as well. In other words, you will likely be able to learn
> everything useful about your spec and its properties even without
> those beer-drinking Germans. ;-)

I guess that Hillel pointed me in the same direction with using
CONSTRAINT in the model configuration.  This will be interesting
how this works out (I read about that option and forgot about it
because I was doing fine with INVARIANT and CONSTANTS options in
the TLC model configurations so far).

-- 
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/87tupqoy3w.fsf%40x230a3.onfire.org.