Testing the optimality of algorithms using Alloy - Part 2

 Continuing where we left off last time on
http://feels-good-to-ramble.blogspot.com/2012/11/testing-optimality-of-algorithms-using.html
, I give the description of a first-shot Alloy model that tries to check whether there is a graph for which the Alloy analyzer can find a better (cheaper) vertex coloring than the one based on BFS (Breadth First Search).
It is not the intent of this post to be a tutorial for Alloy. There are more competent places for that viz.
  http://alloy.mit.edu/alloy/documentation.html
But some words to build the context are in order.  Pardon me if this is turning out to be some kind of 'notes to myself' article.
 How many times has it happened that we are confident that an algorithm we devised is correct, only to find some days later, and sometimes after the solution reaches the Testing department or the Customer, that there was one or more important scenarios that we missed out leading to costly recoding/fixing/rework not to mention embarrassment ?
 When the nature of the problem is such that there are a combinatorially large number of possible cases to test, Test engineers may also miss some or all of these cases, just because there are so many of them even for a relatively small problem size, and the tests simply did not cover the problem cases ( which might be like needles in a haystack). Now, consider the situation where these one off trouble cases happen to introduce say, a possible security threat, or cause the application to hang completely in a deadlock, or give a completely way-off calculation for the insurance premium to be charged. Then, it becomes important for Testing to cover all cases, so as to instil confidence in the provided solution. The Alloy tool helps in this humanly tedious (if not impossible) task, by an ability to deliver at the analysis and design (i.e. pre-coding) stage itself. Developers can model their solution at a high level of abstraction in the Alloy language, and run checks on what they have modeled, long before actual coding in the implementation language. Alloy lets you test the model in two ways.

•   produces instances of the model or tells you the model is inconsistent and no instance exists. This is done via the 'run' command
•  produce counter-examples for an assertion coded in Alloy. This is done via the 'check' command. If the assertion is a valid one then Alloy cannot produce any counter-examples and reports likewise.

Both the above tests are done for a limited scope, i.e. all the combinatorially many solutions are evaluated for only a fixed number of objects of a 'signature' i.e. set (the phrase in bold corresponds to the phrase, 'small problem size' above. In Alloy 'fixed' is not necessarily very small, because SAT analyzers today can address fairly large problems, even in the case where the problem is NP-complete). The 'run' command might be specified like this in the Alloy file.

run bfs_suboptimal for 10

where bfs_suboptimal is the name of a predicate that we defined earlier in the model. In this case, 10 is the fixed number of objects of any signature that the Alloy analyzer will process. The basis for trusting the analysis for a fixed number, or 'scope' of the analysis, is that most often the results carry over to higher numbers. But one needs to 'experiment' with several values before achieving some confidence level.

The 'check' command might be specified like this.

check coloringIsCorrect for 6

where coloringIsCorrect is the name of an assert block that was defined in the model.

First remember that the Alloy modeling language is a declarative language after the style of Prolog or Lisp. This means the statements of an Alloy program describe the constraints etc. that hold in the resultant model, and the Alloy analyzer derives the model that satisfy these constraints. This is a paradigm shift for most of us programmers who have been raised on a staple of imperative languages like Java, C, C++ etc. where the program statements are actually instructions about what steps to take, the resulting constraints and values etc. being only implied. To mention one big difference, Alloy has no 'assignment' statement. Something like "x=x+1" is simply a 'FALSE' statement in Alloy, just as in Mathematics, and does not assign anything to x. Only some familiar imperative languages have accorded legitimacy to such syntax. To give an example of an Alloy model ( we use the term 'model' interchangeably for an Alloy program source as well as for the structures generated from the program by the Alloy analyzer). Let's take a directed acyclic graph (DAG) data structure. This would be specified in Alloy as follows :

--Directed Acyclic Graph

sig Node{
   children: set Node
}

fact {

--The first fact asserts that there is at least one node in our model

  some Node

--The next fact asserts that no node is its own ancestor, i.e. that the structure

-- has no cycles

  no node:Node | node in node.^children

--The next fact asserts that any two nodes have a path from at least one of them

--to the other

  all disj n1,n2:Node | n1 in n2.^children or n2 in n1.^children
}

--Predicate to keep generating and showing instances of the data structure 

--described by the above model

pred show(){}

--Run the predicate for at most 5 nodes

run show for 5

  Some of the DAGs obtained by running the analyzer on the above model are shown in the images of figures 1a to 1d.

Fig 1a

Fig 1b

Fig 1c

Fig 1d

