From: Stefano Zacchiroli Date: Fri, 23 May 2003 11:11:42 +0000 (+0000) Subject: - (badly) written section 2 (Architecture) X-Git-Tag: submitted~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3fc483b35a97067f72a32663dda60d92fd8de3d7 - (badly) written section 2 (Architecture) - removed old oldparts in introduction, added some ednotes --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 1cd791f83..bd1a64768 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -8,7 +8,7 @@ \newcommand{\myincludegraphics}[5]{ \begin{figure}[#2] \begin{center} - \includegraphics[width=#3]{XFIG-EPS/#1.eps} + \includegraphics[width=#3]{eps/#1.eps} \caption[#4]{#5} \label{#1} \end{center} @@ -71,55 +71,29 @@ of applications working on machine-understandable XML documents both for input and output. -\oldpart -{Di effetto la prima fase. La seconda era troppo fuori-tema e dettagliata per - un abstract} -{ - This lack of organization along with the huge amount of documents available, - have posed not a few problems for data location. If this limitation could be - overcome using heuristic-based search engine for HTML pages, a satisfying - solution has yet to be found for \ws{} location \ednote{location non mi piace, ma - "localization" e' anche peggio, "retrieval"?}. A promising architecture seems - to be the use of \emph{brokers}, which access point (usually an URI) is known - by the potential clients or by \emph{registries}, to which the \wss{} subscribe - to publish their functionalities. -} -\begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale -dovrebbe essere una versione pi\'u fluida e leggera. Boh.} -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 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. + 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 + 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. -Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET}, -following the guidelines of the \wss{}/brokers approach, is -\end{newpart} - working on the development of a framework aimed at providing a set of software - tools for the advertisement and discovering of mathematical web services. -%CSC This framework turns out to be strongly based on both \wss{} and brokers. -\oldpart -{Hhhmm. Chiaro il punto, ma CAS and Theorem Prover related web-services non - \'e molto preciso.} -{ - Several examples of CAS (Computer Algebra System) and Theorem Prover related - \wss{} have been shown to be useful and to fit well in the MONET Architecture - \ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?} - the set of \wss{} related to Proof Assistants tends to be ... rather ... - empty!\ednote{gia' mi immagino il tuo commento: BUHM! :-)} -} -\begin{newpart}{riformulo} - Several groups have already developed \wss{} providing both computational - and reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori - carini dalle conferenze calculemus}: the formers are implemented - on top of Computer Algebra Systems; the latters provide interfaces to - well-known theorem provers. Proof-planners, proof-assistants, CAS and - domain-specific problem solvers are natural candidates to be client - of these services. Nevertheless, so far the number of examples in the - literature has been extremely low and the concrete benefits are still - to be assessed.\ednote{A questo punto bisogna venire al - sodo prima che il lettore passi al caff\'e} -\end{newpart} + Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET}, + following the guidelines \ednote{guidelines non e' molto appropriato, dato che + il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers + approach, is working on the development of a framework aimed at providing a + set of software tools for the advertisement and discovering of mathematical + web services. + %CSC This framework turns out to be strongly based on both \wss{} and brokers. + + Several groups have already developed \wss{} providing both computational and + reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini + dalle conferenze calculemus}: the first ones are implemented on top of + Computer Algebra Systems; the last ones provide interfaces to well-known + theorem provers. Proof-planners, proof-assistants, CAS themselves and + domain-specific problem solvers are natural candidates to be client of these + services. Nevertheless, so far the number of examples in the literature has + been extremely low and the concrete benefits are still to be assessed. In this paper we present an architecture, namely \hbugs{}, implementing a \emph{suggestion engine} for the proof assistant developed on behalf of the @@ -145,7 +119,10 @@ following the guidelines of the \wss{}/brokers approach, is As usual, the paper ends with the conclusions and future works. \oldpart -{Non so se/dove mettere queste parti} +{CSC: Non so se/dove mettere queste parti. + Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte + non e' molto utile, ma la seconda sugli usi tipici di proof assistant + come ws client si} { Despite of that the proof assistant case seems to be well suited to investigate the usage of many different mathematical \wss{}. Indeed: most proof @@ -160,8 +137,89 @@ following the guidelines of the \wss{}/brokers approach, is domain. } -\section{???} +\section{Architecture} \label{architecture} + \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. \section{???} \label{implementation}