From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Fri, 28 Aug 2009 17:27:32 +0000 (+0100)
Subject: Extend proof to non-connected graphs; cosmetic improvements
X-Git-Tag: 3.4~71^2
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~yarrgweb/git?p=ypp-sc-tools.db-test.git;a=commitdiff_plain;h=ca87f8859bd503ffcaf7760879ffc746f967e2dd

Extend proof to non-connected graphs; cosmetic improvements
---

diff --git a/yarrg/yppedia-chart-parser b/yarrg/yppedia-chart-parser
index 92b609c..fca7abd 100755
--- a/yarrg/yppedia-chart-parser
+++ b/yarrg/yppedia-chart-parser
@@ -36,6 +36,7 @@ sub print_messages () {
 	print sort @$m or die $!;
     }
 }
+sub progress ($) { print "($_[0])\n"; }
 
 if (@ARGV && $ARGV[0] eq '--debug') {
     shift @ARGV;
@@ -354,7 +355,7 @@ sub compare_island_lists () {
 	}
 	my $dbarch= $dbisland2arch{$island};
 	if ($wiarch ne $dbarch) {
-	    change("change archipelago from $dbarch to $wiarch".
+	    change("archipelago change from $dbarch to $wiarch".
 		   " for island $island");
 	}
     }
@@ -367,17 +368,17 @@ sub compare_island_lists () {
 		next;
 		# We check arches of non-new islands above
 	    }
-	    change("new island in $wiarch: $island");
+	    change("island new in $wiarch: $island");
 	}
     }
 }
 
 sub shortest_path_reduction ($$) {
-    my ($what,$base) = @_;
+    my ($what,$g) = @_;
     #
-    # Takes a graph $base (and a string for messages $what) and returns
+    # Takes a graph $g (and a string for messages $what) and returns
     # a new graph which is the miminal shortest path transient reduction
-    # of $base.
+    # of $g.
     #
     # We also check that the shortest path closure of the intended result
     # is the same graph as the input.  Thus the input must itself be
@@ -387,15 +388,16 @@ sub shortest_path_reduction ($$) {
 
     Premises and definitions:
 
-    1. F is a connected undirected weighted graph with positive edge
-       weights.
+    1. F is an undirected weighted graph with positive edge weights.
 
     2. All graphs we will consider have the same vertices as F.
 
-    3. G = Closure(F) is the complete graph whose edge weights
-       are the shortest paths in F.  (G is the input graph $base.)
+    3. G = Closure(F) is the graph of cliques whose edge weights
+       are the shortest paths in F, one clique for each connected
+       component in F.
 
     3a. |XY| for vertices X, Y is the weight of the edge XY in G.
+       If XY is not in G, |XY| is infinite.
 
     4. A `reduction' of G is a subgraph K of G such that Closure(K) = G.
        The reduction is `minimal' if there is no strict subgraph K'
@@ -441,20 +443,20 @@ sub shortest_path_reduction ($$) {
 
 END
     
-    printf DEBUG "spr %s before %d\n", $what, scalar($base->edges());
+    printf DEBUG "spr %s before %d\n", $what, scalar($g->edges());
 
     my $result= Graph::Undirected->new();
-    foreach my $edge_ac ($base->edges()) {
-	my $edgename_ac= join '..', @$edge_ac;
+    foreach my $edge_ac ($g->edges()) {
+	my $edgename_ac= join ' .. ', @$edge_ac;
 	printf DEBUG "spr %s edge %s\n", $what, $edgename_ac;
-	my $w_ac= $base->get_edge_weight(@$edge_ac);
+	my $w_ac= $g->get_edge_weight(@$edge_ac);
 	my $needed= 1;
-	foreach my $vertex_b ($base->vertices()) {
+	foreach my $vertex_b ($g->vertices()) {
 	    next if grep { $_ eq $vertex_b } @$edge_ac;
-	    my $w_ab= $base->get_edge_weight($edge_ac->[0], $vertex_b);
+	    my $w_ab= $g->get_edge_weight($edge_ac->[0], $vertex_b);
 	    next unless defined $w_ab;
 	    next if $w_ab >= $w_ac;
-	    my $w_bc= $base->get_edge_weight($vertex_b, $edge_ac->[1]);
+	    my $w_bc= $g->get_edge_weight($vertex_b, $edge_ac->[1]);
 	    next unless defined $w_ac;
 	    next if $w_ab + $w_bc > $w_ac;
 	    # found path
@@ -471,13 +473,14 @@ END
     printf DEBUG "spr %s result %d\n", $what, scalar($result->edges());
 
     my $apsp= $result->APSP_Floyd_Warshall();
-    foreach my $ia (sort $base->vertices()) {
-	foreach my $ib (sort $base->vertices()) {
-	    my $din= $base->get_edge_weight($ia,$ib);
+    foreach my $ia (sort $g->vertices()) {
+	foreach my $ib (sort $g->vertices()) {
+	    my $din= $g->get_edge_weight($ia,$ib);
 	    my $dout= $apsp->path_length($ia,$ib);
 	    $din= defined($din) ? $din : 'infinity';
 	    $dout= defined($dout) ? $dout : 'infinity';
-	    error("$what spr apsp discrepancy in=$din out=$dout for $ia..$ib")
+	    error("$what spr apsp discrepancy in=$din out=$dout".
+                  " for $ia .. $ib")
 		if $din != $dout;
 	}
     }
@@ -507,13 +510,13 @@ sub compare_distances () {
 	    next unless defined $dbdist || defined $widist;
 	    
 	    if (!defined $widist) {
-		warning(sprintf "route delete %2d for %s..%s",
+		warning(sprintf "route delete %2d for %s .. %s",
 			$dbdist, $ia,$ib);
 	    } elsif (!defined $dbdist) {
-		change(sprintf "route create %2d for %s..%s",
+		change(sprintf "route new %2d for %s .. %s",
 		       $widist, $ia,$ib);
 	    } elsif ($dbdist != $widist) {
-		change(sprintf "route change %2d to %2d for %s..%s",
+		change(sprintf "route change %2d to %2d for %s .. %s",
 		       $dbdist, $widist, $ia,$ib);
 	    }
 	}
@@ -522,27 +525,25 @@ sub compare_distances () {
 
 parse_info_serverside();
 
-print "reading database\n";
+progress("reading database");
 
 db_setocean($ocean);
 db_connect();
 database_fetch_ocean();
 
-print "computing database spr\n";         database_graph_spr();
+progress("computing database spr");         database_graph_spr();
 
-print "reading yppedia chart\n";          yppedia_chart_parse();
-print "adding shortcuts\n";               yppedia_graphs_add_shortcuts();
-print "pruning boring vertices\n";        yppedia_graphs_prune_boring();
-print "checking yppedia graphs\n";        yppedia_graphs_check();
-print "setting archs from source-info\n"; yppedia_archs_sourceinfo();
-print "computing shortest paths\n";       yppedia_graph_shortest_paths();
-print "setting archs from labels\n";      yppedia_archs_chart_labels();
-print "setting archs from nearby\n";      yppedia_archs_fillbynearest();
-print "computing yppedia spr\n";          yppedia_graph_spr();
+progress("reading yppedia chart");          yppedia_chart_parse();
+progress("adding shortcuts");               yppedia_graphs_add_shortcuts();
+progress("pruning boring vertices");        yppedia_graphs_prune_boring();
+progress("checking yppedia graphs");        yppedia_graphs_check();
+progress("setting archs from source-info"); yppedia_archs_sourceinfo();
+progress("computing shortest paths");       yppedia_graph_shortest_paths();
+progress("setting archs from labels");      yppedia_archs_chart_labels();
+progress("setting archs from nearby");      yppedia_archs_fillbynearest();
+progress("computing yppedia spr");          yppedia_graph_spr();
 
-print "comparing\n";
-
-compare_island_lists();
-compare_distances();
+progress("comparing islands");              compare_island_lists();
+progress("comparing distances");            compare_distances();
 
 print_messages();