For our problem of deducing whether the BFS-based vertex-coloring algorithm we outlined in the last post is suboptimal, our approach will be to define a predicate called bfs_suboptimal which asserts that the number of colors as derived by the Alloy analyzer, given a free hand so to say, is less than the number of colors that are required if the coloring follows the BFS-based approach. The BFS-coloring is described in the predicate bfs. This is a bit tricky to code, because the BFS algorithm has more of a "do this-do that" nature, and mapping that to the declarative paradigm of Alloy can be non-trivial. We look at this algorithm as follows - note we use the terms 'vertex' and 'node' interchangeably. First we choose a starting vertex (Node), which will form the root of the BFS tree to be generated by the algorithm, and assign it the first color in the Color set. We then 'discover' nodes adjacent to this node and color them, and then the (as yet undiscovered) nodes adjacent to those in turn and so on. At any stage, we use the fact that all nodes adjacent to a given node, except for the ones that have already been discovered in a previous stage by the BFS algorithm,  are at the same distance from the starting vertex, i.e. at the same 'level'. Any node will be then given a color that is the 'lowest' color  in the set of colors that were earlier assigned to all discovered nodes that are adjacent to this node (for example if all colors are numbered 0,1,2,...,  and the set of colors contains the colors 2,4,8 then color 2 is the lowest in this set). Before we proceed further, I must clarify something here. The use of words 'earlier', 'discover' etc. gives a connotation of time, which can be misleading. As mentioned earlier there is no assignment, so it is not as if a single set of discovered nodes get updated from stage to stage as new nodes are discovered. On the contrary, we need to store (this is one way to do it) what may be called a snapshot ( set) of discovered nodes at every stage, unique to that stage. I'll  provide the details as we discuss the program itself.

We first include several modules that we will use, and that come with the Alloy installation. These are parametrized modules and they define predicates related to Graphs, and predicates related to there being a total ordering defined for Nodes, Colors and Levels.

open util/graph[Node] as GR

open util/ordering[Node] as trnode

open util/ordering[Color] as CO

open util/ordering[Level] as LV

Then we define several 'signatures' which are like Java Classes, and also like Sets of Mathematics. The signature 'Node' represents the set of vertices of a graph. 'Level' represents the set of levels. The level of a vertex is its least distance from the starting vertex when a BFS tree is created from the graph. The signature Node has some interesting fields. The field 'adjacency' is the set of Nodes adjacent to a Node. The field 'done_nodes' is the snapshot set of Nodes discovered at the end of a stage. Since at every BFS stage exactly one new Node is discovered, we store this snapshot with a Node. The field 'color' is a Node's color as per the BFS algorithm, while the field 'optcolor' is the color as per only the bare minimal constraints defined i.e. as per the non-BFS solution.

sig Color {}

sig Node{

    adjacency: set Node,

    level: Level,

    done_nodes: set Node, 

    color: one Color,

    optcolor: one Color

}

sig Level {}

 This is followed by several predicates, most of which are internal ones, but some of them are also later used as  predicates for the 'run' command.

This predicate asserts  (by the way, see http://www.thefreedictionary.com/predicate for meanings of the word 'predicate') that elements of the set Node form an undirected graph with no self loops and that the graph is strongly connected i.e. that all of the undirected graph is just one connected component.

pred  undirected_graph() {

    GR/undirected[adjacency]

    GR/noSelfLoops[adjacency]

       GR/stronglyConnected[adjacency]

}

This next one is an Alloy function (a function in Alloy simply wraps an Alloy expression). It returns  a sibling, if any,  at the same level as the input Node n - this requires you to look at the graph with a BFS tree superimposed on it, the starting vertex for the BFS being the root of the BFS tree. Since there may be one or no such sibling in the BFS tree, the return value of the function is qualified with the keyword 'lone', meaning 0 or 1.

fun next_sibling(n:Node): lone Node

{

  let parent_nodes= level.(LV/prev[n.level]) |

     some parent_nodes implies {

       let siblings = parent_nodes.adjacency -  n.done_nodes |

        some siblings  implies

          trnode/min[siblings]

        else

          none

     }

    else

      none

}

This Alloy function will (as is obvious from its name) find the child at the next level, from input Node, if any.

fun first_child_at_next_level(last_upper_node:Node) : lone Node

{

   trnode/min[last_upper_node.level.~level.adjacency - last_upper_node.done_nodes]

}

The following predicate is the workhorse for the BFS algorithm. It first calls the init predicate explained later. Then it calls the step predicate, passing two consecutive levels (remember Levels are totally ordered). This is very typical of how we specify in Alloy how two stages of an algorithmic model are related. Finally it imposes the correctness constraint for vertex coloring, so as to further narrow down the graphs enumerated by Alloy to only the valid ones.

pred bfs() {

    init 

    all n:Node - trnode/last  |    { let n'=trnode/next[n]  | step [n,n'] } 

    correctness

}

The following predicate initializes the BFS, by asserting that the first Node ( there is a total order on Node too) gets the first color ( as calculated by the BFS algorithm) from Color (there is a total order on Color too), and optcolor, which represents the color as calculated by Alloy (the prefix 'opt' stands for optimal, which is something of a misnomer), is also initialized to the same color.

