diff --git a/doc/examples/client_server_example.md b/doc/examples/client_server_example.md
index c0d20aa..0ae035c 100644
--- a/doc/examples/client_server_example.md
+++ b/doc/examples/client_server_example.md
@@ -109,16 +109,16 @@ This produces the following rather uninformative display:
Let's ask IVy to check our invariant. We select the `Check induction`
operation, like this:
-
+
Here's what IVy says:
-
+
It is telling us that our conjectured invariant fails the consecution test.
When we click OK, we see the counter-example to induction:
-
+
On the left-hand side of the display, we see a transition of the
program from a state labeled `0` to a state labeled `1`. The action
@@ -144,7 +144,7 @@ display further information about the state.
Checking the box to view the `semaphore`
relation, we observe the following:
-
+
Notice that the `server` node is now labeled with `semaphore`, meaning
that `semaphore` is true for this node (if it were false, the label would
@@ -153,7 +153,7 @@ the semaphore should be down. We will conjecture that in fact
this 'bad pattern' never occurs. To do this we select the `Gather` option
from the `Conjecture` menu. When then see the following:
-
+
IVy has collect three facts about the displayed state, shown under the
heading 'Constraints'. These facts are a logical representation of the
@@ -168,7 +168,7 @@ generalize it to produce new conjectured invariant about the program
state. Choosing the `Strengthen` option from the `Conjecture` menu, we
see:
-
+
IVy is suggesting to add this fact to the list of conjectured invariants:
@@ -181,13 +181,13 @@ conjectured invariants.
We can now try checking inductiveness again with our new conjecture.
We see the following:
-
+
We now have a proof that our program is safe. Of course, we want to
save that proof so we can use it again later. We select `Save invariant` from
the `File` menu and enter a file name:
-
+
Here is the content of the file:
@@ -217,7 +217,7 @@ There are several ways in which we can get some automated help with
this task. Let's go back to the counterexample in which one client is
connected, but the semaphore is up:
-
+
This pattern actually contains an irrelevant fact. That is, our bad
pattern requires that there are two distinct nodes, `0` and `1`. In
@@ -229,11 +229,11 @@ that is, `semaphore(0)` and `link(0,0)`.
To check this idea, we remove the irrelevant fact from the pattern by clicking on it.
The unwanted fact becomes gray:
-
+
When we strengthen using this pattern, we get this:
-
+
That is, our new conjecture says that no client can be connected to a
server with the semaphore up, but it doesn't depend on the existence
@@ -253,7 +253,7 @@ unwanted facts, we can select `Minimize` from the `Conjecture`
menu. IVy ask for the number of steps to check. Somewhat arbitrarily,
we choose four. This is the result we get:
-
+
IVy has recognized that there is a more general pattern that can be
ruled out if we consider only four steps of execution of the protocol.
@@ -276,7 +276,7 @@ occur within some fixed number of steps.
To see how this goes, suppose we get into this situation:
-
+
Here, we didn't consider the semaphore and we conjectured a bad
pattern in which there is a client connected to a server. Obviously
@@ -284,13 +284,13 @@ pattern in which there is a client connected to a server. Obviously
we can select `Bounded check` from the `Conjecture` menu. Here's what we see when we choose
one step:
-
+
IVy tried the conjecture that node client is connected to any server
for one step and found it false. If we click `View`, here is what we see:
-
+
IVy has created a new tab in the interface with a trace consisting of
two steps. The arrow represents a transition from state `0` to state
@@ -298,7 +298,7 @@ two steps. The arrow represents a transition from state `0` to state
Clicking on state `0`, and checking the `link` and `semaphore` relations,
we see the following:
-
+
That is, in the initial state there are two clients and one server, the
semaphore of the server is up and there are no links.
@@ -306,7 +306,7 @@ semaphore of the server is up and there are no links.
Now, clicking on state `1`, we see our proposed bad pattern. This
means that the pattern can actually occur.
-
+
# Debugging
@@ -315,25 +315,25 @@ To see details of the execution path, we left-click on the action
actions. In this case, we see that the environment has decided to call
the exported action `connect`:
-
+
Applying `Decompose` to this action we see:
-
+
This shows us that `connect` is made up of a sequence of three smaller
actions. If we left-click on one of these and choose `Show source`,
the corresponding source line is display. By single-clicking on a state,
we can display it graphically:
-
+
This is state 2, which is after the link is created, but before the
semaphore is lowered. The two identifiers `fml:x` and `fml:y` represent
the formal parameters of action `connect`. We can see which client is `x`
at this point in the code by checking the `+` box for `fml:x`:
-
+
As we decompose actions, we build up a sequence of tabs,
corresponding to something like a stack trace of the program's
@@ -351,7 +351,7 @@ strengthen the invariant with a conjecture that isn't true. If this happens,
or if we regret a conjecture for any other reason, we can remove it using
the `Weaken` operation in the `Invariant` menu:
-
+
This dialog can be resized to see long formulas.
diff --git a/doc/examples/leader.md b/doc/examples/leader.md
index 35ee6a1..84b5adf 100644
--- a/doc/examples/leader.md
+++ b/doc/examples/leader.md
@@ -341,11 +341,11 @@ method](client_server_example.html). We start IVy using this command:
We start, as usual, with `Invariant|Check induction`. Ivy tells us the
the safety check failed, meaning that an assert fails in some action:
-
+
When we click OK, this is what we see:
-
+
On the left, we see a failing transition starting in state `0`, using
one of our two exported actions, `app.async` and `trans.recv`. To
@@ -364,7 +364,7 @@ could start selecting relations to see more information, but let's
instead choose the command `Invariant|Diagram` to see what information
IVy thinks might be relevant to the failure. Here's what we see:
-
+
The arrow from id 0 to id 1 is depicting the relation `X:id.t < Y`.
Because the arrow goes from `X` to `Y`, we interpret the arrow to mean
@@ -379,18 +379,18 @@ to become leader, but it does not have highest id. This situation
clearly has to be ruled out. We do this by selecting the
`Conjecture|Strengthen` command. Here is what IVy says:
-
+
In other words, we conjecture that it never happens that a node N has
id less than a node P, and node N is receiving its own id. Now we choose
`Invariant|Check induction` again, to see if our conjecture is inductive.
Of course, it isn't. Here's what Ivy says:
-
+
And here is the counterexample to induction:
-
+
Here, some externally called action transitions from state `0`
satisfying our conjecture to state `1` *not* satisfying the
@@ -398,7 +398,7 @@ conjecture. IVy is depicting state `0`, with all the relations that
appear in the conjecture. It's not immediately clear what's wrong here,
so let's try `Invariant|Diagram` again to see what IVy thinks:
-
+
Now we can see the problem: node 1's id is arriving at node 0, but it
should never have passed node 2, because node 2 has a higher
@@ -410,14 +410,14 @@ trick up our sleeve. We can use bounded checking to see if some arrows
can be removed. We choose `Conjecture|Minimize` and (somewhat
arbitrarily) select a bound of 4 steps. Here is what IVy says:
-
+
This conjecture says that we never have nodes in the order `N < P < Q`
such that `P` has a smaller id than `Q` and the id of `P` is arriving
at `N`. In the graph, we see that the highlights have been removed
from the two irrelevant arrows:
-
+
IVy discovered that, within 4 steps, we
can rule out the highlighted facts. By ruling out a more general
@@ -429,7 +429,7 @@ Now let's try `Invariant|Check induction` again. IVy is still unhappy
and says that our first conjecture is still not relatively inductive. We
try `Invariant|Diagram` again and here is what we see:
-
+
This looks very similar to the diagram that led to our previous
conjecture. Here, however, it's the id of node 0 that is arriving at
@@ -441,7 +441,7 @@ we'll see a way to avoid this symmetry breaking. For now, though,
we'll just slog through the cases. As before, we minimize this
diagram by bounded checking. Here is the result:
-
+
IVy conjectures that we do not have nodes `N < P < Q` such that `N`
has a lower id than `P` and the id of `N` is arriving at `Q`. This is
@@ -453,17 +453,17 @@ Now we try `Invariant|Check induction` (the reader may be able to
guess what happens next). Again, IVy says that our first conjecture is
not relatively inductive. After `Invariant|Diagram`, we see this:
-
+
This describes the same situation, where the id of node 2 is arriving at node 1.
Once again, we generalize using `Conjecture|Minimize`, giving this conjecture:
-
+
We add this conjecture using `Conjecture|Strengthen`. Now when we
use `Invariant|Check induction`, we get the following:
-
+
That is, we have found a proof for the isolate. We can save this invariant to
a file using the `File|Save invariant` command. We edit these conjectures
@@ -548,7 +548,7 @@ Now, let's try to verify the isolate `iso_app` with this new version of `ring_to
As before, after `Invariant|Check induction` and `Invariant|Diagram`, this is what we see:
-
+
That is, we have a node `1` that is receiving its own id while node
`0` has a greater id. Notice, though, that on the right the relation
@@ -561,7 +561,7 @@ Now, as before, let's add this as a conjecture using
that this conjecture is not relatively inductive. Applying `Invariant|Diagram`,
this is what we see:
-
+
This is similar to what we saw before, but notice the blue arrow from
node `0` to node `1`. This corresponds to a new relation that has
@@ -577,14 +577,14 @@ in this case, there is no effect. No matter -- since this looks like a
reasonable conjecture, we use `Conjecture|Strengthen` to add it to our
invariant. Here is the result:
-
+
This says it is not possible to have nodes `Q,N,P` in ascending order of id,
such that `N` is on the way from `Q` to `P` and the id of `N` is arriving at `Q`.
Now let's try `Invariant|Check induction`:
-
+
Because we haven't broken the rotational symmetry of the ring, there
is just one case needed when we state the key invariant that an id
diff --git a/doc/examples/specification.md b/doc/examples/specification.md
index aca4374..7c78801 100644
--- a/doc/examples/specification.md
+++ b/doc/examples/specification.md
@@ -23,7 +23,7 @@ process observed at different interfaces. That is, TCP is sandwiched
between a higher-level application (say, a web browser and web server)
and the lower-level datagram protocol (typically the IP protocol) as shown below:
-
+
The TCP service specification describes the events we observe at the
interface between the application layer and the transport layer. The
diff --git a/doc/examples/testing/leader.md b/doc/examples/testing/leader.md
index 9ac9f44..7e6837e 100644
--- a/doc/examples/testing/leader.md
+++ b/doc/examples/testing/leader.md
@@ -60,7 +60,7 @@ that only the node with the maximum `id` value can be elected.
Our protocol consists of a collection of concurrent process layered on
top of two services: a network service and a timer service:
-
+
Let's consider now the two intermediate interfaces. The specification
for the network service is quite simple and comes from IVy's standard
@@ -179,7 +179,7 @@ would increase the amount of time needed to see an election event.
We're going to divide the system into three isolates, one for each of
its major components. Here is what the three isolates will look like:
-
+
Here are the isolate definitions:
diff --git a/doc/examples/testing/specification.md b/doc/examples/testing/specification.md
index 40fc5eb..513bfea 100644
--- a/doc/examples/testing/specification.md
+++ b/doc/examples/testing/specification.md
@@ -28,7 +28,7 @@ process observed at different interfaces. That is, TCP is sandwiched
between a higher-level application (say, a web browser and web server)
and the lower-level datagram protocol (typically the IP protocol) as shown below:
-
+
The TCP service specification describes the events we observe at the
interface between the application layer and the transport layer. The
@@ -425,7 +425,7 @@ will do something:
Here is the call graph of the system we have defined:
-
+
Now what we want to do is to generate testers for the left and right
players in isolation. That is, we want the tester for the left player
@@ -445,7 +445,7 @@ separate verification problems called "isolates".
Here's the call graph for the left player isolate `iso_l`:
-
+
We can see what the first isolate looks like textually as follows (leaving a few
things out):