[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ Specification for Einsteins Riddle



On 03.03.21 13:56, Hillel Wayne wrote:
Q2: While running the TLC model checker, I got output like this
(line wrapped for readability):

--8<---------------cut here---------------start------------->8---
  ...
Progress(7) at 2021-02-25 15:25:21: 53,778,336 states generated
    (27,490,150 s/min),
    4,258,962 distinct states found (1,912,070 ds/min),
    3,721,176 states left on queue.
Progress(8) at 2021-02-25 15:26:21: 77,487,511 states generated
   (23,709,175 s/min),
    5,818,666 distinct states found (1,559,704 ds/min),
    5,043,790 states left on
  queue.
   ...
--8<---------------cut here---------------end--------------->8---

What does the number in curved brackets mean i.e. 7 in
Progress(7) or 8 in Progress(8)?
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.


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. ;-)

M.

--
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/48c1ad5e-a690-fd46-cde9-1d4724904526%40lemmster.de.