pred init () {

    let n=trnode/first |

    n.level=LV/first and n.done_nodes=n and n.color=CO/first and n.optcolor=n.color

}

This predicate asserts the basic vertex-coloring requirement that any coloring produced by BFS must satisfy, i.e. that a Node's 'color' must be different from that of its adjacent Nodes.

pred correctness {

   all n:Node | n.color not in n.adjacency.color

}

This assert is just a wrapper over the predicate 'correctness', so that we can run some 'check' commands (as mentioned before) to ensure the generated models have correct coloring.

assert coloringIsCorrect {

    correctness

}

The following predicate asserts the basic vertex-coloring requirement that any coloring produced using the 'optcolor' field must satisfy, i.e. that a Node's 'optcolor' must be different from that of its adjacent Nodes. Note how this depends only on specifying the bare minimum constraint. This predicate is used to generate the 'optcolor' fields. Being as minimally constrained as it is, this predicate will not actually generate optimal colorings if used in isolation, but the single predicate 'bfs_suboptimal', described later will let us do what we set about to i.e. to prove that it generates a coloring that is better than the BFS-based, thus showing that BFS-coloring is suboptimal.

pred coloring_prob  { (no n,m:Node | (m in n.adjacency and n.optcolor= m.optcolor) ) }

The following predicate sets the BFS 'color' of a Node to be the minimum from the set of Colors that is the complement of the BFS 'color's of the already discovered Nodes adjacent to it - that's a mouthful, but you get the idea. The effect is that the input Node is given the least color chosen from the entire set of Colors, minus the ones given to adjacent Nodes that have been discovered thus far.

pred set_color(n:Node)

{

 let cols=Color - (n.adjacency & n.done_nodes).color |

   n.color = CO/min[cols]

}

The following predicate is probably the most important one for the BFS coloring. It relates two consecutive BFS coloring stages. Since a stage corresponds to a Node, it takes two Nodes  as arguments. These Nodes are the ones that were discovered consecutively in the two consecutive stages. The second argument Node is asserted to be either a sibling (which here means either an immediate sibling or a cousin) of the first argument Node or the first child at the next level. Finally, the second Node is colored using the predicate 'set_color' described earlier.

--This creates the next level from the current level. It is based on traversing the adjacencies

pred step (n,n': Node) {

     some n::next_sibling implies

     {

       n'=n::next_sibling and n'.level= n.level and n'.done_nodes = n.done_nodes + n'

     }

    else {

     let m=n::first_child_at_next_level  |

      some m implies {

       n'=m and n'.level = LV/next[n.level] and  n'.done_nodes = n.done_nodes + n'

      }

      else {

         n'.level = n.level

         n'.done_nodes = n.done_nodes

      }

    }

    set_color[n']

}

This fact brings it all together, ensuring that the Graph structures generate by Alloy have Node 'color's as per BFS, and Node 'optcolor's as per the bare minimum constraints as specified in predicate 'coloring_prob'.

fact {

  undirected_graph 

  bfs

  coloring_prob

}

This predicate further constrains our model to those in which the number of colors used by the BFS is higher than the ones obtained from 'coloring_prob'. 

If there happens to be some Graph structure that Alloy finds for this predicate, then it means our BFS-based  coloring algorithm is suboptimal for those graphs, and therefore suboptimal in general.

pred bfs_suboptimal()

{

   #Node.optcolor < #Node.color

}

 Finally, we run the predicate 'bfs_suboptimal' for at most 5 objects of any signature, except for the signature Color, which we limit to 4. I actually started with values 3,then 4 etc. for the generic scope value, but didn't find any suboptimal graph coloring. The first suboptimal graphs started appearing for values 5 onwards. Similar experimentation was conducted for the scope value of Color.

run bfs_suboptimal for 5 but 4 Color

The following images are for some of the instances produced by the Alloy analyzer for the above 'run'. The red, double-arrowed edges between the blue Nodes denote the adjacency. A saffron colored arrow points from a Node to the 'optcolor' set for a Node, while any brown arrow points from a Node to the BFS 'color' for that Node. In all the instances, Node0 is the starting vertex for the BFS.

Fig 2a

Fig 2b

Fig 2c

Here's a fairly complex graph of 10 Nodes for a different run. I have eliminated the Color objects to avoid clutter.

Fig 2d

 So we seem to have found a fairly dependable way to check whether our algorithms behave as expected (e.g. whether our BFS-based coloring is suboptimal, in this case). But are you sure ? The alert reader may argue that our model is flawed. Our BFS algorithm was run only for a single Node as starting vertex. May be if we had coded our Alloy program to run the BFS for every node of a graph as starting vertex in turn, and then called 'bfs_suboptimal', may be we would never have found any suboptimal graph. Note that this way our algorithm would still be in complexity class P, since the time would simply get multiplied by n, the number of vertices. 
 We'll see about this in the next post.