The Joys of Working Code

I've discovered that the AffineTransform support in prefuse appears to be broken. Flipping (i.e. scaling by a negative factor) doesn't work, or at least misplaces the transformed co-ordinates. Rotating the display appears to expose some form of redrawing bug, as parts of the display aren't drawn (or need the display to be panned or scrolled).

This is in addition to what I imagine is a race condition of some description that causes a ConcurrentModificationException (if that is the correct exception class) to be thrown by a collection somewhere in the bowels of the library.

All in all, I'm glad that:

1. the AffineTransform modification didn't take too much time;


2. that I've been able to get some diagrams done for my presentation; and


3. that not much was riding on this project.

While it would have been nice to have a complete package to deliver to my supervisor, I can deal with having a dodgy hack. In addition, I don't think I'll be able to get my log filter scripts completed in time for my presentation or, probably, the end of the project. I'd have liked to have more than one problem displayable, but I can't seem to get the filters to deal with things like subsumption and demodulation properly.

Curses!

Screen-shots now hosted on Flickr

Screen-shots now hosted on Flickr, originally uploaded by thsutton.

I'm now putting my various screen-shots and other images on Flickr so that they'll remain live once my RSISE account goes off-line.

So, without further ado, a repeat of the latest screen-shot, this time, from Flickr.

On the Benefits of Documentation and Its Reading

I am stupid. That is the only possible explanation for the way I've wasted most of the last couple of weeks of work, by hard-coding a number of transformations into my code, when the library I'm using (prefuse, just in case you'd forgotten) supports java.awt.geom.AffineTransform, in all it's glory, or should that be gory. So now, I've been hacking out all my size handling code; all my device co-ordinate handling code; all the uncommented, unneccessary, inexplicable cruft that has been cluttering up my code, and replacing it all with a single AffineTransform applied to the Display.

This has meant that I've been able to trash my idea of creating a new class. I'd already pretty much finished AdjacencyMatrixManager which was to know the size we were drawing at (i.e. the dimensions of the matrix we were filling in) and be able to convert points in a useful co-ordinate system (such as one with the origin at the bottom-left) into device co-ordinates. As quick as it was to hack up, it didn't take much longer to tear out again.

Now, all my classes are smaller (most of the are just a couple of one-liners in an interface stub), my code is [probably] going to be faster (there are a lot fewer method calls), and it is a lot simpler, with all of the stupidity caused by the device co-ordinates confined to one place.

The only problem I can see will be in adding interface elements that I don't want the AffineTransform to be applied to. Things like tooltips mustn't be transformed, or we'll wind up with huge, unreadable text the obscures its subject. On the other hand, it will be a lot easier to do things like highlighting effects, and such like as I no longer need to pass around various parameters.

On the whole, this is the better path, even though I may need to start poking at prefuse's insides.

Colouring Inside the Box

SET012-demo.png (PNG Image, 2551x284 pixels)

Now that the data sets can be reprocessed more easily, and have more, relevant, data in them, I've started working on the colouring code. At the moment, I've just cleaned up the colours (to get rid of the grey fill colour, etc) and added highlighting of factors. In the image linked above, factors appear as blue points, the green points on the left-hand side are the "given" clauses and the black points are any edges not created by factorisation.

Also evident in this image are the diagonal lines mentioned in a previous post, caused by the implementation of the theorem prover.

All in all, it has been a fairly productive day (so far).

Input Processing: The Joys of a Dodgy Hack

Just finished a rewrite of the input processing scripts. I now have a single Python script that reads a SOFTIE log from a file and does a few things with it. The first new feature is that it processes the option and parameter declarations output at the start of the log and warns the user if very_verbose, print_kept and print_deleted are not turned on. It understands enough to set and unset option flags and parameters, but the parsing is a little stupid. It will ignore warning lines, but treats everything else that looks like a parameter or option as a parameter or option, until it sees the start of the theorem proper.

It then proceeds to build a number of lists of clause Nodes. There is a list of all clauses and a list each of those that were kept, deleted and subsumed. Whilst building the lists of clauses, it keeps an eye on the time (i.e. the iteration) and increments it when necessary.

Once it is done building the lists of clauses, it, by default, prints out the list of kept clauses as a graph in the XML dialect used by prefuse, with the nodes and edges bearing the attributes that the visualisation software expects.

Though it would probably be faster if written with more care (or in a text processing language like Perl or awk), this new script has turned what used to be a 5 (or more) stage process with 3 passes over the log file, into a single stage process with one pass over the data. It doesn't spawn any processes and doesn't use much memory (as opposed to the old shell scripts, and the libxml2 Python scripts respectively).

A Traditional Adjacency Matrix

John just raised the point that the size problem would be solved by using a 'full' adjacency matrix on the usable set (instead of all clauses). This would indeed give us a square of n size, with the triangular half of it filled. It might also be interesting in that it would allow us to, more easily, represent numerical statistics. These might include the number of clauses that were subsumed by a particular set of clauses, the number of children or the distance from the proof.

On the less positive side, it is possible that the plot might tend toward completeness. This may be a boon however as there may be some relation between its tendency toward completeness and the likelihood of finding a proof. Also, with a denser graph it may be reasonable (though probably quite naive) to assume that any blank space will be more meaningful.

These issues need, and deserve, to be addressed by implementing this idea. Sounds like I'm going to be trying to get a lot of little things done tomorrow.

The end is nigh. Or at least in sight.

The end is nigh, or in sight, depending on which way you look at it. There are only a few weeks left of the summer scholarship program, and a lot of work still to be done.

On the other hand, a meeting with my supervisor (John Slaney) today has reassured me that I'm not doing as badly as I had expected, and when you look at the graphs I've been drawing on a large scale, you can see why. The matrix style diagrams display a number of features that clearly illustrate properties of the system, and the problems being solved.

In the SET012 problem, we can clearly see repeating patterns which may be a graphical reflection of the symmetry of the problem (from Set Theory and regarding some relation between sets and another). Another interesting feature is a number of peculiar 'gaps' in the graph where large numbers of factors are generated consecutively. One of these gaps is several tens of clauses wide.

Also clearly visible are sloping vertical "lines" (in reality they are just adjacent points). This appears to be caused by the method used by the reasoning system. To generate new clauses from a given clause, the system attempts to unify it with the clauses in the usable set. This process traverses the list of usable clauses in reverse order which, for given clauses that unify with a large number of usable clauses, gives the appearance of sloping lines.

Other noticeable features include the appearance of a number of short horizontal "lines", strangely regular patterns, patterns that appear to be interrupted then continue and some patterns that bear a small resemblance to the Game of Life and other cellular automata.

I'm about to start working on adding some useful features to help give some more meaning to the graph. Unless I have a stroke of genius, this will probably be restricted to colouring the nodes (to easily differentiate factors, given clauses, etc) and highlighting those nodes that form part of the proof.

When these features are added in (hopefully be tomorrow or early next week), I'll move on to dynamic exploration. Some form of "zoom" function whereby those parts of the graph not in the immediate vicinity of the cursor are scaled down may be useful due to the rather long horizontal axis. Another feature that I'll have a go at implementing is a "cross-hair" on the cursor to allow the user to view other relations involving the node/s they are interested in, trace across to row and column labels, etc. Another possibility is to have the system display the text of a clause, the method that generated it and other possibly interesting data.

All in all, there is too much to do, and too little time.