[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Getting all possible unique traces
On 10/12/21 11:37 PM, Vladislav Shpilevoy wrote:
Hi! I've just watched the TLA+ video course, and started writing my own
specs. But almost immediately realized I have very view means to ensure
that the spec actually checks the intended behaviour. As Leslie L. said,
you should be afraid when it says the model is correct.
So to see what the model actually checks I used 2 means so far. Both
work, but have drawbacks. (I use command line tool.)
1) `-dump` option. It saves all reachable states into a file. But in my
very simple model (FIFO) with just one possible trace it saves some
states multiple times into the dump file. Which looks like they are
repeating or even revert some variable and 'violate' my invariants. But
when I dump into `-dump dot` file, it looks absolutely correct. No
duplicates, no reverts. However with big number of states I expect it
might look hard to read on a picture, even in .svg.
2) `-simulate` option. I found that it runs infinitely without any
output if not given more args. If you specify `file=...`, it just
generates infinite number of the same files (in my case they are all the
same - the unique trace is just one). However if you limit their max
number, you can't be sure you got all the possible traces before the max
number was reached.
Is there a builtin way to inspect all possible unique traces which I
missed somehow? It would also be very useful for writing tests for
future more complicated models when you start coding them.
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/bf352191-cd61-33ee-91e1-d088ef1d6df3%40lemmster.de.