From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Oct 2001 12:03:05 +0000 (+0000)
Subject: New implementation: now the number of nodes is used to prune the graph
X-Git-Tag: v0_1_3~74
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f01ce40bc7c19da0a220a9899019074acf94ff8;p=helm.git

New implementation: now the number of nodes is used to prune the graph
---

diff --git a/helm/graphs/tools/mk_html.pl b/helm/graphs/tools/mk_html.pl
index 5c1daa5b8..b98e38de1 100755
--- a/helm/graphs/tools/mk_html.pl
+++ b/helm/graphs/tools/mk_html.pl
@@ -107,7 +107,7 @@ EOT
    var iurl = unescape(getParam("url"));
    var getterURL = getParam3(iurl,"param.getterURL");
    var interfaceURL = unescape(getParam3(iurl,"param.interfaceURL"));
-   var url = setParam(iurl,"keys","d_c%2CC1%2CHC2%2CL");
+   var url = setParam(iurl,"keys",getParam3(iurl,"param.keys"));
    url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D$uri");
    url = setParam(url,"param.CICURI","$uri");
    url = setParam(url,"param.RDFURI","helm:rdf:www.cs.unibo.it/helm/rdf/rdfprova//$uri");
diff --git a/helm/graphs/tools/uri_set_queue.cgi b/helm/graphs/tools/uri_set_queue.cgi
index 4c6651528..6c6baf096 100755
--- a/helm/graphs/tools/uri_set_queue.cgi
+++ b/helm/graphs/tools/uri_set_queue.cgi
@@ -12,14 +12,15 @@ $SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes
 
 my %uri_sets;
 my %uri_queues;
+my %overflowed;
+my %size;
 
-#NOT REENTRANT: CAN NOT FORK DUE TO THE GLOBAL VARIABLES %uri_sets & %uri_queues
+#NOT REENTRANT: CAN NOT FORK DUE TO THE GLOBAL VARIABLES %uri_sets & ...
 #HENCE, THE "PID" ARGUMENT OF EVERY REQUEST MUST IDENTIFY THE SET OF URI
 #IT WANTS TO WORK WITH. MOREOVER, EVERY CLIENT MUST WORK WITH A DIFFERENT SET
 #OF URI, I.E. EVERY PID MUST BE UNIQUE.
 
 #CSC: WHAT IF THE CLIENTS ARE ON DIFFERENT MACHINES AND HAVE THE SAME PID?
-#CSC: CGI MODULE REQUIRED TO PROCESS PARAMETERS BETTER
 
 while (my $c = $d->accept) {
     while (my $r = $c->get_request) {
@@ -32,14 +33,14 @@ while (my $c = $d->accept) {
             print(@{$uri_queues{$pid}} + 0);
             print "/";
             my $tot = keys(%{$uri_sets{$pid}}) + 0;
+            $tot .= "*" if defined($overflowed{$pid});
 	    print "$tot $uri: ";
 
             my $res;
 	    if (!(defined($uri_sets{$pid}->{$uri}))) {
-                if ($tot + 1 > 20) {
-	           $uri_sets{$pid}->{$uri} = -1;
-                   push @{$uri_queues{$pid}},$uri;
-                   $res = "added_with_mark";
+                if ($tot + 1 > $size{$pid}) {
+                   $res = "not_added_because_already_too_many";
+                   $overflowed{$pid} = 1;
                 } else {
 	           $uri_sets{$pid}->{$uri} = 1;
                    push @{$uri_queues{$pid}},$uri;
@@ -54,6 +55,32 @@ while (my $c = $d->accept) {
             $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
 	    $response->content_type('text/xml');
             $c->send_response($response);
+        } elsif ($r->method eq 'GET' and $r->url->path eq '/is_overflowed') {
+            my $http_query = $r->url->equery;
+            my $cgi = new CGI("$http_query");
+            my $pid = $cgi->param('PID');
+	    print "$pid: ";
+            print(@{$uri_queues{$pid}} + 0);
+            print "/";
+	    print(keys(%{$uri_sets{$pid}}) + 0);
+            print "*" if defined($overflowed{$pid});
+            my $res = defined($overflowed{$pid}) ? "true" : "false";
+            print " is_overflowed: $res\n";
+	    my $response = new HTTP::Response;
+            $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
+	    $response->content_type('text/xml');
+            $c->send_response($response);
+        } elsif ($r->method eq 'GET' and $r->url->path eq '/set_uri_set_size') {
+            my $http_query = $r->url->equery;
+            my $cgi = new CGI("$http_query");
+            my $pid = $cgi->param('PID');
+            my $size = $cgi->param('size');
+	    print "$pid: size := $size\n";
+            $size{$pid} = $size;
+	    my $response = new HTTP::Response;
+            $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
+	    $response->content_type('text/xml');
+            $c->send_response($response);
         } elsif ($r->method eq 'GET' and $r->url->path eq '/get_next') {
             my $http_query = $r->url->equery;
             my $cgi = new CGI("$http_query");
@@ -62,22 +89,23 @@ while (my $c = $d->accept) {
             print(@{$uri_queues{$pid}} + 0);
             print "/";
 	    print(keys(%{$uri_sets{$pid}}) + 0);
+            print "*" if defined($overflowed{$pid});
             print " ";
 
             my $elem = shift @{$uri_queues{$pid}};
-            my $mark = $uri_sets{$pid}->{$elem};
+            my $mark = $overflowed{$pid};
 
 	    my $response = new HTTP::Response;
             my $xml_header = "<?xml version=\"1.0\"?>\n";
-            if ($mark == 1) {
-	       print "$elem removed\n";
-               $response->content("$xml_header<uri value=\"$elem\"/>\n");
-            } elsif ($mark == -1) {
+            if (!defined($elem)) {
+	       print "is now empty\n";
+               $response->content("$xml_header<empty/>\n");
+            } elsif ($mark == 1) {
 	       print "$elem (marked) removed\n";
                $response->content("$xml_header<marked_uri value=\"$elem\"/>\n");
             } else {
-	       print "is now empty\n";
-               $response->content("$xml_header<empty/>\n");
+	       print "$elem removed\n";
+               $response->content("$xml_header<uri value=\"$elem\"/>\n");
             }
 	    $response->content_type('text/xml');
             $c->send_response($response);
@@ -92,6 +120,8 @@ while (my $c = $d->accept) {
             }
 	    print "************\nThe URI set $pid is now empty again\n";
 	    delete($uri_sets{$pid});
+            delete($overflowed{$pid});
+            delete($size{$pid});
 	    my $response = new HTTP::Response;
             $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
 	    $response->content_type('text/xml');