Getting all possible unique traces

[Vladislav Shpilevoy]

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.

Here is my model:

------------------------------ MODULE SimpleQueue ------------------------------

EXTENDS TLC, Integers, Sequences

--------------------------------------------------------------------------------

\*

\* Definitions.

\*

\* How many messages to pass through the pipe in total.

CONSTANT Count

\* How many messages can be in the pipe at once.

CONSTANT Lim

\* Sequence of messages. Example: <<1, 2, 3, 4, 5>>.

VARIABLES Pipe, LastReceived, LastSent

vars == <<Pipe, LastReceived, LastSent>>

Init == /\ Pipe = << >>

        /\ LastReceived = 0

        /\ LastSent = 0

PipeInvariant ==

  /\ \A i \in 1..Len(Pipe) - 1: Pipe[i] + 1 = Pipe[i + 1]

  /\ Len(Pipe) =< Lim

  /\ \/ Len(Pipe) = 0

     \/ Pipe[1] = LastReceived + 1

--------------------------------------------------------------------------------

\*

\* Actions.

\*

Send == /\ Len(Pipe) < Lim

        /\ LastSent < Count

        /\ Pipe' = Append(Pipe, LastSent + 1)

        /\ LastSent' = LastSent + 1

        /\ UNCHANGED<<LastReceived>>

Recv == /\ Len(Pipe) > 0

        /\ LastReceived' = Head(Pipe)

        /\ Pipe' = Tail(Pipe)

        /\ UNCHANGED<<LastSent>>

Next == Send \/ Recv

Spec == /\ Init

        /\ [][Next]_vars

        /\ WF_vars(Send)

        /\ WF_vars(Recv)

Property == <>[](LastSent = Count)

================================================================================

And its config:

INVARIANT PipeInvariant

CONSTANTS

Count = 3

Lim = 1

SPECIFICATION Spec

PROPERTY Property

CHECK_DEADLOCK FALSE

[Markus Kuppe]

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.

https://www.youtube.com/watch?v=lj31oIaYSj4&list=PLWLcqZLzY8u8EA8UlsZ5xKMvtUoeGr5R_&index=13

M.