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