]> matita.cs.unibo.it Git - helm.git/commitdiff
New implementation: now the number of nodes is used to prune the graph
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Oct 2001 12:03:05 +0000 (12:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Oct 2001 12:03:05 +0000 (12:03 +0000)
helm/graphs/tools/mk_html.pl
helm/graphs/tools/uri_set_queue.cgi

index 5c1daa5b87e2592b304af2de5a3071b542195cf3..b98e38de13af906ff681087dc09fc57e983ae6ba 100755 (executable)
@@ -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");
index 4c66515288a269f352bde72483c4cc25eb2e81aa..6c6baf096d60605a31683dbb58f461170b926f21 100755 (executable)
@@ -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');