From 1e0a8dd4a766c45c4c69c9e04f35557da84bf627 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 8 May 2025 17:42:52 +0200 Subject: [PATCH 1/2] =?UTF-8?q?Whitespace=20around=20=E2=80=94?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/core/concurrency.rst | 6 +++--- docs/core/constants.rst | 2 +- docs/core/functions.rst | 2 +- docs/core/invariants.rst | 4 ++-- docs/core/nondeterminism.rst | 2 +- docs/core/pluscal.rst | 2 +- docs/core/tla.rst | 2 +- docs/index.rst | 2 +- docs/topics/aux-vars.rst | 2 +- docs/topics/cli.rst | 2 +- 10 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/core/concurrency.rst b/docs/core/concurrency.rst index 52f7384..7b428b7 100644 --- a/docs/core/concurrency.rst +++ b/docs/core/concurrency.rst @@ -118,7 +118,7 @@ Notice how many more states we have. The ``while`` loop is nonatomic, and every :diff: reader_writer/rw_local_1/reader_writer.tla :ss: rw_local_2 -As with global variables, we can have multiple starting local variables— ``i \in 1..3`` is valid. +As with global variables, we can have multiple starting local variables — ``i \in 1..3`` is valid. In practice, local variables aren't often used, as operators in `define ` blocks can't use them. This means you can't easily typecheck them, write helper operators, etc. Generally we use local variables as :ref:`auxiliary ` or "bookkeeping" variables, like loop iterations and model bounding. @@ -197,11 +197,11 @@ In real systems you often have *bounded* queues, which prevent writes when they' :diff: reader_writer/rw_many_3/reader_writer.tla :ss: rw_await -``await`` is a *restriction* on when the label can run. The label can only run— the state "committed", if you will— if *every* ``await`` statement in the label evaluates to true. +``await`` is a *restriction* on when the label can run. The label can only run — the state "committed", if you will — if *every* ``await`` statement in the label evaluates to true. .. note:: `with ` ``x \in set`` also blocks if the set is empty. -.. warning:: ``await`` interacts a little oddly with variable updates— it will be based on the updated value if directly embedded but not if the variable is used via a ``defined`` operator. This is due to the PlusCal->TLA+ translation grammar. As a general precaution, don't use updated variables in ``await`` statements. +.. warning:: ``await`` interacts a little oddly with variable updates — it will be based on the updated value if directly embedded but not if the variable is used via a ``defined`` operator. This is due to the PlusCal->TLA+ translation grammar. As a general precaution, don't use updated variables in ``await`` statements. .. index:: Deadlocks .. _deadlock: diff --git a/docs/core/constants.rst b/docs/core/constants.rst index b6345d8..e199298 100644 --- a/docs/core/constants.rst +++ b/docs/core/constants.rst @@ -113,7 +113,7 @@ We can also assign constants to sets of model values. Put it in as a normal set, S <- [model value] {s1, s2, s3, s4, s5} -Sets of model values will become *extremely* useful when we start modeling :doc:`concurrency `, but there's still one cool trick we can do with them right now. If you run the model with that value of ``S``, you will get 4,375 states total— the same as if you did ``S <- 1..5``. But notice this other option below the "set of model values" bar: +Sets of model values will become *extremely* useful when we start modeling :doc:`concurrency `, but there's still one cool trick we can do with them right now. If you run the model with that value of ``S``, you will get 4,375 states total — the same as if you did ``S <- 1..5``. But notice this other option below the "set of model values" bar: .. image:: img/symmetry_set.png diff --git a/docs/core/functions.rst b/docs/core/functions.rst index 091f1d9..f0ba247 100644 --- a/docs/core/functions.rst +++ b/docs/core/functions.rst @@ -194,7 +194,7 @@ We can check that these are equivalent by writing a quantifier check: Using Functions ----------------- -Why functions over operators? We rarely use functions for computations— operators are far superior for that. Functions are important as *values*. We can assign them to variables and manipulate them like any other value. +Why functions over operators? We rarely use functions for computations - operators are far superior for that. Functions are important as *values*. We can assign them to variables and manipulate them like any other value. In a spec I once wrote, I had to assign tasks to CPUs. Some tasks needed to be assigned to many CPUs, but each CPU should only have one task. In that spec, the best solution was to store assignments as functions, where each task mapped to a set of CPUs. diff --git a/docs/core/invariants.rst b/docs/core/invariants.rst index f9a0a6a..4c77f18 100644 --- a/docs/core/invariants.rst +++ b/docs/core/invariants.rst @@ -44,7 +44,7 @@ This operator needs to know about the ``is_unique`` variable, so we have to put :diff: duplicates/3/duplicates.tla :ss: duplicates_many_inputs -To check this, we add it as an :doc:`invariant `. TLC will check it at every possible state. All of the invariants passing looks the same as us not having any invariants— TLC will only do something interesting if the invariant fails. Here's what happens if we instead change the invariant to ``is_unique = TRUE``: +To check this, we add it as an :doc:`invariant `. TLC will check it at every possible state. All of the invariants passing looks the same as us not having any invariants — TLC will only do something interesting if the invariant fails. Here's what happens if we instead change the invariant to ``is_unique = TRUE``: .. figure:: img/invariants_fail.png @@ -95,7 +95,7 @@ We can simplify this by just using ``=``. Now the next two steps: 1. Actually implement ``IsUnique(s)``. -2. Currently, ``is_unique`` starts out true and flips to false if we find a duplicate. If the sequence *isn't* unique, then the invariant would fail as soon as we start— ``is_unique`` is true but ``IsUnique(seq)`` will be false. So we only want to check the "invariant" after the algorithm finishes running. +2. Currently, ``is_unique`` starts out true and flips to false if we find a duplicate. If the sequence *isn't* unique, then the invariant would fail as soon as we start — ``is_unique`` is true but ``IsUnique(seq)`` will be false. So we only want to check the "invariant" after the algorithm finishes running. Writing ``IsUnique(s)`` *properly* requires learning some things. Writing it *improperly* is possible though, so let's start with that, then cover (2), the double back to doing ``IsUnique`` properly. diff --git a/docs/core/nondeterminism.rst b/docs/core/nondeterminism.rst index 9d6f636..d372161 100644 --- a/docs/core/nondeterminism.rst +++ b/docs/core/nondeterminism.rst @@ -173,7 +173,7 @@ One way we use nondeterminism is to simulate user input. Our system has to handl .. spec:: calculator/1/calculator.tla :name: calculator_1 -.. todo:: This example might work better if I break the ``while`` into a separate step. But that's for after v2 is up and I'm polishing— might be totally unnecessary. +.. todo:: This example might work better if I break the ``while`` into a separate step. But that's for after v2 is up and I'm polishing — might be totally unnecessary. Two things to notice: diff --git a/docs/core/pluscal.rst b/docs/core/pluscal.rst index 6736e46..c066ce8 100644 --- a/docs/core/pluscal.rst +++ b/docs/core/pluscal.rst @@ -168,7 +168,7 @@ if end if; -You *can* put labels inside an if block. This is useful if your logic branches, and some of the branches represent more complicated behavior. You don't need to balance the labels in an if block— some conditionals can have labels and others do not. **However, if any branch has a label, you must follow the entire block with a label**. To see why, consider the following: +You *can* put labels inside an if block. This is useful if your logic branches, and some of the branches represent more complicated behavior. You don't need to balance the labels in an if block — some conditionals can have labels and others do not. **However, if any branch has a label, you must follow the entire block with a label**. To see why, consider the following: :: diff --git a/docs/core/tla.rst b/docs/core/tla.rst index 987bf6a..35e2014 100644 --- a/docs/core/tla.rst +++ b/docs/core/tla.rst @@ -298,7 +298,7 @@ Looking it at piece-by-piece: /\ pc' = [pc EXCEPT ![self] = "Done"] -The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of it, it sets ``pc[self]`` to "Done". That's how we emulate sequentiality in TLA+ algorithm— it's like going from the "IncCounter" label to the "Done" label. Each label corresponds to exactly one action, and vice versa. +The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of it, it sets ``pc[self]`` to "Done". That's how we emulate sequentiality in TLA+ algorithm — it's like going from the "IncCounter" label to the "Done" label. Each label corresponds to exactly one action, and vice versa. .. _trans: .. tip:: diff --git a/docs/index.rst b/docs/index.rst index 15a1a39..4d53420 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -20,7 +20,7 @@ Learn TLA+ ==================================== -Most software flaws come from one of two places. A code bug is when the code doesn't match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we're just taught to "think about it really hard". +Most software flaws come from one of two places. A code bug is when the code doesn't match our design — for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we're just taught to "think about it really hard". TLA+ is a "formal specification language", a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and CrowdStrike. TLA+ doesn't replace our engineering skill but *augments* it. With TLA+ we can design systems faster and more confidently. Check out the `chapter_overview` to see an example of this in practice. diff --git a/docs/topics/aux-vars.rst b/docs/topics/aux-vars.rst index 3cce42b..30873cf 100644 --- a/docs/topics/aux-vars.rst +++ b/docs/topics/aux-vars.rst @@ -66,7 +66,7 @@ It can be hard to tell in the error trace which branch was taken; you have to in or \* ... -Then you can see which path you took in ``pc``. But doing this adds a lot of extra concurrency to your spec— at best exploding the state space, at worst changing the spec semantics! +Then you can see which path you took in ``pc``. But doing this adds a lot of extra concurrency to your spec — at best exploding the state space, at worst changing the spec semantics! What we want is to enrich the error traces without changing the spec semantics. This is a great place for an aux var. diff --git a/docs/topics/cli.rst b/docs/topics/cli.rst index ff3cd26..da8d0ac 100644 --- a/docs/topics/cli.rst +++ b/docs/topics/cli.rst @@ -52,7 +52,7 @@ Config Format The model checking config language is a special DSL for using TLC from the command line. It's what the toolbox abstracts away on the backend. -All config files need a ``SPECIFICATION {spec}`` line, where ``Spec`` is whatever action encompasses your initial and next states. By convention, this should be called ``Spec``, but this isn't required— useful if you want different configs to test different variations of your system. +All config files need a ``SPECIFICATION {spec}`` line, where ``Spec`` is whatever action encompasses your initial and next states. By convention, this should be called ``Spec``, but this isn't required — useful if you want different configs to test different variations of your system. Invariants you want to check must be prefixed with ``INVARIANT``, temporal properties with ``PROPERTY``. Both can have commas, eg ``INVARIANT TypeInvariant, IsSafe`` is a valid line. Unlike in the toolbox, you **cannot** make expressions invariants— they must be named operators. From 96075e09b216a8bea627316cf874db18cf995cd0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 16 Sep 2025 09:53:20 +0200 Subject: [PATCH 2/2] Revised documentation and fixed typos and minor issues --- docs/core/concurrency.rst | 6 +++--- docs/core/constants.rst | 2 +- docs/core/functions.rst | 8 ++++---- docs/core/invariants.rst | 2 +- docs/core/operators.rst | 4 ++-- docs/core/pluscal.rst | 4 ++-- docs/core/temporal-logic.rst | 4 ++-- docs/core/tla.rst | 2 +- docs/topics/cli.rst | 2 +- docs/topics/message-queues.rst | 4 ++-- docs/topics/toolbox.rst | 2 +- 11 files changed, 20 insertions(+), 20 deletions(-) diff --git a/docs/core/concurrency.rst b/docs/core/concurrency.rst index 7b428b7..e55f04c 100644 --- a/docs/core/concurrency.rst +++ b/docs/core/concurrency.rst @@ -35,7 +35,7 @@ Now let's add another process that reads from the queue. Different processes cannot share label names. -The writer has a single action, ``Write``, and the reader has a single action, ``Read``. We haven't specified which should happen first, so the two can happen in any order. Either we (1) write to the queue and then read from it, or (2) read from the queue and then write to it. +The writer has a single action, ``AddToQueue``, and the reader has a single action, ``ReadFromQueue``. We haven't specified which should happen first, so the two can happen in any order. Either we (1) write to the queue and then read from it, or (2) read from the queue and then write to it. Behavior (2) doesn't make any sense: how can we read from the queue if there's nothing already in it? And if you try to run the spec, TLC will raise this as an error. @@ -155,7 +155,7 @@ This is equivalent to putting the label in a ``while TRUE`` loop. .. rubric:: ``self`` -In process sets we have a special keyword ``self``, which retrieves the "value" of the process. So for the writers, the values of the process would be ``1`` and ``2``. If we tell the writers to put ``self`` on instead of ``1``, we'd expect the end total to be 6. +In process sets we have a special keyword ``self``, which retrieves the "value" of the process. So for the writers, the values of the process would be ``1``, ``2`` and ``3``. If we tell the writers to put ``self`` on instead of ``1``, we'd expect the end total to be 6. .. spec:: reader_writer/rw_many_3/reader_writer.tla :diff: reader_writer/rw_many_2/reader_writer.tla @@ -249,7 +249,7 @@ The thread-local variable is an "internal implementation detail", and I don't th Before we continue, I want to recommend a good exercise to improve your modeling skills. You know, based on how I'm presenting this example, that this will fail. But *how* will it fail? Before you run the model checker, try to figure out what error it will give you and why. See if you can guess the number of steps it will take, and what order the processes will run. -This is will help you get better with TLA+, but it does something else, too. As you write more specifications, you'll start to see errors *without* running the model checker. One reason why concurrency is so unintuitive is we normally don't get rapid feedback on the mistakes we make. If you had a race condition to your code, it could be days or weeks before bites you, and then it takes even longer to fully understand it. Whereas in a specification, the model checker shows you immediately. This trains your intuition for race conditions much more quickly than normal. +This is will help you get better with TLA+, but it does something else, too. As you write more specifications, you'll start to see errors *without* running the model checker. One reason why concurrency is so unintuitive is we normally don't get rapid feedback on the mistakes we make. If you had a race condition to your code, it could be days or weeks before it bites you, and then it takes even longer to fully understand it. Whereas in a specification, the model checker shows you immediately. This trains your intuition for race conditions much more quickly than normal. ... diff --git a/docs/core/constants.rst b/docs/core/constants.rst index e199298..72d75f8 100644 --- a/docs/core/constants.rst +++ b/docs/core/constants.rst @@ -67,7 +67,7 @@ If you have a spec with constants, you should put constraining assumptions on th Model Values ---------------- -That takes care of ordinary assignments, what about "model values"? Model values are a special type of value in TLA+. A model value has no operations and can only be tested for equality, and is only equal to itself. IE +That takes care of ordinary assignments, what about "model values"? Model values are a special type of value in TLA+. A model value has no operations and can only be tested for equality, and is only equal to itself. .. code-block:: diff --git a/docs/core/functions.rst b/docs/core/functions.rst index f0ba247..a2a9d25 100644 --- a/docs/core/functions.rst +++ b/docs/core/functions.rst @@ -102,7 +102,7 @@ The set we're mapping from, ``S``, is the **domain** of the function, and can be 1. A sequence is just a function where the domain is ``1..n``. 2. A struct is just a function where the domain is a set of strings. -But functions are a more general than that, and can map *any* set of values. For example, we can have pairs of numbers in the domain of the function. +But functions are more general than that, and can map *any* set of values. For example, we can have pairs of numbers in the domain of the function. :: @@ -271,11 +271,11 @@ Some more examples of function sets: Encountered "\|->" in line X, column Y - In a function set, then you probably wrote ``[S |-> T]`` instead of ``[S -> T]``. Similarly, if you get + in a function set, then you probably wrote ``[S |-> T]`` instead of ``[S -> T]``. Similarly, if you get Encountered "->" in line X, column Y - In a function, then you probably wrote ``[x \in S -> T]`` instead of ``[x \in S |-> T]``. Don't worry, everybody gets the two mixed up at some point. + in a function, then you probably wrote ``[x \in S -> T]`` instead of ``[x \in S |-> T]``. Don't worry, everybody gets the two mixed up at some point. .. rubric:: Example: Sorting @@ -320,7 +320,7 @@ To figure out if two sequences have the same number of each element, let's defin CountMatching(f, val) == Cardinality({key \in DOMAIN f: f[key] = val}) -Then we just need to test to check this over every element in the sequence: +Then we just need to check this over every element in the sequence: :: diff --git a/docs/core/invariants.rst b/docs/core/invariants.rst index 4c77f18..0ba45a6 100644 --- a/docs/core/invariants.rst +++ b/docs/core/invariants.rst @@ -97,7 +97,7 @@ Now the next two steps: 1. Actually implement ``IsUnique(s)``. 2. Currently, ``is_unique`` starts out true and flips to false if we find a duplicate. If the sequence *isn't* unique, then the invariant would fail as soon as we start — ``is_unique`` is true but ``IsUnique(seq)`` will be false. So we only want to check the "invariant" after the algorithm finishes running. -Writing ``IsUnique(s)`` *properly* requires learning some things. Writing it *improperly* is possible though, so let's start with that, then cover (2), the double back to doing ``IsUnique`` properly. +Writing ``IsUnique(s)`` *properly* requires learning some things. Writing it *improperly* is possible though, so let's start with that, then cover (2), then double back to doing ``IsUnique`` properly. Here's the improper solution for ``IsUnique``: diff --git a/docs/core/operators.rst b/docs/core/operators.rst index 0ef468c..830f6e2 100644 --- a/docs/core/operators.rst +++ b/docs/core/operators.rst @@ -123,7 +123,7 @@ A quick mnemonic: ``~`` is a little flippy thing, so it's "not". ``/\`` looks li .. index:: => (implies) .. _=>: -There is one more boolean operator of note: ``=>``, or "implication". ``A => B`` means "A is at least as true as B". ``A => B = FALSE`` when false if A is true and B is false, otherwise it's true. B is true or A is false (or both). You don't see this very often in programming, as it's pretty useless for control flow. But it's *extremely* important for any kind of specification work. We'll go into more detail about it `later >`. [#iff]_ +There is one more boolean operator of note: ``=>``, or "implication". ``A => B`` means "A is at least as true as B". ``A => B = FALSE`` if A is true and B is false, otherwise it's true. You don't see this very often in programming, as it's pretty useless for control flow. But it's *extremely* important for any kind of specification work. We'll go into more detail about it `later >`. [#iff]_ .. exercise:: Contrapositives :name: contrapositive @@ -527,5 +527,5 @@ Summary - We can map and filter sets. -.. [#except-strings] Except strings. Well actually there is a keyword, ``STRING``, but it represents all possible strings, which is an infinitely large set, so... .. [#iff] There's also ``A <=> B`` for "A and B are both true or both false", but it's the same thing as writing ``A = B``. +.. [#except-strings] Except strings. Well actually there is a keyword, ``STRING``, but it represents all possible strings, which is an infinitely large set, so... diff --git a/docs/core/pluscal.rst b/docs/core/pluscal.rst index c066ce8..2124201 100644 --- a/docs/core/pluscal.rst +++ b/docs/core/pluscal.rst @@ -328,7 +328,7 @@ To check both, we can use multiple starting states. TLA+ doesn't just let us ass .. spec:: duplicates/2/duplicates.tla :diff: duplicates/1/duplicates.tla -The model checker will now check *both* ``<<1, 2, 3, 2>>`` and ``<1, 2, 3, 4>>`` as the value of ``seq``. More specifically, does two complete runs, one for each possible value. If either complete run, or :dfn:`behavior`, would lead to an error, TLC will let us know. +The model checker will now check *both* ``<<1, 2, 3, 2>>`` and ``<1, 2, 3, 4>>`` as the value of ``seq``. More specifically, it does two complete runs, one for each possible value. If either complete run, or :dfn:`behavior`, would lead to an error, TLC will let us know. .. figure:: graphs/duplicates_2.gv.png @@ -372,7 +372,7 @@ Summary - Specifications have variables. These can either be a fixed value (using ``=``) or an element in a set (using ``\in``). Any TLC value can be a variable. - - If an element of a set, then TLC will test the model on *every possible starting state*. + - If a variable is an element of a set, then TLC will test the model on *every possible starting state*. - PlusCal is a language that makes writing specifications easier. - In the PlusCal algorithm body, variables are updated with ``:=``. ``=`` is comparison. diff --git a/docs/core/temporal-logic.rst b/docs/core/temporal-logic.rst index f515d74..62e544a 100644 --- a/docs/core/temporal-logic.rst +++ b/docs/core/temporal-logic.rst @@ -66,7 +66,7 @@ At the beginning of the behavior, we pick one online server. That server is then .. figure:: graphs/liveness.gv.png - The behavior sequence 1-2-3 breaks violates our safety property, even though no state is individually a "bad state". + The behavior sequence 1-2-3 violates our safety property, even though no state is individually a "bad state". In summary, adding ``[]`` to the language lets us represent all invariants, and a host of other properties too. @@ -105,7 +105,7 @@ Not so fast! There's a *third* thing the orchestrator can do: it can crash. In T .. note:: Why haven't we see this before? Because up until now we've only had invariants, which are only violated by "bad states": particular configurations of variables that break the invariants. Stutter steps don't change the values of anything, so a stutter step can never break an invariant. Here's the first time it can break things by *preventing* us from reaching a good state. -TLA+ allows infinite stutter steps because it is fundamentally a worst-case scenario language. IN reality, systems always crash. If we do not *explicitly say* a system can't crash, TLA+ will assume the system can crash at the worst possible time. +TLA+ allows infinite stutter steps because it is fundamentally a worst-case scenario language. In reality, systems always crash. If we do not *explicitly say* a system can't crash, TLA+ will assume the system can crash at the worst possible time. .. figure:: graphs/stuttering.gv.png diff --git a/docs/core/tla.rst b/docs/core/tla.rst index 35e2014..65b3c6a 100644 --- a/docs/core/tla.rst +++ b/docs/core/tla.rst @@ -303,7 +303,7 @@ The action is only enabled when ``pc[self] = "IncCounter"``, and then as part of .. _trans: .. tip:: - The PlusCal to TLA+ translator is very simple. If we were writing the TLA+ from scatch, we could use a helper action to these transitions look cleaner: + The PlusCal to TLA+ translator is very simple. If we were writing the TLA+ from scatch, we could use a helper action to make these transitions look cleaner: :: diff --git a/docs/topics/cli.rst b/docs/topics/cli.rst index da8d0ac..5d578dd 100644 --- a/docs/topics/cli.rst +++ b/docs/topics/cli.rst @@ -103,7 +103,7 @@ Finally, we have ``ALIAS``. This lets us effectively simulate the `Error Trace E incx |-> x + 1] ===== -If we add ``ALIAS Alias`` to our config file, then the error trace will show the values of x, ``nextx``, and ``incx`` in the error output. +If we add ``ALIAS Alias`` to our config file, then the error trace will show the values of ``x``, ``nextx``, and ``incx`` in the error output. .. note:: The alias *replaces* the standard error output. If you don't include some variables in the alias, then they won't show on the error output either. diff --git a/docs/topics/message-queues.rst b/docs/topics/message-queues.rst index 6f79035..3c31a1c 100644 --- a/docs/topics/message-queues.rst +++ b/docs/topics/message-queues.rst @@ -16,7 +16,7 @@ For now let's consider a perfect FIFO queue, with the operations to push new mes The ``queue`` variable is generally a `sequence ` of message `structs `. To write a new message, we just do ``queue := Append(queue, msg)`` (or ``queue' = ...``). There's an easy way and a hard way to read from a queue. -The *easy* way is to destructively update the queue, so that the newest message is always ``Head(queue)``. This is conceptually simple, and it's easy to do things like check if the queue is empty and write a type invariant (see below). The one downside is that you can't write properties that rely on the queue's history, like "the same message is never enqueued twice". You'd be able to see if duplicates are on the queue at the same time, but not that a duplicae was pushed after the original was popped. At least, not without a `history queue `. +The *easy* way is to destructively update the queue, so that the newest message is always ``Head(queue)``. This is conceptually simple, and it's easy to do things like check if the queue is empty and write a type invariant (see below). The one downside is that you can't write properties that rely on the queue's history, like "the same message is never enqueued twice". You'd be able to see if duplicates are on the queue at the same time, but not that a duplicate was pushed after the original was popped. At least, not without a `history queue `. The *hard* way is to make the queue immutable. You append to the queue like normal, but have an additional ``i`` variable representing the next message to read. To "pop" a message, increment ``i``. This is harder to work with, adds variable bloat, and makes a lot of simple queue checks (like getting the length) more awkward. The one upside is that you preserve the whole queue history, making generalized properties easier. @@ -58,7 +58,7 @@ Use a set of structs. QueueType == Seq(MessageType) MessageType == [id: Nat, from: Writer, data: DataType] -Having an ``id`` field is good practice because it lets you distinguish difference messages with the same content (make sure to have a ``MaxId`` constant!). ``DataType`` can also be a struct. If you want to have multiple distinct kinds of messages, add an additional ``msg`` field and push the details of the data to the ``data`` struct. Then make the ``MessageType`` a union of the possible subtypes: +Having an ``id`` field is good practice because it lets you distinguish different messages with the same content (make sure to have a ``MaxId`` constant!). ``DataType`` can also be a struct. If you want to have multiple distinct kinds of messages, add an additional ``msg`` field and push the details of the data to the ``data`` struct. Then make the ``MessageType`` a union of the possible subtypes: :: diff --git a/docs/topics/toolbox.rst b/docs/topics/toolbox.rst index a68b852..6a1437a 100644 --- a/docs/topics/toolbox.rst +++ b/docs/topics/toolbox.rst @@ -148,7 +148,7 @@ Simulation Mode Simulation mode runs never stop, even if they've exhaustively checked the state space. You have to end them manually. Profiling - Two types of profiling are available. "Action Enablement" records how often each partiuclar action was called. This is shown in the model checking results, under statistics. You can use this to check if an action is never enabled, in which case you have a bug in your spec. + Two types of profiling are available. "Action Enablement" records how often each particular action was called. This is shown in the model checking results, under statistics. You can use this to check if an action is never enabled, in which case you have a bug in your spec. "On" does full profiling: how often each operator is called, how often each branch of an expression was used, and how much each operator cost to invoke. You can use this to help with optimizing models.