+ \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
+
+ The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
+ different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
+ Each actor present one or more \ws{} interface to its neighbours \hbugs{}
+ actors.
+
+ In this section we will detail the role and requiremente of each kind of
+ actors and discuss about the correspondencies between them and the MONET
+ entities described in \cite{MONET-Overview}.
+
+ \paragraph{Clients}
+ An \hbugs{} client is a software component able to produce \emph{proof
+ status} and to consume \emph{hints}.
+
+ \ednote{"status" ha il plurale?}
+ 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 requirement exists on the proof status, but there should be an
+ agreement on its format between clients and tutors. An hint is a
+ representation of a step that can be performed in order to proceed in an
+ incomplete proof. Usually it represents a tactic available on some proof
+ assistant along with instantiation of its parameters for tactics which
+ require them.
+
+ Clients act both as \ws{} provider and requester (using W3C's terminology
+ \cite{ws-glossary}). They act as providers for the broker (to receive hints)
+ ans as requesters again for the broker (to submit new status). Clients
+ additionally use broker service to know which tutors are available and to
+ subscribe to one or more of them.
+
+ Usually, when the role of client is taken by an interactive proof assistant,
+ new status are sent to the broker as soon as the proof change (e.g. when the
+ user applies a tactic or when a new proof is started) and hints are shown to
+ the user be the means of some effect in the user interface (e.g. popping a
+ dialog box or enlightening a tactic button).
+
+ \hbugs{} clients act as MONET clients and ask broker to provide access to a
+ set of services (the tutors). \hbugs{} has no actors corresponding to MONET's
+ Broker Locating Service (since the client is supposed to know the URI of at
+ least one broker) and Mathematical Object Manager (since proof status are
+ built on the fly and not stored).
+
+ \paragraph{Brokers}
+ \hbugs{} brokers are the key actors of the \hbugs{} architecture since they
+ act as intermediaries between clients and tutors. They act both as \ws{}
+ provider and requester \emph{both} for clients and tutors.
+
+ With respect to client, a broker act as \ws{} provider receiving status and
+ forwarding them to one or more tutors. They act as \ws{} requester sending
+ hints to client as soon as they are available from tutors.
+
+ With respect to tutors, the \ws{} provider role is accomplished by receiving
+ hints as soon as they are produced; the \ws{} requester one is accomplished
+ by requesting computations (\emph{musings} in \hbugs{} terminology) on status
+ received by clients and stopping out of date ongoing musings.
+
+ Additionally brokers keep track of available tutors and subscription of each
+ client.
+
+ \hbugs{} brokers act as MONET brokers implementing the following components:
+ Client Manager, Service Registry Manager (keeping track of available
+ tutors), Planning Manager (chosing the available tutors among the ones to
+ which the client is subscribed), Execution Manager. \ednote{non e' chiaro se
+ in monet le risposte siano sincrone o meno, se cosi' fosse dobbiamo
+ specificare che nel nostro caso non lo sono}
+
+ \paragraph{Tutors}
+ Tutors are software component able to consume proof status producing hints.
+ \hbugs{} doesn't specify by which means hints should be produced, tutors can
+ use any means necessary (heuristics, external theorem prover or CAS, ...).
+ The only requirement is that exists an agreement on the formats of proof
+ status and hints.
+
+ tutors act both as \ws{} providers and requesters for broker. As providers,
+ they wait for commands requesting to start a new musing on a given proof
+ status or to stop an old, out of date, musing. As requesters, they signal to
+ the broker the end of a musing along with its outcome (an hint in case of
+ success or a notification of failure).
+
+ \hbugs{} tutors act as MONET services.