From: Claudio Sacerdoti Coen 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("\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("\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("\n\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 = "\n"; - if ($mark == 1) { - print "$elem removed\n"; - $response->content("$xml_header\n"); - } elsif ($mark == -1) { + if (!defined($elem)) { + print "is now empty\n"; + $response->content("$xml_header\n"); + } elsif ($mark == 1) { print "$elem (marked) removed\n"; $response->content("$xml_header\n"); } else { - print "is now empty\n"; - $response->content("$xml_header\n"); + print "$elem removed\n"; + $response->content("$xml_header\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("\n\n"); $response->content_type('text/xml');