]> matita.cs.unibo.it Git - helm.git/commitdiff
Several editor notes resolved.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 17:48:22 +0000 (17:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 29 May 2003 17:48:22 +0000 (17:48 +0000)
helm/papers/calculemus-2003/hbugs-calculemus-2003.tex

index 723d21dd1c5e627e6126bcd420e011a6b6b5c069..49322ba2e7f0eebc3e15cd01a5f8e897f5c19b20 100644 (file)
@@ -75,7 +75,7 @@
   
   The big challenge for the next future is to provide stable and reliable
   services over this disorganized, unreliable and ever-evolving architecture.
-  The standard solution \ednote{zack: buhm! :-P} is providing a further level of
+  The standard solution is providing a further level of
   stable services (called \emph{brokers}) that behave as common gateway/address
   for client applications to access a wide variety of services and abstract over
   them.
   \Omegapp{} proof-planner \cite{omega}. The main architectural difference
   between \hbugs{} and \OmegaAnts{} are that the latter is based on a
   black-board architecture and it is not implemented using \wss{} and
-  brokers. Other differences will be detailed in Sect. \ref{conclusions}
-  \ednote{CSC: che si fa di sta frase?}.
+  brokers.
 
   In Sect. \ref{architecture} we present the architecture of \hbugs{}.
   Further implementation details are given in Sect. \ref{implementation}.
     A proof status is a representation of an incomplete proof and is supposed to
     be informative enough to be used by an interactive proof assistant. No
     additional requirements exist on the proof status, but there should be an
-    agreement on its format between clients and tutors. An hint is a
-    representation\ednote{CSC: non c'\'e un sinonimo pi\'u carino? Zack: l'unico
-    decente sembra essere nuovamente "suggestion". CSC: chiamalo sinonimo!}
-    of a step that can be performed in order to proceed in an
+    agreement on its format between clients and tutors. An hint is an
+    encoding of a step that can be performed in order to proceed in an
     incomplete proof. Usually it represents a reference to a tactic available
     on some proof assistant along with an instantiation for its formal
     parameters. More structured hints can also be used: an hint can be
     hints as soon as they are produced; as a requester, it is accomplished
     by asking for computations (\emph{musings} in \hbugs{} terminology) on
     status received by clients and by stopping already late but still
-    ongoing \musings{}
-    \ednote{Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo
-    commento sulla utilita'/quantita' delle figure ... CSC: vanno benissimo}
+    ongoing \musings{}.
 
     Additionally brokers keep track of available tutors and clients
     subscriptions.
     the broker instead of being received from the service when it is
     initialized. In particular, a session is identified by an unique identifier
     for the client (its URL) and an unique identifier for the broker (its
-    URL).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i
-    multi-sessione. Ma mi sembra la strada che prenderemmo, no?}
+    URL).
 
     The MONET architecture specification does not state explicitly whether
     the service and broker answers can be asynchronous. Nevertheless, the
@@ -384,7 +378,7 @@ the \hbugs{} architecture.
     has unsubscribed), the broker is able to decide to which tutors the
     new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
     della possibilit\'a di avere un vero brocker che multiplexi le richieste
-    del tutor localizzando i servizi, etc.}
+    dei client localizzando i servizi, etc.}
 
     The forwarding operation is performed using the \texttt{Start\_musing}
     method of the tutors, that is a request to start a new computation
@@ -401,17 +395,14 @@ the \hbugs{} architecture.
     inform him and the \texttt{Musing\_completed} method is called
     just to update the \musings{} registry.
 
-    Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
-    stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
-    ovviamente ... CSC: ma a che serve???} is able to know, at each time,
-    which \musings{} are in execution on which tutor. This peculiarity is
+    Consulting the \musings{} registry, the broker is able to know, at each
+    time, which \musings{} are in execution on which tutor. This peculiarity is
     exploited by the broker on invocation of Status method. Receiving a new
     status from the client implies indeed that the previous status no longer
     exists and all \musings{} working on it should be stopped: additionally to
     the already described behavior (i.e. starting new \musings{} on the
-    received status), the tutor\ednote{CSC: Ma sei veramente veramente sicuro?}
-    takes also care of stopping ongoing computation invoking
-    \texttt{Stop\_musing} tutors' method.
+    received status), the broker takes also care of stopping ongoing
+    computation invoking \texttt{Stop\_musing} tutors' method.
 
   \paragraph{\wss{}}
     As already discussed, all \hbugs{} actors act as \wss{} offering one or more