adding leader section to doc, improving diagram

doc/_data/contents.yml

@@ -7,3 +7,4 @@
   - examples/client_server_example
   - examples/specification
   - examples/datatypes
+  - examples/leader

doc/examples/leader.md

@@ -3,9 +3,9 @@ layout: page
 title: Parameterized systems
 ---
 
-Many systems are designed to include an arbitray number of similar or
+Many systems are designed to include an arbitrary number of similar or
 identical components. A good example of such a system is the Internet,
-which is designed to accomdate a large number of hosts, all
+which is designed to accommodate a large number of hosts, all
 communicating using the same set of protocols. Another example would
 be peer-to-peer protocols such as
 [Chord](https://en.wikipedia.org/wiki/Chord_(peer-to-peer)).
@@ -21,11 +21,11 @@ parameter of the same type. Here is an example of an object parameterized on typ
     object foo = {
 
         function bit(S:t) : bool
-	init ~bit(S)
+        init ~bit(S)
 
-	action set_bit(self:t) = {
-	    bit(self) := true
-	}
+        action set_bit(self:t) = {
+            bit(self) := true
+        }
     }
 
 Notice that both the state component `bit` and the action `set_bit`
@@ -44,11 +44,11 @@ write the object `foo` as follows:
     object foo(self:t) = {
 
         individual bit : bool
-	init ~bit
+        init ~bit
 
-	action set_bit = {
-	    bit := true
-	}
+        action set_bit = {
+            bit := true
+        }
     }
 
 Ivy adds the parameter `self` to each state component of `foo`, and
@@ -64,13 +64,13 @@ objects.  For example, you can compile them and run them in separate
 process spaces or on different hosts. In addition, when proving
 assertions that relate to only one process, you can ignore the
 parameter. This can be a good trick for staying within a decidable
-fragment.
+logical fragment.
 
 ### Leader election ring
 
 As an example of a parameterized protocol, lets look at the very
-simple leader election protocol, introduced in [this paper](...) in
-1974.
+simple leader election protocol, introduced in [this paper](http://dl.acm.org/citation.cfm?id=359108) in
+1979.
 
 In this protocol we have a collection of distributed processes
 organized in a ring. Each process can send messages to its right
@@ -81,8 +81,8 @@ has the highest `id` value. This process is elected as the "leader".
 
 This protocol itself is trivially simple. Each process transmits its
 own `id` value. When it receives a value, it retransmits the value,
-but only it is is *greater than* the procees' own `id` value. If a
-process receives its own `id`, this value must have travelled all the
+but only if it is *greater than* the process' own `id` value. If a
+process receives its own `id`, this value must have traveled all the
 way around the ring, so the process knows its `id` is greater than all
 others and it declares itself leader.
 
@@ -90,26 +90,26 @@ We'll start with a service specification for this protocol:
 
     object serv = {
 
-	function pid(X:node.t) : id.t          # map each node to an id
+        function pid(X:node.t) : id.t          # map each node to an id
 
-	axiom pid(X) = pid(Y) -> X=Y           # id's are unique
+        axiom pid(X) = pid(Y) -> X=Y           # id's are unique
 
-	action elect(v:node.t)                 # called when v is elected leader
+        action elect(v:node.t)                 # called when v is elected leader
 
-	object spec = {
-	    before elect {
-		assert pid(v) >= pid(X)        # only the max pid can be elected
-	    }
-	}
+        object spec = {
+            before elect {
+                assert pid(v) >= pid(X)        # only the max pid can be elected
+            }
+        }
     }
 
 This object is parameterized on an abstract datatype `node` that we
 will define shortly. Type `node.t` represents a reference to a process
-in our system. The servicee specification contains a function `pid` that
+in our system. The service specification contains a function `pid` that
 maps each node to its unique `id` value. The fact that the `id` values
 are unique is guaranteed by the axiom.
 
-The specification has one action `elect` which is called whan a given
+The specification has one action `elect` which is called when a given
 node is elected leader. Its specification says that only the node with
 the maximum `id` value can be elected.
 
@@ -118,22 +118,22 @@ protocol itself.  First, we use the explicit parameter style:
 
     object app = {
 
-	action async(me:node.t) = {
-	    call trans.send(node.get_next(me),serv.pid(me))
-	}
+        action async(me:node.t) = {
+            call trans.send(node.get_next(me),serv.pid(me))
+        }
 
-	implement trans.recv(me:node.t,v:id.t) {
-	    if v = serv.pid(me) {       # Found a leader!
-		call serv.elect(me)
-	    }
-	    else if v > serv.pid(me)  { # pass message to next node
-		call trans.send(node.get_next(me),v)
-	    }
-	}
+        implement trans.recv(me:node.t,v:id.t) {
+            if v = serv.pid(me) {       # Found a leader!
+                call serv.elect(me)
+            }
+            else if v > serv.pid(me)  { # pass message to next node
+                call trans.send(node.get_next(me),v)
+            }
+        }
 
     }
 
-Our protocol implementation referes to two interfaces: the `serv`
+Our protocol implementation refers to two interfaces: the `serv`
 interface we just defined, and a network transport interface `trans`
 defined below. It also refers to the abstract datatype `node` that we
 will also define shortly.
@@ -159,18 +159,18 @@ Here is the same object described in the implicit style:
 
     object app(me:node.t) = {
 
-	action async = {
-	    call trans.send(node.get_next(me),serv.pid(me))
-	}
+        action async = {
+            call trans.send(node.get_next(me),serv.pid(me))
+        }
 
-	implement trans.recv(v:id.t) {
-	    if v = serv.pid(me) {       # Found a leader!
-		call serv.elect(me)
-	    }
-	    else if v > serv.pid(me)  { # pass message to next node
-		call trans.send(node.get_next(me),v)
-	    }
-	}
+        implement trans.recv(v:id.t) {
+            if v = serv.pid(me) {       # Found a leader!
+                call serv.elect(me)
+            }
+            else if v > serv.pid(me)  { # pass message to next node
+                call trans.send(node.get_next(me),v)
+            }
+        }
 
     }
 
@@ -178,29 +178,29 @@ Here is the same object described in the implicit style:
 There is not much difference. Notice that we dropped the parameter
 `me` from the action definition. However, references to other objects
 still have to have the explicit parameter `me`. The implicit style
-mainly shows an advantage when the parameterized object has many state
-components.
+mainly shows an advantage when the parameterized object has many references
+to its own actions and state components.
 
 With our protocol implemented, let's look at the interfaces that it's
-built on, starting with the type 'id` values:
+built on, starting with the type of `id` values:
 
     module totally_ordered(t) = {
-	relation (X:t < Y:t)
-	property [transitivity] X:t < Y & Y < Z -> X < Z
-	property [antisymmetry] ~(X:t < Y & Y < X)
-	property [totality] X:t < Y | X = Y | Y < X
+        relation (X:t < Y:t)
+        property [transitivity] X:t < Y & Y < Z -> X < Z
+        property [antisymmetry] ~(X:t < Y & Y < X)
+        property [totality] X:t < Y | X = Y | Y < X
     }
 
     module total_order = {
-	type t
-	instantiate totally_ordered(t)   # t is totally ordered
+        type t
+        instantiate totally_ordered(t)   # t is totally ordered
     }
 
     instance id : total_order
 
 Notice that we defined a couple of modules that we can re-use later.
 The first gives the axioms of a total order. The second defines a
-datatype that obeys these axions. We then define our abstract type
+datatype that obeys these axioms. We then define our abstract type
 `id` to be an instance of `total_order`. Later, we will implement
 `id.t` with fixed-width integers.
 
@@ -208,57 +208,52 @@ Now let's look at the type of node references, which is a bit more
 interesting:
 
     module ring_topology = {
-	type t
+        type t
+        instantiate total_order_axioms(t)   # t is totally ordered
 
-	individual head:t  # ring head
-	individual tail:t  # ring tail
+        action get_next(x:t) returns (y:t)
 
-	instantiate totally_ordered(t)
-	axiom head <= X              # head is minimal
-	axiom X <= tail              # tail is maximal
-
-	action get_next(x:t) returns (y:t)
-
-	object spec = {
-	    after get_next {
-		assert (x = tail & y = head) | (x < y & ~ (x < Z & Z < y))
-	    }
-	}
+        object spec = {
+            after get_next {
+                assert (x < y & ~ (x < Z & Z < y)) | (y <= X & X <= x)
+            }
+        }
     }
 
     instance node : ring_topology
 
-We start by defining a generic module for types that are organized in a
-ring topology.  We use a totally ordered type `t` for the ring
-elements. Type `t` has mimimum and maximum elements called `head` and
-`tail`. The `get_next` action takes an element `x` and returns the
-next element `y` in the ring. The specification says that this is
-either the head, if `x` is the tail, or it is some element that is
-greater than `x` with no elements in between. This is one way of
-specifying a ring topology. Later we will see a different way that can
-make the proofs a little simpler. We can implement either version with
-fixed-width integers.
+We start by defining a generic module for types that are organized in
+a ring topology.  We use a totally ordered type `t` for the ring
+elements. In addition, the `get_next` action takes an element `x` and
+returns the next element `y` in the ring.  The specification says that
+either `y` is the least element larger than `x` or `x` is the maximum
+element and `y` the minimum (that is, we "wrap around" to the
+beginning). In principle, we should also say that the set `t` is finite,
+but we won't actually need this fact to prove safety of our protocol.
+This is one way of specifying a ring topology. Later we will
+see a different way that can make the proofs a little simpler. We can
+implement either version with fixed-width integers.
  
 Finally, we need the service specification for the network transport
 layer. It's quite simple:
 
-object trans = {
+    object trans = {
 
-    relation sent(V:id.t, N:node.t)
-    init ~sent(V, N)
-    
-    action send(dst:node.t, v:id.t)
-    action recv(dst:node.t, v:id.t)
+        relation sent(V:id.t, N:node.t)
+        init ~sent(V, N)
 
-    object spec = {
-	before send {
-	    sent(v,dst) := true
-	}
-	before recv {
-	    assert sent(v,dst)
-	}
+        action send(dst:node.t, v:id.t)
+        action recv(dst:node.t, v:id.t)
+
+        object spec = {
+            before send {
+                sent(v,dst) := true
+            }
+            before recv {
+                assert sent(v,dst)
+            }
+        }
     }
-}
 
 The relation `sent` tells us which values have been sent to which
 nodes.  Initially, nothing has been sent. The interface provides two
@@ -266,22 +261,22 @@ actions `send` and `recv` which are called, respectively, when a value
 is sent or received. The `dst` parameter gives the destination node of
 the message.
 
-The specification says that a values is marked as sent when `send`
+The specification says that a value is marked as sent when `send`
 occurs and a value must be marked sent before it can be received.
 This describes a network service that can duplicate or re-order
 messages, but cannot corrupt messages.
 
 ## Verifying the leader election protocol
 
-Now let's try to verify that our leader election protcol `app` guarantees
+Now let's try to verify that our leader election protocol `app` guarantees
 its service specification `serv` , assuming the specifications of `trans`,
 `node` and `id`. Here is the isolate declaration:
 
-isolate iso_p = app with node,id,trans,serv
+    isolate iso_p = app with node,id,trans,serv
 
 We are trying to prove that, when any node calls `serv.elect`, it in
 fact has the highest `id`. That is, the `before` specification of
-`serv.elect` is a guarantee of `proto` when it calls `serv.elect`.
+`serv.elect` is a guarantee of `app` when it calls `serv.elect`.
 
 To get a sense of what we're proving, let's have a look at the
 isolate:
@@ -291,37 +286,37 @@ isolate:
     ... various declarations ...
 
     action trans.send(dst:node.t,v:id.t) = {
-	trans.sent(v,dst) := true
+        trans.sent(v,dst) := true
     }
 
     action ext:trans.recv(dst:node.t,v:id.t) = {
-	assume trans.sent(v,dst);
-	if v = serv.pid(dst) {
-	    call serv.elect(dst)
-	}
-	else {
-	    if v > serv.pid(dst) {
-		local loc[0] {
-		    call loc[0] := node.get_next(dst);
-		    call trans.send(loc[0], v)
-		}
-	    }
-	}
+        assume trans.sent(v,dst);
+        if v = serv.pid(dst) {
+            call serv.elect(dst)
+        }
+        else {
+            if v > serv.pid(dst) {
+                local loc[0] {
+                    call loc[0] := node.get_next(dst);
+                    call trans.send(loc[0], v)
+                }
+            }
+        }
     }
 
     action serv.elect(v:node.t) = {
-	assert serv.pid(v) >= serv.pid(X)
+        assert serv.pid(v) >= serv.pid(X)
     }
 
     action ext:app.send(me:node.t) = {
-	local loc[0] {
-	    call loc[0] := node.get_next(me);
-	    call trans.send(loc[0], serv.pid(me))
-	}
+        local loc[0] {
+            call loc[0] := node.get_next(me);
+            call trans.send(loc[0], serv.pid(me))
+        }
     }
 
     action node.get_next(x:node.t) returns(y:node.t) = {
-	assume ((x < y & ~(Z:node.t < y & x < Z)) | (x = node.tail & y = node.head))
+        assume ((x < y & ~(Z:node.t < y & x < Z)) | (x = node.tail & y = node.head))
     }
 
 Notice that the assertion in `serv.elect` is preserved as a guarantee. However,
@@ -333,6 +328,266 @@ method](client_server_example.html).  We start IVy using this command:
 
     $ ivy ui=cti isolate=iso_app leader_election_ring.ivy
 
+We start, as usual, with `Invariant|Check induction`. Ivy tells us the
+the safety check failed, meaning that an assert fails in some action:
+
+![IVy screenshot](images/leader1.png)
+
+When we click OK, this is what we see:
+
+![IVy screenshot](images/leader2.png)
+
+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
+discover which action failed, and explore the execution path to the
+failure, we can left-click on the transition and choose `Decompose`.
+In this case, however, we already have a pretty good idea of what went
+wrong: some node must have received its own `id` and declared itself
+leader without having the highest `id`. This is not surprising, since
+with no invariant conjectures, the only thing we know about state `0`
+is that it satisfies our axioms.
+
+On the right, we see a depiction of the state `0`. There are two
+elements in each of the two sorts `id.t` and `node.t`. Since we
+haven't yet selected any relations to view, this is all we see. We
+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:
+
+![IVy screenshot](images/leader3.png)
+
+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
+`0:id.t < 1`.  Similarly, the arrow from node 0 to id 0 means that
+`serv.pid(0) = 0`.  That is, the id of node 0 is 0. We can also see
+that node 1's id is 1 and that `trans.sent(0,1)`, in other words, id 0
+has been sent to node 0. These facts are displayed below the graph
+under the heading "Constraints".
+
+The problem is clear: node 1 is receiving its own id, so it is about
+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:
+
+![IVy screenshot](images/leader4.png)
+
+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:
+
+![IVy screenshot](images/leader5.png)
+
+And here is the counterexample to induction:
+
+![IVy screenshot](images/leader6.png)
+
+Here, some externally called action transitions from state `0`
+satisfying our conjecture to state `1` *not* satisfying the
+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:
+
+![IVy screenshot](images/leader7.png)
+
+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
+id. Notice, though, that there are two additional arrows in the diagram
+we didn't mention (the ones from node 0 to id 0 and id 0 to id 1). Maybe
+these are actually irrelevant. We could remove these manually by
+clicking on the corresponding facts below. However, we have another
+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:
+
+![IVy screenshot](images/leader8.png)
+
+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 screenshot](images/leader9.png)
+
+IVy discovered that, within 4 steps, we
+can rule out the highlighted facts. By ruling out a more general
+situation, we obtain a stronger conjecture. Since this new conjecture
+seems right, let's add it to our set by selecting
+`Conjecture|Strengthen`.
+
+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:
+
+![IVy screenshot](images/leader10.png)
+
+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
+node 2, when it couldn't have passed through node 1. This situation is
+symmetric to the previous one by rotating the ring. Unfortunately, the
+way we described the ring topology using a linear order has broken the
+ring's rotational symmetry, so this appears as a distinct case. Later,
+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 screenshot](images/leader11.png)
+
+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
+just another case of the general proposition that a lower id cannot
+pass a higher id. We chose `Conjecture|Strengthen` to add this new
+conjecture to our set.
+
+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:
+
+![IVy screenshot](images/leader12.png)
+
+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:
+
+![IVy screenshot](images/leader13.png)
+
+We add this conjecture using `Conjecture|Strengthen`. Now when we
+use `Invariant|Check induction`, we get the following:
+
+![IVy screenshot](images/leader14.png)
+
+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
+into our implementation object `app`, like this:
+
+    object app = {
+
+        action async(me:node.t) = {
+            call trans.send(node.get_next(me),serv.pid(me))
+        }
+
+        implement trans.recv(me:node.t,v:id.t) {
+            if v = serv.pid(me) {       # Found a leader!
+                call serv.elect(me)
+            }
+            else if v > serv.pid(me)  { # pass message to next node
+                call trans.send(node.get_next(me),v)
+            }
+        }
+
+        conjecture ~(serv.pid(N) < serv.pid(P) & trans.sent(serv.pid(N),N))
+        conjecture ~(serv.pid(P) < serv.pid(Q) & N:node.t < P & P < Q & trans.sent(serv.pid(P),N))
+        conjecture ~(serv.pid(N) < serv.pid(P) & N < P & P < Q & trans.sent(serv.pid(N),Q))
+        conjecture ~(serv.pid(Q) < serv.pid(N) & N < P & P < Q & trans.sent(serv.pid(Q),P))
+    }
+
+Of course, if we don't want to mess up our pretty implementation with parts of the proof,
+we can put the conjectures in a separate object and include that object in the isolate definition,
+like this:
+
+     object app_proof = {
+        conjecture ~(serv.pid(N) < serv.pid(P) & trans.sent(serv.pid(N),N))
+        conjecture ~(serv.pid(P) < serv.pid(Q) & N:node.t < P & P < Q & trans.sent(serv.pid(P),N))
+        conjecture ~(serv.pid(N) < serv.pid(P) & N < P & P < Q & trans.sent(serv.pid(N),Q))
+        conjecture ~(serv.pid(Q) < serv.pid(N) & N < P & P < Q & trans.sent(serv.pid(Q),P))
+     }
+
+    isolate iso_p = app with node,id,trans,serv,app_proof
+     
+## How not to break the rotational symmetry
+
+As we observed above, this proof is a bit messy because of the way we
+described the ring topology using a totally ordered set. There's a
+different way to describe rings that avoids this problem. Here is an
+alternative specification of `ring_topology`:
+
+    module ring_topology = {
+        type t
+        relation btw(X:t,Y:t,Z:t)
+
+        property btw(W, Y, Z) & btw(W, X, Y) -> btw(X, Y, Z)
+        property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, X, Y)
+        property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, Y, Z)
+        property btw(W, Y, Z) & btw(W, X, Y) -> btw(W, X, Z)
+        property W = X | btw(W, X, W)
+        property ~btw(X, X, Y)
+        property ~btw(X, Y, Y)
+        property btw(X,Y,Z) |  Y = Z |  btw(X,Z,Y)
+        property btw(X,Y,Z) |  Y = X |  btw(Y,X,Z)
+
+        action get_next(x:t) returns (y:t)
+
+        object spec = {
+            after get_next {
+                assert ~btw(x,Z,y)
+            }
+        }
+    }
+
+Instead of putting the nodes in a total order, we define are relation
+`btw(X,Y,Z)` that holds when `Y` occurs on the path form `X` to `Z` in
+the ring. The axioms of `btw` are a bit more complex than the axioms
+of a total order. One the other hand, it is very easy to specify
+`get_next` in terms of `btw`. We say that `y` is next after `x` in the
+ring if there is no `Z` between `x` and `y`. You might wonder if the
+properties given above for `btw` are really correct. Later, when we
+implement `ring_topology`, we'll prove that it has these properties.
+
+Now, let's try to verify the isolate `iso_app` with this new version of `ring_topology`:
+
+    $ ivy ui=cti isolate=iso_app leader_election_ring_btw.ivy
+
+As before, after `Invariant|Check induction` and `Invariant|Diagram`, this is what we see:
+
+![IVy screenshot](images/leader15.png)
+
+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
+`node.btw` doesn't appear. This is because it is a ternary relation
+and IVy doesn't know how to display it graphically in a reasonable
+way.
+
+Now, as before, let's add this as a conjecture using
+`Conjecture|Strengthen`.  As before, `Invariant|Check induction` shows
+that this conjecture is not relatively inductive. Applying `Invariant|Diagram`,
+this is what we see:
+
+![IVy screenshot](images/leader16.png)
+
+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
+been added on the right: `node.btw(2,X,Y)`. From this arrow, we can
+infer that `node.btw(2,0,1)` holds. That is, starting at `2`, and
+moving around the ring, we see `0` before `1`. We can also see this
+fact stated below under "Constraints". This means that, from `0`, we
+must pass through `1` on the way to `2`. Therefore, the id of `0`
+cannot possibly reach `2`, as the diagram shows.
+
+We can try generalizing this diagram using `Conjecture|Minimize`, but
+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:
+
+![IVy screenshot](images/leader17.png)
+
+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`:
+
+![IVy screenshot](images/leader18.png)
+
+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
+can't bypass a higher id in the ring. This illustrates that the
+complexity of the proof can be affected by how we write the
+specification. Once again, we can save this invariant and edit it into
+the definition of `app`.
+
+
+
+
+
+
 
 
 

doc/examples/leader_election_ring.ivy

@@ -50,27 +50,16 @@ module total_order = {
 module ring_topology = {
     type t
 
-    individual head:t  # ring head
-    individual tail:t  # ring tail
-
     # Axioms that ensure that t is totally ordered with head the
     # minimal element and tail the maximal element.
 
     instantiate total_order_axioms(t)   # t is totally ordered
 
-    axiom head <= X              # head is minimal
-    axiom X <= tail              # tail is maximal
-
     action get_next(x:t) returns (y:t)
-    action get_prev(y:t) returns (x:t)
 
     object spec = {
 	after get_next {
-	    assert (x = tail & y = head) | (x < y & ~ (x < Z & Z < y))
-	}
-
-	after get_prev {
-	    assert (x = tail & y = head) | (x < y & ~ (x < Z & Z < y))
+	    assert (y <= X & X <= x) | (x < y & ~ (x < Z & Z < y))
 	}
     }
 }
@@ -142,7 +131,7 @@ object serv = {
 
 module process(pid) = {
 
-    action send(me:node.t) = {
+    action async(me:node.t) = {
 	call trans.send(node.get_next(me),pid(me))
     }
 
@@ -155,10 +144,10 @@ module process(pid) = {
         }
     }
 
-    # conjecture ~(pid(N1) <= pid(N0) & trans.sent(pid(N1),N1) & pid(N1) ~= pid(N0))
-    # conjecture ~(pid(N2) <= pid(N0) & trans.sent(pid(N2),N1) & N0 <= N1 & N2 <= N0 & N0 ~= N2 & N1 ~= N0)
-    # conjecture ~(pid(N2) <= pid(N0) & trans.sent(pid(N2),N1) & N0 <= N1 & N1 <= N2 & N1 ~= N0)
-    # conjecture ~(pid(N2) <= pid(N0) & trans.sent(pid(N2),N1) & N1 <= N2 & N2 <= N0 & N0 ~= N2)
+    # conjecture ~(serv.pid(N) < serv.pid(P) & trans.sent(serv.pid(N),N))
+    # conjecture ~(serv.pid(P) < serv.pid(Q) & N:node.t < P & P < Q & trans.sent(serv.pid(P),N))
+    # conjecture ~(serv.pid(N) < serv.pid(P) & N < P & P < Q & trans.sent(serv.pid(N),Q))
+    # conjecture ~(serv.pid(Q) < serv.pid(N) & N < P & P < Q & trans.sent(serv.pid(Q),P))
 
 }
 
@@ -168,7 +157,7 @@ instance app: process(serv.pid)
 
 import serv.elect
 import trans.send
-export app.send
+export app.async
 export trans.recv
 
 isolate iso_app = app with node,id,trans,serv

doc/examples/leader_election_ring_btw.ivy

@@ -0,0 +1,168 @@
+#lang ivy1.6
+
+################################################################################
+#
+# A module containing the axioms of total order
+#
+################################################################################
+
+module total_order_axioms(t) = {
+    relation (X:t < Y:t)
+    axiom [transitivity] X:t < Y & Y < Z -> X < Z
+    axiom [antisymmetry] ~(X:t < Y & Y < X)
+    axiom [totality] X:t < Y | X = Y | Y < X
+}
+
+################################################################################
+#
+# A module containing the injectivity axiom
+#
+################################################################################
+
+module injectivity_axioms(f) = {
+    axiom [injectivity] f(X) = f(Y) -> X = Y
+}
+
+################################################################################
+#
+# ADT describing a totally ordered datatype
+#
+################################################################################
+
+module total_order = {
+    type t
+    instantiate total_order_axioms(t)   # t is totally ordered
+}
+
+################################################################################
+#
+# ADT describing a ring topology.
+#
+# The module includes a ring_head and ring_tail elements, and a ring
+# total order relation.
+#
+# The module also includes get_next and get_prev actions.
+#
+# In this module, the ring topology is arbitrary and fixed.
+#
+################################################################################
+
+module ring_topology = {
+    type t
+    relation btw(X:t,Y:t,Z:t)
+
+    property btw(W, Y, Z) & btw(W, X, Y) -> btw(X, Y, Z)
+    property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, X, Y)
+    property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, Y, Z)
+    property btw(W, Y, Z) & btw(W, X, Y) -> btw(W, X, Z)
+    property W = X | btw(W, X, W)
+    property ~btw(X, X, Y)
+    property ~btw(X, Y, Y)
+    property btw(X,Y,Z) |  Y = Z |  btw(X,Z,Y)
+    property btw(X,Y,Z) |  Y = X |  btw(Y,X,Z)
+
+    action get_next(x:t) returns (y:t)
+
+    object spec = {
+	after get_next {
+	    assert ~btw(x,Z,y)
+	}
+    }
+}
+
+
+################################################################################
+#
+# Types, relations and functions describing state of the network
+#
+################################################################################
+
+# A totally ordered set of ids
+instance id : total_order
+
+# A ring topology of nodes
+instance node : ring_topology
+
+################################################################################
+#
+# The transport-layer service specification
+#
+################################################################################
+
+object trans = {
+
+    relation sent(V:id.t, N:node.t) # The identity V is sent at node N
+    init ~sent(V, N)
+    
+    action send(dst:node.t, v:id.t)
+    action recv(dst:node.t, v:id.t)
+
+    object spec = {
+	before send {
+	    sent(v,dst) := true
+	}
+	before recv {
+	    assert sent(v,dst)
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level service specification
+#
+################################################################################
+
+
+object serv = {
+
+    function pid(X:node.t) : id.t          # map each node to an id
+
+    instantiate injectivity_axioms(pid)    # id's are unique
+
+    action elect(v:node.t)                 # called when v is elected leader
+
+    object spec = {
+	before elect {
+	    assert pid(v) >= pid(X)        # only the max pid can be elected
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level protocol
+#
+################################################################################
+
+module process(pid) = {
+
+    action async(me:node.t) = {
+	call trans.send(node.get_next(me),pid(me))
+    }
+
+    implement trans.recv(me:node.t) {
+        if v = pid(me) {  # Found a leader
+            call serv.elect(me)
+        }
+	else if v > pid(me)  { # pass message to next node
+	    call trans.send(node.get_next(me),v)
+        }
+    }
+
+    # conjecture ~(serv.pid(P) < serv.pid(N) & trans.sent(serv.pid(P),P))
+    # conjecture ~(serv.pid(N) < serv.pid(P) & serv.pid(Q) < serv.pid(N) & node.btw(Q,N,P)
+    #                  & trans.sent(serv.pid(N),Q))
+}
+
+# instantiate one process per ring element
+
+instance app: process(serv.pid)
+
+import serv.elect
+import trans.send
+export app.async
+export trans.recv
+
+isolate iso_app = app with node,id,trans,serv
+

ivy/ivy_actions.py

@@ -582,7 +582,10 @@ class EnvAction(ChoiceAction):
             result = join_action(result, foo, domain.relations)
         return result
     def __str__(self):
-        return '{' + ','.join(a.label for a in self.args) + '}'
+        if all(hasattr(a,'label') for a in self.args):
+            return '{' + ','.join(a.label for a in self.args) + '}'
+        return super(ChoiceAction, self).__str__()
+
     @property
     def formal_params(self):
         return []

ivy/ivy_art.py

@@ -384,7 +384,6 @@ class AnalysisGraph(object):
     def decompose_state(self,state):
         if hasattr(state,'expr') and state.expr != None:
             other_art = AnalysisGraph(self.domain)
-            print [a for a in other_art.actions]
             with AC(other_art):
                 res = decompose_action_app(state,state.expr)
                 if res != None:

ivy/ivy_core.py

@@ -2,11 +2,28 @@
 # Copyright (c) Microsoft Corporation. All Rights Reserved.
 #
 # TODO get rid of import *
+
 from z3 import *
+import ivy_utils as iu
 
 def get_id(x):
     return Z3_get_ast_id(x.ctx_ref(), x.as_ast())
 
+def biased_core(s,alits,unlikely):
+    """ Try to produce a minimal unsatisfiable subset of alits, using as few
+    of the alits in unlikely as possible. 
+    """
+    core = alits
+    for lit in unlikely:
+        test = [c for c in core if get_id(c) != get_id(lit)]
+        if s.check(test) == unsat:
+            core = test
+    is_sat = s.check(core)
+    assert is_sat == unsat
+    core = minimize_core(s)
+    return core
+    
+
 def minimize_core_aux2(s, core):
     mus = []
     ids = {}

ivy/ivy_graph.py

@@ -531,8 +531,9 @@ class Graph(object):
         return concept_from_formula(fmla)
 
     def new_relation(self,concept):
-        add_domain_concept(self.concept_domain.concepts,concept)
-        self.new_relations.append(concept)
+        if concept.name not in self.concept_domain.concepts:
+            add_domain_concept(self.concept_domain.concepts,concept)
+            self.new_relations.append(concept)
             
     def state_changed(self,recomp=True):
         cs = self.concept_session

ivy/ivy_solver.py

@@ -17,7 +17,7 @@ from ivy_logic_utils import used_variables_clause, used_variables_ast, variables
    to_clauses, constants_clauses, used_relations_clauses, rel_inst, fun_eq_inst, \
    is_ground_lit, used_constants_clauses, substitute_constants_clauses, eq_atom, \
    functions_clauses, fun_inst, substitute_lit, used_constants_clause, used_symbols_clause,Clauses, used_symbols_clause, and_clauses, true_clauses, used_symbols_ast, sym_placeholders, used_symbols_clauses
-from ivy_core import minimize_core
+from ivy_core import minimize_core, biased_core
 import ivy_utils as iu
 import ivy_unitres as ur
 import logic as lg
@@ -392,13 +392,15 @@ def formula_to_z3(fmla):
         return z3.ForAll(z3_variables, z3_formula)
 
 
-def unsat_core(clauses1, clauses2, implies = None):
+def unsat_core(clauses1, clauses2, implies = None, unlikely=lambda x:False):
 #    print "unsat_core clauses1 = {}, clauses2 = {}".format(clauses1,clauses2)
 #    assert clauses1.defs == []
     fmlas = clauses1.fmlas
     s2 = z3.Solver()
     alits = [z3.Const("__c%s" % n, z3.BoolSort()) for n,c in enumerate(fmlas)]
     cc = [z3.Or(z3.Not(a),formula_to_z3(c)) for a,c in zip(alits,fmlas)]
+    foo = [(a,f) for a,f in zip(alits,fmlas) if unlikely(f)]
+    unlikely_lits = [a for a,f in foo]
     for d in clauses1.defs:
         s2.add(formula_to_z3(d.to_constraint()))
     for c in cc:
@@ -410,7 +412,10 @@ def unsat_core(clauses1, clauses2, implies = None):
     if is_sat == z3.sat:
 #        print "unsat_core model = {}".format(get_model(s2))
         return None
-    core = minimize_core(s2)
+    if unlikely_lits:
+        core = biased_core(s2,alits,unlikely_lits)
+    else:
+        core = minimize_core(s2)
     core_ids = [get_id(a) for a in core]
     res = [c for a,c in zip(alits,fmlas) if get_id(a) in core_ids]
 #    print "unsat_core res = {}".format(res)
@@ -1069,8 +1074,11 @@ def clauses_model_to_diagram(clauses1,ignore = None, implied = None,model = None
 
     uc = true_clauses()
     if weaken:
+        def unlikely(fmla):
+            # remove if possible the =constant predicates
+            return ivy_logic.is_eq(fmla) and ivy_logic.is_constant(fmla.args[0])
         clauses1_weak = bound_quantifiers_clauses(h,clauses1,reps)
-        res = unsat_core(res,and_clauses(uc,axioms),clauses1_weak) # implied not used here
+        res = unsat_core(res,and_clauses(uc,axioms),clauses1_weak,unlikely=unlikely) # implied not used here
 #    print "clauses_model_to_diagram res = {}".format(res)
 
 #    print "foo = {}".format(unsat_core(and_clauses(uc,axioms),true_clauses(),clauses1))

ivy/ivy_ui_cti.py

@@ -1,7 +1,7 @@
 import ivy_ui
 import ivy_logic as il
 import logic as lg
-from ivy_interp import State,EvalContext,reverse
+from ivy_interp import State,EvalContext,reverse,decompose_action_app
 import ivy_module as im
 import ivy_logic_utils as ilu
 import logic_util as lu
@@ -105,6 +105,7 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
         from proof import ProofGoal
         from ivy_logic_utils import Clauses, and_clauses, dual_clauses
         from random import randrange
+        from ivy_art import AnalysisGraph
         
         with self.ui_parent.run_context():
 
@@ -118,12 +119,13 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
                 post = ag.execute(action, pre, None, 'ext')
             post.clauses = ilu.true_clauses()
 
-            to_test = list(self.conjectures) + [None]  # None = check safety
+            to_test =  [None] + list(self.conjectures)  # None = check safety
 
             while len(to_test) > 0:
                 # choose randomly, so the user can get another result by
                 # clicking again
-                conj = to_test.pop(randrange(len(to_test)))
+#                conj = to_test.pop(randrange(len(to_test)))
+                conj = to_test.pop(0)
                 assert conj == None or conj.is_universal_first_order()
                 used_names = frozenset(x.name for x in il.sig.symbols.values())
                 def witness(v):
@@ -162,7 +164,6 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
                 )
 
                 if conj == None:
-                    print "check safety"
                     res = ag.check_bounded_safety(post, _get_model_clauses)
                 else:
                     res = ag.bmc(post, clauses, None, None, _get_model_clauses)
@@ -172,13 +173,14 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
                     assert len(res.states) == 2
     #                self.set_states(res.states[0], res.states[1])
     #                self.cti = self.ui_parent.add(res)
+
                     self.g = res
                     self.rebuild()
                     self.view_state(self.g.states[0], reset=True)
                     self.show_used_relations(clauses)
                     #self.post_graph.selected = self.get_relevant_elements(self.post_state[2], clauses)
                     if conj == None:
-                        self.ui_parent.ok_dialog('An assertion failed. A failing state is displayed. You can decompose\nthe failing action observe the failing execution. ')
+                        self.ui_parent.ok_dialog('An assertion failed. A failing state is displayed. You can decompose\nthe failing action to observe the failing execution. ')
                     else:
                         self.ui_parent.text_dialog('The following conjecture is not relatively inductive:',
                                                    str(il.drop_universals(conj.to_formula())),on_cancel=None)
@@ -201,6 +203,18 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
                 self.current_concept_graph.show_relation(rel,'+',update=False)
                 if both:
                     self.current_concept_graph.show_relation(rel,'-',update=False)
+        need_update_relations = False
+        for app in ilu.apps_clauses(clauses):
+            if len(app.args) == 3 and il.is_numeral(app.args[0]):
+                fmla = app.rep(app.args[0],il.Variable('X',app.args[1].sort),il.Variable('Y',app.args[2].sort))
+                concept = self.current_concept_graph.g.formula_to_concept(fmla)
+                self.current_concept_graph.g.new_relation(concept)
+                need_update_relations = True
+                self.current_concept_graph.show_relation(concept,'+',update=False)
+                if both:
+                    self.current_concept_graph.show_relation(concept,'-',update=False)
+        if need_update_relations:
+            self.current_concept_graph.update_relations()
         self.current_concept_graph.update()
 
     def diagram(self):

test/client_server3.py

@@ -55,14 +55,14 @@ with ivy_module.Module():
     cg = ui.current_concept_graph
     cg.show_relation(cg.relation('s'),'+')
     cg.gather() 
-    cg.select_fact(cg.fact('1:client ~= 0:client'),False)
-    cg.select_fact(cg.fact('0:client ~= 1:client'),False)
+    cg.select_fact(cg.fact('1:client ~= 0'),False)
+    cg.select_fact(cg.fact('0:client ~= 1'),False)
     main_ui.answer("OK")
     assert cg.is_inductive(), "should have been relatively inductive"
     main_ui.answer("OK")
     assert cg.is_sufficient(), "should have been sufficient"
-    cg.select_fact(cg.fact('1:client ~= 0:client'),True)
-    cg.select_fact(cg.fact('0:client ~= 1:client'),True)
+    cg.select_fact(cg.fact('1:client ~= 0'),True)
+    cg.select_fact(cg.fact('0:client ~= 1'),True)
     main_ui.answer("OK")
     cg.minimize_conjecture(bound=2)
     main_ui.answer("OK")

test/transitive.py

@@ -22,7 +22,7 @@ with ivy_module.Module():
     main_ui = new_ui()
     ui = main_ui.add(ivy_from_string(prog))
     cg = ui.view_state(ui.node(0))
-    cg.show_relation(cg.relation('X:t < Y:t'),'+')
+    cg.show_relation(cg.relation('X:t < Y'),'+')
     cg.split(cg.relation('=x'),cg.node('t'))
     cg.show_relation(cg.relation('=x'),'-')
     cg.split(cg.relation('=y'),cg.node('~=x'))