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
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
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