agriesma@306
|
1 |
%nicht vergessen: auch srd.tex ($Revision $) \"andern !
|
akremp@767
|
2 |
\part{Software Requirements Document}
|
agriesma@306
|
3 |
|
agriesma@306
|
4 |
This Software Requirements Document is structured along the modules
|
agriesma@306
|
5 |
abstracted from the functionality defined in the User Requirements
|
agriesma@306
|
6 |
Document. The User Requirements Document, however, is structured along
|
agriesma@306
|
7 |
the different kinds of users envisaged. In order to establish
|
agriesma@306
|
8 |
comfortable tracing, the $m:n$ relation between user requirements and
|
agriesma@306
|
9 |
software requirements will be accurrately recorded in a double-linked
|
agriesma@306
|
10 |
way.
|
agriesma@306
|
11 |
|
akremp@767
|
12 |
\chapter{General requirements}
|
agriesma@306
|
13 |
%One goal of this section is to achieve a smooth design and minimize the effort in development. Although \sisac consists of a number of (more or less) autonomous modules, a number of developments can be shared.
|
agriesma@306
|
14 |
|
wneuper@2323
|
15 |
\section{Delopment environment,} standards and components, documentation and revision control are described in appendix \ref{AP:environment}.
|
agriesma@306
|
16 |
|
wneuper@1692
|
17 |
|
wneuper@2323
|
18 |
\section{Decisions for underlying systems} have been done already.
|
wneuper@1692
|
19 |
As this requirements document shows, \sisac{} is a large system: thus it cannot be done from scratch, rather is has to use as much as components already available. The theorem prover Isabelle provides for both, a comprehensive frontend for interactive deduction (i.e. for definitions, axioms and proving theorems), and a hughe mathematics knowledge base. Both are under rapid development, which \sisac{} shall take advantage of. The kernel of Isabelle, however is relatively stable already, and thus the interfaces to \sisac s math engine (ME) are sufficiently stable.
|
wneuper@1692
|
20 |
{\bf\SR The deductive part is left to Isabelle. \label{deduct-isa}}
|
wneuper@1692
|
21 |
{\bf\SR \sisac s math engine closely cooperates with Isabelle \label{me-isa}\\}
|
wneuper@1692
|
22 |
Thus the math engine is already implemented in the same program language as Isabelle, SML.
|
wneuper@1692
|
23 |
|
wneuper@1692
|
24 |
%dropped: visitor canNOT calculate !
|
wneuper@1692
|
25 |
%
|
wneuper@1692
|
26 |
%\subparagraph{The call hierarchy} between the components underlies a severe restriction due to UR \ref{access-ab} and UR \ref{isac-www}: Because a browser can only deliver a HTTP-request, the worksheet must start browsers, too (and not only the dialog, as it would be desirable w.r.t. the system architecture).
|
wneuper@1692
|
27 |
%{\bf\SR Browsers are called by a 'master-browser' {\em and} by the worksheet. \label{}} ??? %WN2.12.02 ...... ausbessern !!!!
|
agriesma@306
|
28 |
|
wneuper@2323
|
29 |
\section{The connection between Java and SML} has to be 'hand-made'. During the next few years there will be several changes at the interfaces between the
|
agriesma@306
|
30 |
\sisac-components belonging to these two language environments.
|
agriesma@306
|
31 |
{\bf\SR The SML-kernel is started by a java thread \label{}} which controls the time-out eventuall resulting from non-terminating loops in the knowledge interpreter.
|
agriesma@306
|
32 |
{\bf\SR The SML standard-output channel is read by parsers, \label{}} one for the SML-structures, and one for the mathematics formulas embedded in the SML-structures.
|
agriesma@306
|
33 |
|
wneuper@2323
|
34 |
\section{System requirements for the users:} Users (with exception of the math authors, which work directly on the SML-kernel) are expected to work on standard-browsers (UR \ref{browser}) and some additional software components.
|
agriesma@306
|
35 |
{\bf\SR On the client-side a Java virtual machine version .... \label{}} must reside on the local computer of the learners and authors.
|
agriesma@306
|
36 |
{\bf\SR On the server there is a Linux or Unix \label{}} operating system, Linux version ..., Unix ...
|
agriesma@306
|
37 |
|
wneuper@2323
|
38 |
\section{Communication in the distributed system}
|
wneuper@2323
|
39 |
%WN050518---AK.p.58-61->isac-SRD--------BEGIN---please don't remove this line
|
wneuper@2323
|
40 |
\footnote{Begin of copy from \cite{AK04:thesis} p.58-61.}
|
wneuper@2323
|
41 |
\subsection{Choosing a Means of Communication}\label{AK:DESIGN:SYSTEM:DISTRIBUTE:comm}
|
wneuper@2323
|
42 |
|
wneuper@2323
|
43 |
For integration of the various components across several machines an off-the-shelf solution was sought with the following criteria in mind:
|
wneuper@2323
|
44 |
|
wneuper@2323
|
45 |
\begin{description}
|
wneuper@2323
|
46 |
\item[Speed] Many of the user's requests originating on the Worksheet require processing in the Math Engine. With \isac{} being an interactive system, we need response times near the response times in normal human interaction.
|
wneuper@2323
|
47 |
\item[Security] With many of the features of \isac{} depending on the identity of the user and the enforcement of access rights, basic security features are a necessity.
|
wneuper@2323
|
48 |
\item[Mobility] Users might want to use \isac{} at work, in class or at home, even on computers they use only occasionally. This asks for communication robust against changing addresses of client and server computers, but still secure.
|
wneuper@2323
|
49 |
\item[Conformity to Standards] is especially important for the Worksheet, which runs on the user's machine. An ideal solution would build on standard resources available on the user's machine without the need of additional installation. If installation is required, it must be kept as simple as possible.
|
wneuper@2323
|
50 |
|
wneuper@2323
|
51 |
With the goal of being open to cooperation with the tools of other projects, a standard solution would ease integration of the different systems.
|
wneuper@2323
|
52 |
|
wneuper@2323
|
53 |
In addition to that, a standard solution is preferred with the limited resources of the \isac{} project in mind.
|
wneuper@2323
|
54 |
|
wneuper@2323
|
55 |
\end{description}
|
wneuper@2323
|
56 |
|
wneuper@2323
|
57 |
Several options were reviewed to find a suitable means of communication, among them Java-RMI \footnote{http://java.sun.com/products/jdk/rmi/}, XML-RPC \footnote{http://www.xmlrpc.com/spec}, SOAP \footnote{http://www.w3.org/TR/SOAP} and Dinopolis \footnote{http://www.dinopolis.org/}.
|
wneuper@2323
|
58 |
|
wneuper@2323
|
59 |
While the Dinopolis approach looked most promising with respect to the aforementioned criteria, it was not yet available in a stable implementation.
|
wneuper@2323
|
60 |
Java-RMI was chosen for the implementation of the \isac{} prototype. The strongest arguments for Java-RMI were the seamless integration into the Java programming environment and the widespread use and accepted stability.
|
wneuper@2323
|
61 |
|
wneuper@2323
|
62 |
\subsection{The Dinopolis Middleware project}\label{AK:DESIGN:SYSTEM:DISTRIBUTE:dino}
|
wneuper@2323
|
63 |
% pl: Wie schon in meiner e-mail bemerkt, sollten Sie hier lieber Java-RMI
|
wneuper@2323
|
64 |
% skizzieren, das Sie benutzen und nicht Dinopolis, das Sie nicht benuetzen.
|
wneuper@2323
|
65 |
Dinopolis \cite{dino2002} is an object management middleware system aiming at object and component retrieval, security and run-time polymorphism. While not part of the current implementation of \isac{}, Dinopolis still played an important role during the design phase.
|
wneuper@2323
|
66 |
|
wneuper@2323
|
67 |
The main features of Dinopolis include:
|
wneuper@2323
|
68 |
\begin{description}
|
wneuper@2323
|
69 |
|
wneuper@2323
|
70 |
\item[Component and object management]
|
wneuper@2323
|
71 |
Extending the traditional data-and-operations view, Dinopolis objects have the following aspects, all handled by the middleware:
|
wneuper@2323
|
72 |
\begin{description}
|
wneuper@2323
|
73 |
\item[Content] is the traditional data content.
|
wneuper@2323
|
74 |
\item[Meta-Data] can be used for administrative purposes which are not necessarily reflected by the content.
|
wneuper@2323
|
75 |
\item[Interrelations] associate several objects, of equal or different types, in a m:n manner.
|
wneuper@2323
|
76 |
\item[Operations] manipulate the content of an object.
|
wneuper@2323
|
77 |
\item[Services] are GUI building blocks offered by an object to facilitate data manipulation by the user. Services can be viewed as the View and Controller parts of a MVC triple.
|
wneuper@2323
|
78 |
\end{description}
|
wneuper@2323
|
79 |
All of these aspects are handled transparently by the Dinopolis middleware according to the current run-time context, which not only takes burden from the programmer, but also allows for run-time dynamic typing as a key feature.
|
wneuper@2323
|
80 |
|
wneuper@2323
|
81 |
Objects and components are accessed through Globally Unique Handles (GUH), a mechanism allowing for unambiguous retrieval of objects independent of their physical locations \cite{DOLSA}.
|
wneuper@2323
|
82 |
|
wneuper@2323
|
83 |
\item[Role-based security]
|
wneuper@2323
|
84 |
Dinopolis takes control over access to components, objects, their data and operations. Access control is based on the user and his role as opposed to the user's identity alone. With Dinopolis, the same user would have different access rights and therefore see different aspects and different behaviour of objects depending on whether he accesses \isac{} as administrator, teacher or student. All security-relevant operations are handled transparently by the Dinopolis middleware, so the only task left to \isac{} is to identify the user. As far as objects are concerned, the transparent security system may be considered a special case of dynamic typing described above.
|
wneuper@2323
|
85 |
|
wneuper@2323
|
86 |
\item[Ability to embed existing systems]
|
wneuper@2323
|
87 |
Existing systems can easily be integrated into Dinopolis by writing embedders for existing objects such as databases. This could ease integrating \isac{} with other projects without the need to define common data structures. In addition to that, the SML part of \isac{} could easily be integrated this way.
|
wneuper@2323
|
88 |
|
wneuper@2323
|
89 |
\item[Platform-independency]
|
wneuper@2323
|
90 |
At present, Dinopolis is being implemented in C++ and Java, but the protocols and algorithms are open to arbitrary programming languages.
|
wneuper@2323
|
91 |
|
wneuper@2323
|
92 |
\end{description}
|
wneuper@2323
|
93 |
|
wneuper@2323
|
94 |
The features mentioned above make Dinopolis ideally suited for the needs of \isac{}, for communication of the various distributed components as well as for security and role-dependent behaviour of the system. Unfortunately, Dinopolis is still being developed and was not finished in time to base the current prototype of \isac{} on. The \isac{} team still hope to use the features of Dinopolis in future versions.
|
wneuper@2323
|
95 |
|
wneuper@2323
|
96 |
\subsection{Java-RMI}\label{AK:DESIGN:SYSTEM:DISTRIBUTE:rmi}
|
wneuper@2323
|
97 |
Java Remote Method Invocation provides for communication of processes running in different Virtual Machines, even if the VMs run on different computers. Basically, RMI provides invoking methods on remote objects and passing parameters to remote methods. RMI cannot be compared directly to Dinopolis, because RMI's purpose is communication between remote objects, but not object retrieval, system security or dynamic typing.
|
wneuper@2323
|
98 |
|
wneuper@2323
|
99 |
To invoke methods on a remote object, the remote object has to implement a public remote interface extending \texttt{java.rmi.Remote}. Every method in the remote interface has to declare to throw \texttt{RemoteException}. The remote object may implement other methods in addition to the remote interface, but only the methods in the remote interface can be invoked remotely.
|
wneuper@2323
|
100 |
|
wneuper@2323
|
101 |
Any objects implementing the \texttt{java.io.Serializable} interface can be passed as parameter. Unlike other distributed component systems, this is the only condition imposed on parameters.
|
wneuper@2323
|
102 |
|
wneuper@2323
|
103 |
Apart from the non-restrictive conditions listed, remote objects can be used like local objects once a connection is established.
|
wneuper@2323
|
104 |
|
wneuper@2323
|
105 |
This tight integration into the Java programming environment is the key advantage of Java-RMI and one of its few drawbacks, as it is limited to Java as a programming language.
|
wneuper@2365
|
106 |
|
wneuper@2323
|
107 |
\footnote{End of copy from \cite{AK04:thesis} p.58-61.}
|
wneuper@2323
|
108 |
%WN050518---AK.p.58-61->isac-SRD--------END---please don't remove this line
|
agriesma@306
|
109 |
|
wneuper@3881
|
110 |
\begin{verbatim}
|
wneuper@3881
|
111 |
|
wneuper@3881
|
112 |
-------- Original Message --------
|
wneuper@3881
|
113 |
Subject: Re: RK noch eine Bitte
|
wneuper@3881
|
114 |
Date: Thu, 31 May 2007 18:56:28 +0200
|
wneuper@3881
|
115 |
From: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@3881
|
116 |
To: isac@ist.tugraz.at
|
wneuper@3881
|
117 |
References: <465DA1BD.506@ist.tugraz.at> <465DECBF.5030607@sbox.tugraz.at> <465EE077.9000504@ist.tugraz.at> <20070531175410.b9zz0p64g00cckgo@webmail.tugraz.at>
|
wneuper@3881
|
118 |
|
wneuper@3881
|
119 |
Robert Könighofer wrote:
|
wneuper@3881
|
120 |
> Zitat von Walther Neuper <neuper@ist.tugraz.at>:
|
wneuper@3881
|
121 |
>
|
wneuper@3881
|
122 |
>> _noch_ eine Frage zu Eurer, Deiner und Nelles, Arbeit an der HTL: laut
|
wneuper@3881
|
123 |
>>
|
wneuper@3881
|
124 |
>> http://java.sun.com/developer/onlineTraining/rmi/RMI.html
|
wneuper@3881
|
125 |
>>
|
wneuper@3881
|
126 |
>> sollte RMI bei Firewallproblemen _automatisch_ auf http-tunneling
|
wneuper@3881
|
127 |
>> schalten (..it is blocked by the firewall. When this happens, the RMI
|
wneuper@3881
|
128 |
>> transport layer automatically retries by encapsulating the JRMP call
|
wneuper@3881
|
129 |
>> data within an HTTP POST request. etc..)
|
wneuper@3881
|
130 |
>>
|
wneuper@3881
|
131 |
>> Habt Ihr bei Eurer Arbeit davon bemerkt ?
|
wneuper@3881
|
132 |
>
|
wneuper@3881
|
133 |
> Nein, leider.
|
wneuper@3881
|
134 |
>
|
wneuper@3881
|
135 |
Ah, sehr interessant, dass das nicht so läuft ...
|
wneuper@3881
|
136 |
|
wneuper@3881
|
137 |
> Die einleitenden Worte würden schon irgendwie darauf hindeuten, dass das
|
wneuper@3881
|
138 |
> alles automatisch passiert. Davon haben wir allerdings leider nichts
|
wneuper@3881
|
139 |
> bemerkt. Vielleicht haben wir uns dieses feature auch unabsichtlich
|
wneuper@3881
|
140 |
> selbst deaktiviert, als wir anstelle der Default Sockets zur
|
wneuper@3881
|
141 |
> Kommunikation unsere eigenen Sockets mit fixierten Ports aktiviert haben.
|
wneuper@3881
|
142 |
>
|
wneuper@3881
|
143 |
?!?!?
|
wneuper@3881
|
144 |
> [...]
|
wneuper@3881
|
145 |
> "If a client is behind a firewall, it is important that you also set the
|
wneuper@3881
|
146 |
> system property http.proxyHost appropriately. Since almost all firewalls
|
wneuper@3881
|
147 |
> recognize the HTTP protocol, the specified proxy server should be able
|
wneuper@3881
|
148 |
> to forward the call directly to the port on which the remote server is
|
wneuper@3881
|
149 |
> listening on the outside."
|
wneuper@3881
|
150 |
>
|
wneuper@3881
|
151 |
... das gilt für die Firewall auf der Serverseite; wir brauchen aber nur
|
wneuper@3881
|
152 |
die Firewall auf der Clientseite beachten, da der isacserver am IST
|
wneuper@3881
|
153 |
_vor_ der Firewall (in der dmz) läuft !
|
wneuper@3881
|
154 |
|
wneuper@3881
|
155 |
> [...]
|
wneuper@3881
|
156 |
Vielleicht ist das Ganze einfacher, als wir denken !?!
|
wneuper@3881
|
157 |
>
|
wneuper@3881
|
158 |
> lg RK
|
wneuper@3881
|
159 |
>
|
wneuper@3881
|
160 |
lg Walther
|
wneuper@3881
|
161 |
--
|
wneuper@3881
|
162 |
------------------------------------------------------------------------
|
wneuper@3881
|
163 |
Walther Neuper Mailto: neuper@ist.tugraz.at
|
wneuper@3881
|
164 |
Institute for Software Technology Tel: +43-(0)316/873-5728
|
wneuper@3881
|
165 |
TUG University of Technology, Fax: +43-(0)316/873-5706
|
wneuper@3881
|
166 |
and HTL Ortweinschule, Graz, Austria Home: www.ist.tugraz.at/neuper
|
wneuper@3881
|
167 |
------------------------------------------------------------------------
|
wneuper@3881
|
168 |
|
wneuper@3881
|
169 |
|
wneuper@3881
|
170 |
|
wneuper@3881
|
171 |
-------- Original Message --------
|
wneuper@3881
|
172 |
Subject: Re: RK noch eine Bitte
|
wneuper@3881
|
173 |
Date: Fri, 01 Jun 2007 12:35:28 +0200
|
wneuper@3881
|
174 |
From: Nebojsa Simic <nelle@sbox.tugraz.at>
|
wneuper@3881
|
175 |
To: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@3881
|
176 |
References: <465DA1BD.506@ist.tugraz.at> <465DECBF.5030607@sbox.tugraz.at> <465EE077.9000504@ist.tugraz.at> <20070531175410.b9zz0p64g00cckgo@webmail.tugraz.at> <465EFE3C.5030502@ist.tugraz.at>
|
wneuper@3881
|
177 |
|
wneuper@3881
|
178 |
Quoting Walther Neuper <neuper@ist.tugraz.at>:
|
wneuper@3881
|
179 |
|
wneuper@3881
|
180 |
> Robert Könighofer wrote:
|
wneuper@3881
|
181 |
>> Zitat von Walther Neuper <neuper@ist.tugraz.at>:
|
wneuper@3881
|
182 |
>>
|
wneuper@3881
|
183 |
>>> _noch_ eine Frage zu Eurer, Deiner und Nelles, Arbeit an der HTL: laut
|
wneuper@3881
|
184 |
>>>
|
wneuper@3881
|
185 |
>>> http://java.sun.com/developer/onlineTraining/rmi/RMI.html
|
wneuper@3881
|
186 |
>>>
|
wneuper@3881
|
187 |
>>> sollte RMI bei Firewallproblemen _automatisch_ auf http-tunneling
|
wneuper@3881
|
188 |
>>> schalten (..it is blocked by the firewall. When this happens, the
|
wneuper@3881
|
189 |
>>> RMI transport layer automatically retries by encapsulating the
|
wneuper@3881
|
190 |
>>> JRMP call data within an HTTP POST request. etc..)
|
wneuper@3881
|
191 |
>>>
|
wneuper@3881
|
192 |
>>
|
wneuper@3881
|
193 |
> ... das gilt für die Firewall auf der Serverseite; wir brauchen aber
|
wneuper@3881
|
194 |
> nur die Firewall auf der Clientseite beachten, da der isacserver am
|
wneuper@3881
|
195 |
> IST _vor_ der Firewall (in der dmz) läuft !
|
wneuper@3881
|
196 |
|
wneuper@3881
|
197 |
Das grosste Problem ist dass ISAC Client gleichzeitig ein RMI Server ist ...
|
wneuper@3881
|
198 |
Um die Events (CalcChanged + doUIAction) die von Dialog->Worksheet
|
wneuper@3881
|
199 |
gehen, der ISAC Client registriert einen RMI Server auf der Client
|
wneuper@3881
|
200 |
Machine ... Und wenn der Server versucht, die Verbindung aufzubauen,
|
wneuper@3881
|
201 |
dann scheitert das ganze am Client Firewall ...
|
wneuper@3881
|
202 |
|
wneuper@3881
|
203 |
Das alles schaut grob so aus :
|
wneuper@3881
|
204 |
|
wneuper@3881
|
205 |
WindowApplication ISAC Server
|
wneuper@3881
|
206 |
|
wneuper@3881
|
207 |
RMI Client --------------> RMI Server( 1040, 1050 , ... )
|
wneuper@3881
|
208 |
RMI Server (3113) <-------------- RMI Client
|
wneuper@3881
|
209 |
|
wneuper@3881
|
210 |
Wir haben das ganze so umgeschrieben dass die RMI Sockets umgekehrt
|
wneuper@3881
|
211 |
funktionieren ... Das ist eigentlich schwer zu erklären, aber es
|
wneuper@3881
|
212 |
schaut das ganze so aus :
|
wneuper@3881
|
213 |
|
wneuper@3881
|
214 |
RMI Client --------------> RMI Server( 1040, 1050 , ... )
|
wneuper@3881
|
215 |
Quasi RMI Server (3113) --------------> Quasi RMI Client
|
wneuper@3881
|
216 |
|
wneuper@3881
|
217 |
Das Problem da ist, dass ganze sehr empfindlich ist ... Falls die
|
wneuper@3881
|
218 |
Verbindung aufgebrochen wird, gibt es kein mechanismus um die wieder
|
wneuper@3881
|
219 |
aufzubauen und das System wartet ewig darauf ...
|
wneuper@3881
|
220 |
|
wneuper@3881
|
221 |
Beim letzten versuch im HTL war die kommunikation zwischen Client und
|
wneuper@3881
|
222 |
Server schon aufgebaut (wir konnten alle browser fenster aufmachen),
|
wneuper@3881
|
223 |
aber es war, wie schon gesagt, sehr instabil bzw. hat das System oft
|
wneuper@3881
|
224 |
abgesturzt ....
|
wneuper@3881
|
225 |
|
wneuper@3881
|
226 |
Meine vermutung ist dass im ReverseClientSocket und
|
wneuper@3881
|
227 |
ReverseServerSocket ein bug liegt oder dass man diese klassen
|
wneuper@3881
|
228 |
irgendwie umbauen muss ...
|
wneuper@3881
|
229 |
|
wneuper@3881
|
230 |
|
wneuper@3881
|
231 |
--
|
wneuper@3881
|
232 |
lG,
|
wneuper@3881
|
233 |
Nelle
|
wneuper@3881
|
234 |
\end{verbatim}
|
wneuper@3881
|
235 |
|
wneuper@3881
|
236 |
|
agriesma@306
|
237 |
|
akremp@767
|
238 |
\chapter{The worksheet}
|
agriesma@306
|
239 |
A worksheet is the protocol of a more or less interactive calculation of an example, and it offers access to all services necessary to calculate the result of the example.
|
agriesma@306
|
240 |
|
agriesma@306
|
241 |
\subparagraph{A calculation mirrors the structure of the prooftree.}
|
agriesma@306
|
242 |
{\bf\SR The structure of a calculation is given by the ME. \label{}} Consequently any editing in a calculation affects the parts depending on the edited formula or tactic. Edit the worksheet w.r.t. UR \ref{edit} for publication etc. is done outside \sisac{} after having exported the calculation.
|
agriesma@306
|
243 |
{\bf\SR Export a calculation to a standard format \label{}} preferably XML plus MathML.
|
agriesma@306
|
244 |
|
agriesma@306
|
245 |
%{\bf\SR \label{}}
|
agriesma@306
|
246 |
|
rkoenig@3668
|
247 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
248 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
249 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
250 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
251 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
252 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
253 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
254 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
255 |
%--------------------------------------------------------------------------------------------------------
|
rkoenig@3668
|
256 |
% FIXXME RK, Oct. 2006 old version:
|
rkoenig@3668
|
257 |
% \chapter{The browser generators}
|
rkoenig@3668
|
258 |
% \sisac's mathematics knowledge (on (1)theories (2)problems (3)methods)
|
rkoenig@3668
|
259 |
% is held in SML datastructures. Here we describe all requirements
|
rkoenig@3668
|
260 |
% concerning the generation of the browsers written in Java, whereas
|
rkoenig@3668
|
261 |
% the generation of the math knowledge itself is described in the
|
rkoenig@3668
|
262 |
% 'interfaces for authors of math knowledge'.
|
rkoenig@3668
|
263 |
%
|
rkoenig@3668
|
264 |
% The browser generators provide the contents for the browsers. This
|
rkoenig@3668
|
265 |
% means that a browser querys its respective browser generator about
|
rkoenig@3668
|
266 |
% subnodes etc. whereas the further description is held outside the
|
rkoenig@3668
|
267 |
% SML-engine. To maintain this connection, unique identifyer are needed.
|
rkoenig@3668
|
268 |
% {\bf\SR browser-generators use locally unique identifyers \label{}} (locally unique within SML) for their informations (for each node of their structure).
|
rkoenig@3668
|
269 |
%
|
rkoenig@3668
|
270 |
% \subparagraph{Data are structured hierarchically,} i.e. the problems, methods and examples. (The theories for a directed graph without cycles; thus it also can presented by a hierarchy.)
|
rkoenig@3668
|
271 |
% {\bf\SR The hiearchy displayed in a frame \label{}} in order to have it visible all the time.
|
rkoenig@3668
|
272 |
% {\bf\SR The hierarchy has arbitrary levels. \label{}} For the headlines for each level see SR \dots SR \ref{expl-headlines}.
|
rkoenig@3668
|
273 |
% {\bf\SR The hierarchy shows the position \label{}} of the related element displayed in the browser-window; for this purpose an additional button is required, because the 'back' and 'forward'-button on the browser may disconnect the relation.
|
rkoenig@3668
|
274 |
%
|
rkoenig@3668
|
275 |
%
|
rkoenig@3668
|
276 |
% \section{The theory browser generator}
|
rkoenig@3668
|
277 |
% The generation of the theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
|
rkoenig@3668
|
278 |
% {\bf\SR The theory browser generator is given by Isabelle. \label{gen-isa}}
|
rkoenig@3668
|
279 |
%
|
rkoenig@3668
|
280 |
% \section{The problem and method browser generators}
|
rkoenig@3668
|
281 |
% .
|
rkoenig@3668
|
282 |
%
|
rkoenig@3668
|
283 |
% \section{The example browser generator}
|
rkoenig@3668
|
284 |
% This authoring component comprises all tools necessary to generate the content displayed by the example browser.
|
rkoenig@3668
|
285 |
%
|
rkoenig@3668
|
286 |
% {\bf\SR The headlines of the example-hierarchy: \label{expl-headlines}} The hierarchy comprises the labels of the chapters, sections, subsections etc. plus the respective head line, and the blocks of examples with the respective labels -- all defined by the user (see UR \ref{UR161a}).
|
rkoenig@3668
|
287 |
%
|
rkoenig@3668
|
288 |
% {\bf\SR Integrated editors for text, formulas and figures. \label{}} This integration should be as smooth as possible; it includes an MathML-based formula-editor for the formalization.
|
rkoenig@3668
|
289 |
%
|
rkoenig@3668
|
290 |
% \chapter{The knowledge browsers}
|
rkoenig@3668
|
291 |
% \label{kbrowser}
|
rkoenig@3668
|
292 |
% %W.N.: dieser Abschnitt ist f''ur A.G. + W.N.
|
rkoenig@3668
|
293 |
% All browsers (Example-Browser and Knowledge-Browsers) present their
|
rkoenig@3668
|
294 |
% output in a similar way. Textual descriptions have to be combined with
|
rkoenig@3668
|
295 |
% images, formulas, formalisations, problems, \dots and links to further
|
rkoenig@3668
|
296 |
% informations(UR\ref{URinterlink}). The structure of this informations
|
rkoenig@3668
|
297 |
% has to be taken from the respective browser-generators. All kinds of
|
rkoenig@3668
|
298 |
% information might be interlinked among each other, but not all parts
|
rkoenig@3668
|
299 |
% of the information might be already present in the system when a new
|
rkoenig@3668
|
300 |
% item is inserted. (e.g. a example might use the keyword
|
rkoenig@3668
|
301 |
% \emph{is\_rooteq\_in} in its \emph{where}\/clause before the keyword
|
rkoenig@3668
|
302 |
% is described in the system. If the example is viewed after a
|
rkoenig@3668
|
303 |
% description became available, a link to the explanation should be
|
rkoenig@3668
|
304 |
% provided automatically.) To support this feature, the browsers need a
|
rkoenig@3668
|
305 |
% fast way to look up a special description.
|
rkoenig@3668
|
306 |
% {\bf\SR fast look up for description (includes resolve of the
|
rkoenig@3668
|
307 |
% identifyer and query for a description)}
|
rkoenig@3668
|
308 |
%
|
rkoenig@3668
|
309 |
% \subparagraph{Groups of users} are usually 1-to-1 related to courses; members of courses get specific examples and specific advice by explanations.
|
rkoenig@3668
|
310 |
% {\bf\SR Each user is assigned exactly one group during a session. \label{}} The user, however, may start another session as a member of another group.
|
rkoenig@3668
|
311 |
% {\bf\SR There is a default group for visitors. \label{}}
|
rkoenig@3668
|
312 |
% {\bf\SR \label{}}
|
rkoenig@3668
|
313 |
%
|
rkoenig@3668
|
314 |
% \subparagraph{Additional data and visibility properties:} A considerable part of the data are additional to the data generated from the SML structures. The visibility concerns enabled or disabled links from problem and methods, and the access to examples from the hierarchy frame. There are respective time constraints on the visibility.
|
rkoenig@3668
|
315 |
% {\bf\SR Additional data and visibility are course specific. \label{}}
|
rkoenig@3668
|
316 |
% {\bf\SR Time constraints are given by intervals; \label{}} there are specific values for the limits of the interval indicanting infinity (contraint is given from the very beginning, or lasts forever).
|
rkoenig@3668
|
317 |
%
|
rkoenig@3668
|
318 |
%
|
rkoenig@3668
|
319 |
% \section{The theory browser}
|
rkoenig@3668
|
320 |
% The theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
|
rkoenig@3668
|
321 |
% {\bf\SR the theory browser is given by Isabelle. \label{}}
|
rkoenig@3668
|
322 |
%
|
rkoenig@3668
|
323 |
% \section{The problem and method browsers}
|
rkoenig@3668
|
324 |
% %\subparagraph{Static and dynamic views onto the KB} are provided by both browsers. Thus the (HTML-) presentation is generated dynamically. The dynamic view for problemjs concerns instantiation by a model of the current calculation on the worksheet. The dynamic view for methods concerns marking the tactic currently applied in a calculation.
|
rkoenig@3668
|
325 |
% %{\bf\SR Browsers create the presentation in browser-windows dynamically. \label{}}
|
rkoenig@3668
|
326 |
%
|
rkoenig@3668
|
327 |
% \subparagraph{Additional data} are explanations and typical examples which may be provided for each problem and each method. Both of these kinds of additional data are spcific for courses and may underly time constraints (UR \ref{expl-locked}, UR \ref{invisible}, UR \ref{restrict-know}).
|
rkoenig@3668
|
328 |
%
|
rkoenig@3668
|
329 |
% The primary contents are the respective problem and the respective method; {\em all} other data are reachable by links. This holds for special mathematical data (on rulesets etc.) from SML, too.
|
rkoenig@3668
|
330 |
% {\bf\SR A problem-page consists of \label{problem-page}} the
|
rkoenig@3668
|
331 |
% \begin{tabbing}
|
rkoenig@3668
|
332 |
% 12345\=123\=123\=\kill
|
rkoenig@3668
|
333 |
% \>name of the problem\\
|
rkoenig@3668
|
334 |
% \>the fields 'given', 'where', 'find' and 'relate'\\
|
rkoenig@3668
|
335 |
% \>a link to the special math data\\
|
rkoenig@3668
|
336 |
% \>a list of subordinated methods (only displayed in the hierarchy-frame)\\
|
rkoenig@3668
|
337 |
% \>an arbitrary list of links to additional data
|
rkoenig@3668
|
338 |
% \end{tabbing}
|
rkoenig@3668
|
339 |
% The next lower and next higher level in the hierarchy can be found in the hierarchy-frame.
|
rkoenig@3668
|
340 |
% {\bf\SR A method-page consists of \label{method-page}}
|
rkoenig@3668
|
341 |
% \begin{tabbing}
|
rkoenig@3668
|
342 |
% 12345\=123\=123\=\kill
|
rkoenig@3668
|
343 |
% \>name of the method\\
|
rkoenig@3668
|
344 |
% \>the script\\
|
rkoenig@3668
|
345 |
% \>a link to the special math data\\
|
rkoenig@3668
|
346 |
% \>a list of subordinated methods (only displayed in the hierarchy-frame)\\
|
rkoenig@3668
|
347 |
% \>an arbitrary list of links to additional data
|
rkoenig@3668
|
348 |
% \end{tabbing}
|
rkoenig@3668
|
349 |
% {\bf\SR The links to additional data \label{}} have the following attributes:
|
rkoenig@3668
|
350 |
% \begin{tabbing}
|
rkoenig@3668
|
351 |
% 12345\=123\=123\=\kill
|
rkoenig@3668
|
352 |
% \>text on the link\\
|
rkoenig@3668
|
353 |
% \>the reference (to an explanation or to an example starting a worksheet)\\
|
rkoenig@3668
|
354 |
% \>groups\\
|
rkoenig@3668
|
355 |
% \>\>ID of first group\\
|
rkoenig@3668
|
356 |
% \>\>\>locked: list of intervals\\
|
rkoenig@3668
|
357 |
% \>\>\>???used by userID ---$>$ usermodel???\\
|
rkoenig@3668
|
358 |
% \>\>ID of second group \dots
|
rkoenig@3668
|
359 |
% \end{tabbing}
|
rkoenig@3668
|
360 |
% %{\bf\SR Explanations and examples are optional. \label{}} For each problem and each method there is {\em one ???} link for the explanations and {\em one} link for the examples (which may be disabled).
|
rkoenig@3668
|
361 |
% %{\bf\SR Access to explanations and examples of other courses \label{}} is possible by ... ??? (see UR \ref{other-courses}).
|
rkoenig@3668
|
362 |
%
|
rkoenig@3668
|
363 |
%
|
rkoenig@3668
|
364 |
%
|
rkoenig@3668
|
365 |
%
|
rkoenig@3668
|
366 |
% \section{The example browser}
|
rkoenig@3668
|
367 |
% In contrary to the problem and method browsers, the presentation of the contents of a browser-window is {\em not} generated automatically. UR \ref{expl-layout} requests for a layout 'handmade' by the course designer; there are, however, a lot of attributes invisible for the learner to be added by the course designer, too.
|
rkoenig@3668
|
368 |
%
|
rkoenig@3668
|
369 |
% \subparagraph{Attributes of examples and collections} are numerous, and thus defaults help to safe space. There is only one collection, partitioned hierarchically into subcollections.
|
rkoenig@3668
|
370 |
% {\bf\SR Default data \label{}} are filled in bottum up: A default is filled by the first non-default parent.
|
rkoenig@3668
|
371 |
% {\bf\SR A subcollection has the attributes \label{coll-attr}}
|
rkoenig@3668
|
372 |
% \begin{tabbing}
|
rkoenig@3668
|
373 |
% 12345\=123\=123\=123\=123\=\kill
|
rkoenig@3668
|
374 |
% \>headline of the collection (displayed also in the hiearchy-frame) \\
|
rkoenig@3668
|
375 |
% \>description of the collection\\
|
rkoenig@3668
|
376 |
% \>list of subcollections\\
|
rkoenig@3668
|
377 |
% \>OR\\
|
rkoenig@3668
|
378 |
% \>layout of examples belonging to this subcollection\\
|
rkoenig@3668
|
379 |
% \>author\\
|
rkoenig@3668
|
380 |
% \>copyright owner\\
|
rkoenig@3668
|
381 |
% \>groups of users, for each group: \\
|
rkoenig@3668
|
382 |
% \>\>ID of the group \\
|
rkoenig@3668
|
383 |
% \>\>schemas \\
|
rkoenig@3668
|
384 |
% \>\>\>error \\
|
rkoenig@3668
|
385 |
% \>\>\>fill-in \\
|
rkoenig@3668
|
386 |
% \>\>\> \\
|
rkoenig@3668
|
387 |
% \>\>dialog \\
|
rkoenig@3668
|
388 |
% %\>\>\>blackbox \\
|
rkoenig@3668
|
389 |
% \>\>\>detail \\
|
rkoenig@3668
|
390 |
% \>\>\>activity \\
|
rkoenig@3668
|
391 |
% \>\>\>stepwidt \\
|
rkoenig@3668
|
392 |
% \>\>\> \\
|
rkoenig@3668
|
393 |
% \>\>invisible: list of intervals OR duration (? TODO !)\\
|
rkoenig@3668
|
394 |
% \>\>locked: list of intervalsOR duration (? TODO !) \\
|
rkoenig@3668
|
395 |
% \>\>evaluation \\
|
rkoenig@3668
|
396 |
% \>\>\>TODO: difficulty, length, \dots \\
|
rkoenig@3668
|
397 |
% \>\>\>finished-by: \\
|
rkoenig@3668
|
398 |
% \>\>\>\>elements: list of mandatory examples (or groups) to be done \\
|
rkoenig@3668
|
399 |
% \>\>\>\>number: number of (arbitrary) examples (or groups) to be done \\
|
rkoenig@3668
|
400 |
% \>\>\>\>points: calculated from TODO: difficulty, length, \dots \\
|
rkoenig@3668
|
401 |
% \end{tabbing}
|
rkoenig@3668
|
402 |
% Pay attention to the entry 'list of subcollections OR ayout of examples belonging to this subcollection': This means that the subcollection {\em exactly one} hierarchy-level above the bottom of individual examples has a specific content, the graphical layout of the examples. This is in order to meet UR \ref{expl-layout}.
|
rkoenig@3668
|
403 |
%
|
rkoenig@3668
|
404 |
%
|
rkoenig@3668
|
405 |
% {\bf\SR An example has the attributes \label{expl-att}}
|
rkoenig@3668
|
406 |
% \begin{tabbing}
|
rkoenig@3668
|
407 |
% 12345\=123\=123\=123\=123\=123\=\kill
|
rkoenig@3668
|
408 |
% \>label \\
|
rkoenig@3668
|
409 |
% \>reference ??? to the description of the example (in the layout ?)\\
|
rkoenig@3668
|
410 |
% \>list of formalizations and specifications \\
|
rkoenig@3668
|
411 |
% \>author\\
|
rkoenig@3668
|
412 |
% \>copyright owner\\
|
rkoenig@3668
|
413 |
% \>time stamp\\
|
rkoenig@3668
|
414 |
% \>groups of users, for each group: \\
|
rkoenig@3668
|
415 |
% \>\>ID of the group \\
|
rkoenig@3668
|
416 |
% \>\>schemas \\
|
rkoenig@3668
|
417 |
% \>\>\>error \\
|
rkoenig@3668
|
418 |
% \>\>\>fill-in \\
|
rkoenig@3668
|
419 |
% \>\>\> \\
|
rkoenig@3668
|
420 |
% \>\>dialog \\
|
rkoenig@3668
|
421 |
% \>\>\>blackbox \\
|
rkoenig@3668
|
422 |
% \>\>\>detail \\
|
rkoenig@3668
|
423 |
% \>\>\>activity \\
|
rkoenig@3668
|
424 |
% \>\>\>stepwidt \\
|
rkoenig@3668
|
425 |
% \>\>\> \\
|
rkoenig@3668
|
426 |
% \>\>invisible: list of intervals OR duration (? TODO !) \\
|
rkoenig@3668
|
427 |
% \>\>locked: list of intervals OR duration (? TODO !)\\
|
rkoenig@3668
|
428 |
% \>\>evaluation \\
|
rkoenig@3668
|
429 |
% \>\>\>TODO: difficulty, length, \dots \\
|
rkoenig@3668
|
430 |
% \>\>???done by userID ---$>$ usermodel???
|
rkoenig@3668
|
431 |
% \end{tabbing}
|
rkoenig@3668
|
432 |
% {\bf\SR Hitting the label of the example starts the calculation. \label{}}
|
rkoenig@3668
|
433 |
%
|
rkoenig@3668
|
434 |
% \subparagraph{Visibility of the examples} is defined in two levels: (1) 'locked' displays the text of the example, but doesn't allow to calculate it; and (2) 'invisible' desn't display the example at all.
|
rkoenig@3668
|
435 |
% {\bf\SR {\em Only} visible examples are checked for being locked.\label{}}
|
rkoenig@3668
|
436 |
% %{\bf\SR Authoring-/learner-mode:} the formalization and other attributes are shown/not shown, depending on the group the user belongs to.
|
rkoenig@3668
|
437 |
%
|
rkoenig@3668
|
438 |
% %\subparagraph{}
|
rkoenig@3668
|
439 |
% %{\bf\SR \label{}}
|
agriesma@306
|
440 |
|
wneuper@3670
|
441 |
%WN050519---AG------old version replaced by RK below
|
wneuper@3670
|
442 |
%WN050519---RK->isac-SRD-----------------BEGIN---please don't remove this line
|
agriesma@306
|
443 |
|
agriesma@306
|
444 |
|
rkoenig@3668
|
445 |
% FIXXME RK, Oct. 2006 new version:
|
rkoenig@3668
|
446 |
\chapter{Views on Examples and Knowledge Items}
|
wneuper@3670
|
447 |
|
wneuper@3684
|
448 |
\footnote{Begin of \cite{ba-RK06} p....-- p....}
|
wneuper@3670
|
449 |
|
wneuper@3670
|
450 |
This chapter describes the software requirements for the browsers and the
|
rkoenig@3668
|
451 |
browserdialogs controlling these browsers.
|
agriesma@306
|
452 |
|
rkoenig@3668
|
453 |
All browsers (Example-Browser and Knowledge-Browsers) present their
|
rkoenig@3668
|
454 |
output in a similar way. Textual descriptions have to be combined with
|
rkoenig@3668
|
455 |
images, formulas, formalisations, problems, \dots and links to further
|
wneuper@3670
|
456 |
informations. All items of
|
wneuper@3670
|
457 |
information might be interlinked with each other.%WN061009??,but not all parts
|
wneuper@3670
|
458 |
%of the information might be already present in the system when a new
|
wneuper@3670
|
459 |
%item is inserted.
|
agriesma@306
|
460 |
|
rkoenig@3668
|
461 |
\section{General Requirements}
|
agriesma@306
|
462 |
|
rkoenig@3668
|
463 |
%NOTE: completely new:
|
wneuper@3670
|
464 |
{\bf\SR Unique identification by a GUH.\label{SR.RK-id-by-guh}}
|
wneuper@3670
|
465 |
Each item of the examples collection or the knowledge base is uniquely identified
|
wneuper@3670
|
466 |
by a GUH (Global Unique Identifier).
|
rkoenig@3668
|
467 |
The GUH is a String starting with \verb,'thy_', for theory elements, \verb,'pbl_', for problem elements,
|
rkoenig@3668
|
468 |
\verb,'met_', for method elements and \verb,'exp_', for examples.
|
agriesma@306
|
469 |
|
rkoenig@3668
|
470 |
%NOTE: completely new:
|
wneuper@3670
|
471 |
{\bf\SR Presentation in a standard browser and in the \isac-browsers.\label{SR.RK-stand-and-isac-browser}} The knowledge elements and examples can be viewed in a standard browser as well
|
wneuper@3670
|
472 |
as in the \isac-browsers. Thus, knowledge elements have to be available in HTML
|
rkoenig@3668
|
473 |
form in some way.
|
rkoenig@3668
|
474 |
|
rkoenig@3668
|
475 |
%NOTE: completely new:
|
wneuper@3670
|
476 |
{\bf\SR GUHs as links.\label{SR.RK-link-by-guh}}
|
wneuper@3670
|
477 |
Links between elements of the knowledge base are defined by the GUH of the link target.
|
rkoenig@3668
|
478 |
To make the links work in a standard browser, some path information has to be added to the URL in the
|
rkoenig@3668
|
479 |
HMTL representation of the knowledge elements.
|
rkoenig@3668
|
480 |
|
wneuper@3670
|
481 |
%NOTE: something similar already existed: RIGHT: this is a USER-requirement
|
wneuper@3670
|
482 |
%{\bf\SR Additional information can be given to any element of the knowledge base or the
|
wneuper@3670
|
483 |
%examples collection.\label{SR.RK-add-info}}
|
wneuper@3670
|
484 |
%This information is not extracted from the SML structures, it is added by the course designer.
|
wneuper@3670
|
485 |
%The additional information can contain links to
|
wneuper@3670
|
486 |
%examples or elements of the knowledge base. External links and images are possible as well.
|
rkoenig@3668
|
487 |
|
rkoenig@3668
|
488 |
%NOTE: completely new:
|
wneuper@3670
|
489 |
%WN061009 isn't that an (ugly!) _consequence_ of the present (ugly!) handling of the browsers contents ?!?
|
wneuper@3670
|
490 |
%{\bf\SR The \isac-browsers can display the content of HTML files on the local file system as
|
wneuper@3670
|
491 |
%well as files available over the World Wide Web.\label{SR.RK-html-local-web}}
|
rkoenig@3668
|
492 |
|
rkoenig@3668
|
493 |
%NOTE: completely new:
|
wneuper@3670
|
494 |
{\bf\SR Asynchronous load of content.\label{SR.RK-browser-load-asynch}} The \isac-browsers load the content to be displayed asynchronously. That means, that the
|
rkoenig@3668
|
495 |
user interface does not block until the page is loaded. The page is loaded in an extra thread instead.
|
rkoenig@3668
|
496 |
|
rkoenig@3668
|
497 |
%NOTE: copied:
|
rkoenig@3668
|
498 |
{\bf\SR The hierarchy is displayed in a frame \label{SR.RK-hier-in-frame}} in order to have it visible all the time.
|
rkoenig@3668
|
499 |
%NOTE: copied:
|
rkoenig@3668
|
500 |
{\bf\SR The hierarchy has arbitrary levels. \label{SR.RK-hier-arb-levels}}
|
rkoenig@3668
|
501 |
%NOTE: copied:
|
rkoenig@3668
|
502 |
{\bf\SR The hierarchy shows the position \label{SR.RK-hier-arb-levels}} of the related element displayed in the browser-window.
|
rkoenig@3668
|
503 |
|
rkoenig@3668
|
504 |
\section{The Knowledge Browsers}
|
wneuper@3670
|
505 |
The following enumerations do {\em not} show all items contained in the respective sml datastructure; rather it shows the 'most important' ones --- a preliminary decision, which will be overlayed by filtering due to the dialog-guide.
|
rkoenig@3668
|
506 |
%NOTE: modified:
|
rkoenig@3668
|
507 |
{\bf\SR A problem page consists of:\label{SR.RK-pbl-consists}}
|
wneuper@3670
|
508 |
%WN061009 problem content-page ? problem content ?
|
rkoenig@3668
|
509 |
\begin{enumerate}
|
wneuper@3670
|
510 |
\item name of the problem or the 'CAS-command' (a short command similar to an algebra system; e.g. {\em solve})
|
rkoenig@3668
|
511 |
\item a model consisting of the fields 'given', 'where', 'find' and 'relate'
|
wneuper@3670
|
512 |
\item explanations %WN see 'list of terms...' additional data
|
rkoenig@3668
|
513 |
\item the authors
|
wneuper@3670
|
514 |
\item the position within the problem-hierarchy displayed in the hierarchy-frame)
|
rkoenig@3668
|
515 |
\end{enumerate}
|
rkoenig@3668
|
516 |
|
rkoenig@3668
|
517 |
%NOTE: modified:
|
rkoenig@3668
|
518 |
{\bf\SR A method page consists of:\label{SR.RK-met-consists}}
|
rkoenig@3668
|
519 |
\begin{enumerate}
|
rkoenig@3668
|
520 |
\item the script
|
rkoenig@3668
|
521 |
\item a name (only displayed in the hierarchy-frame)
|
rkoenig@3668
|
522 |
\item a guard consisting of the fields 'given', 'where', 'find' and 'relate'
|
wneuper@3670
|
523 |
\item explanations %WN see 'list of terms...' additional data
|
rkoenig@3668
|
524 |
\item the authors
|
wneuper@3670
|
525 |
\item the position within the method-hierarchy displayed in the hierarchy-frame\end{enumerate}
|
rkoenig@3668
|
526 |
|
rkoenig@3668
|
527 |
%NOTE: completely new:
|
wneuper@3670
|
528 |
{\bf\SR A theorem page (within theories) consists of:\label{SR.RK-thm-thy-consists}}
|
rkoenig@3668
|
529 |
\begin{enumerate}
|
rkoenig@3668
|
530 |
\item the name of the theorem
|
wneuper@3670
|
531 |
\item the formula of the theorem
|
wneuper@3670
|
532 |
\item a link to the proof of the theorem within Isabelle %WN061009 TODO
|
wneuper@3670
|
533 |
\item explanations %WN see 'list of terms...' additional data
|
rkoenig@3668
|
534 |
\item the authors (math authors and course designers)
|
rkoenig@3668
|
535 |
\end{enumerate}
|
rkoenig@3668
|
536 |
|
rkoenig@3668
|
537 |
%NOTE: completely new:
|
wneuper@3670
|
538 |
{\bf\SR A ruleset page (within theories) consists of:\label{SR.RK-rls-thy-consists}}
|
rkoenig@3668
|
539 |
\begin{enumerate}
|
rkoenig@3668
|
540 |
\item the identifier of the ruleset
|
wneuper@3670
|
541 |
\item the type of the ruleset ({\tt Rls, Seq, Rrls}) %WN061009 TODO: use tag <TYPE>
|
wneuper@3670
|
542 |
\item a list of rules and links to the rules. Rules can be theorems other rulesets or operations.
|
rkoenig@3668
|
543 |
\item a rewrite order
|
wneuper@3670
|
544 |
\item explanations %WN see 'list of terms...' additional data
|
rkoenig@3668
|
545 |
\item the authors (math authors and course designers)
|
wneuper@3670
|
546 |
\item the position within the theory-hierarchy displayed in the hierarchy-frame
|
rkoenig@3668
|
547 |
\end{enumerate}
|
rkoenig@3668
|
548 |
|
rkoenig@3668
|
549 |
%NOTE: completely new:
|
rkoenig@3668
|
550 |
{\bf\SR A htmldata theory page consists of:\label{SR.RK-html-thy-consists}}
|
rkoenig@3668
|
551 |
\begin{enumerate}
|
wneuper@3670
|
552 |
\item explanations %WN see 'list of terms...' additional data
|
rkoenig@3668
|
553 |
\item the authors
|
rkoenig@3668
|
554 |
\end{enumerate}
|
rkoenig@3668
|
555 |
|
rkoenig@3668
|
556 |
%NOTE: completely new:
|
wneuper@3670
|
557 |
{\bf\SR Similar representation for static and dynamic content.\label{SR.RK-add-context-2-html}}
|
wneuper@3670
|
558 |
If elements of the knowledge base are shown in the \isac-browser, the
|
wneuper@3670
|
559 |
content can be enriched with dynamically generated context dependent information.
|
rkoenig@3668
|
560 |
Any selected formula in the worksheet has a context to an element of the knowledge base.
|
rkoenig@3668
|
561 |
This context information is inserted into the HTML content displayed in the browser if the
|
rkoenig@3668
|
562 |
feature is activated.
|
rkoenig@3668
|
563 |
|
rkoenig@3668
|
564 |
%NOTE: completely new:
|
wneuper@3670
|
565 |
{\bf\SR Data and representation separated.\label{SR.RK-data-rep-sep}}
|
wneuper@3670
|
566 |
The knowledge data and its representation should be separated well.
|
rkoenig@3668
|
567 |
|
rkoenig@3668
|
568 |
%NOTE: completely new:
|
wneuper@3670
|
569 |
{\bf\SR Easy generation of different representations.\label{SR.RK-rep-to-data}} SR.\ref{SR.RK-data-rep-sep}
|
wneuper@3670
|
570 |
The system must provide an easy way of generating different representations
|
wneuper@3670
|
571 |
of the same knowledge data. SR.\ref{SR.RK-data-rep-sep} is a precondition to
|
rkoenig@3668
|
572 |
make this possible.
|
rkoenig@3668
|
573 |
|
neuper@4128
|
574 |
\section{The example browser} In contrary to the knowledge browsers,
|
neuper@4128
|
575 |
the presentation of the contents of a browser-window is {\em not}
|
neuper@4128
|
576 |
generated automatically. UR \ref{expl-layout} requests for a layout
|
neuper@4128
|
577 |
'handmade' by the course designer; there are, however, a lot of
|
neuper@4128
|
578 |
attributes invisible for the learner to be added by the course
|
neuper@4128
|
579 |
designer, too.
|
agriesma@306
|
580 |
|
neuper@4128
|
581 |
{\bf\SR The headlines of the
|
neuper@4128
|
582 |
example-hierarchy: \label{expl-headlines}} The hierarchy comprises the
|
neuper@4128
|
583 |
labels of the chapters, sections, subsections etc. plus the respective
|
neuper@4128
|
584 |
head line, and the blocks of examples with the respective labels --
|
neuper@4128
|
585 |
all defined by the user (see UR \ref{UR161a}).
|
agriesma@306
|
586 |
|
wneuper@3670
|
587 |
{\bf\SR Metadata for selecting examples: \label{SR.WN-exp-metadata}}
|
neuper@4128
|
588 |
\subparagraph{Attributes of examples and collections} are numerous,
|
neuper@4128
|
589 |
and thus defaults help to safe space.
|
agriesma@306
|
590 |
|
neuper@4128
|
591 |
{\bf\SR Visibility of examples: \label{SR.WN-exp-visible}} Visibility
|
neuper@4128
|
592 |
of the examples is defined in two levels: (1) 'locked' displays the
|
neuper@4128
|
593 |
text of the example, but doesn't allow to calculate it; and (2)
|
neuper@4128
|
594 |
'invisible' doesn't display the example at all.
|
agriesma@306
|
595 |
|
agriesma@306
|
596 |
{\bf\SR {\em Only} visible examples are checked for being locked.\label{}}
|
agriesma@306
|
597 |
|
wneuper@3684
|
598 |
\footnote{End of \cite{ba-RK06} p....-- p....}
|
wneuper@3670
|
599 |
%WN050519---RK->isac-SRD-----------------END---please don't remove this line
|
rkoenig@3668
|
600 |
|
rkoenig@3668
|
601 |
|
rkoenig@3668
|
602 |
|
agriesma@306
|
603 |
|
agriesma@306
|
604 |
|
agriesma@306
|
605 |
|
akremp@767
|
606 |
\chapter{The dialog guide}
|
agriesma@306
|
607 |
|
agriesma@306
|
608 |
%{\bf\SR A learner has a dialog state within the current session. \label{}}
|
agriesma@306
|
609 |
%{\bf\SR Each learner has a history of all sessions. \label{}}
|
agriesma@306
|
610 |
%{\bf\SR The history holds the condensed performance in calculations. \label{}}
|
agriesma@306
|
611 |
%{\bf\SR The history holds requests into the knowledge. \label{}\\}
|
agriesma@306
|
612 |
%\subparagraph{}
|
agriesma@306
|
613 |
%{\bf\SR \\}
|
agriesma@306
|
614 |
|
neuper@4128
|
615 |
As of 2012, the dialog is still a stub which just passes input from
|
neuper@4128
|
616 |
the learner on to the math engine, and results of calculation from the
|
neuper@4128
|
617 |
math engine back to the learner. Presently, replacement of Java code
|
neuper@4128
|
618 |
by a rule-based system in the dialog is under construction. A
|
neuper@4128
|
619 |
UserLogger is being re-engineered in order to serve dialog guidance
|
neuper@4128
|
620 |
planned for the future.
|
agriesma@306
|
621 |
|
neuper@4108
|
622 |
\section{Components of the dialog guide}
|
neuper@4108
|
623 |
{\bf\SR A dialog consists of }\label{DG:components}
|
neuper@4108
|
624 |
\begin{enumerate}
|
neuper@4108
|
625 |
\item a {\em dialog profile} which initializes the dialog
|
neuper@4108
|
626 |
\item a {\em dialog history} which records each step in problem solving
|
neuper@4108
|
627 |
\item {\em dialog rules} which which determine the flow of interaction
|
neuper@4108
|
628 |
\item a {\em dialog guide} which selects the {\em dialog rules};\\
|
neuper@4108
|
629 |
these rules determine what is called a 'dialog mode'
|
neuper@4108
|
630 |
\item a {\em dialog state} which comprises the data from the current session
|
neuper@4128
|
631 |
\item a {\em learner model} which abstracts from the {\em dialog state}s
|
neuper@4128
|
632 |
during a course.
|
neuper@4108
|
633 |
\end{enumerate}
|
neuper@4128
|
634 |
The above notions will be used without the initial 'dialog' in a respective
|
neuper@4128
|
635 |
context.
|
neuper@4108
|
636 |
|
neuper@4128
|
637 |
{\bf\SR A dialog profile determines initialisation}\label{xxx} of the
|
neuper@4209
|
638 |
dialog guide at the first registration and also in case of an
|
neuper@4209
|
639 |
'exclusive' profile (in exams etc). A dialog profile can be
|
neuper@4209
|
640 |
'exclusive' in order to feature assessments: within explicit time
|
neuper@4209
|
641 |
limits an exclusive profile inhibits all other sessions of this
|
neuper@4209
|
642 |
student.
|
neuper@4108
|
643 |
|
neuper@4128
|
644 |
{\bf\SR The dialog history records {\em dialog atoms}}\label{xxx} ,
|
neuper@4128
|
645 |
i.e. steps of problem solving (an input by the learner together with
|
neuper@4128
|
646 |
the reaction of the math engine) or look-ups in the knowledge base.
|
neuper@4108
|
647 |
|
neuper@4128
|
648 |
{\bf\SR A set of dialog rules comprises {\em dialog
|
neuper@4128
|
649 |
patterns}}\label{xxx} which in turn are composed from {\em dialog
|
neuper@4128
|
650 |
atoms}.
|
neuper@4108
|
651 |
|
neuper@4128
|
652 |
{\bf\SR The dialog guide selects {\em dialog patterns}}\label{xxx}
|
neuper@4128
|
653 |
according to the {\em user model} from previous sessions, from the
|
neuper@4128
|
654 |
{\em dialog profile} at start of the current session and from the
|
neuper@4128
|
655 |
dialog state modified during the current session.
|
neuper@4108
|
656 |
|
neuper@4128
|
657 |
{\bf\SR The dialog state comprises current data}\label{xxx}, i.e. the
|
neuper@4128
|
658 |
{\em dialog history} of the current session and the sets of {\em
|
neuper@4128
|
659 |
dialog rules} employed in the current session.
|
neuper@4108
|
660 |
|
neuper@4128
|
661 |
{\bf\SR The learner model abstracts over all sessions}\label{xxx} in a
|
neuper@4128
|
662 |
course such that the next session can be started adapting to the
|
neuper@4128
|
663 |
personal needs of the learner.
|
neuper@4108
|
664 |
\\
|
neuper@4108
|
665 |
|
neuper@4108
|
666 |
%{\bf\SR xxx }\label{xxx}
|
neuper@4108
|
667 |
|
neuper@4108
|
668 |
$/------$ not revised since $1^{st}$ design phase in 2001 $------\backslash$
|
neuper@4108
|
669 |
|
neuper@4128
|
670 |
\section{The dialogstate} is read and updated during {\em one}
|
neuper@4128
|
671 |
session. A dialog resumes the dialogstate from the previous session
|
neuper@4128
|
672 |
done as a member of the same student-group.
|
neuper@4108
|
673 |
|
neuper@4128
|
674 |
{\bf\SR The last dialogstate is stored \label{}} at the end of a
|
neuper@4128
|
675 |
student's session for each group the student is a member of. When
|
neuper@4128
|
676 |
storing and replacing the previous dialogstate, this dialogstate is
|
neuper@4128
|
677 |
transferred to the history of the usermodel (eventually after
|
neuper@4128
|
678 |
compression).
|
neuper@4108
|
679 |
|
agriesma@306
|
680 |
{\bf\SR The dialogstate has the attributes \label{}}
|
agriesma@306
|
681 |
{\small
|
agriesma@306
|
682 |
\begin{tabbing}
|
agriesma@306
|
683 |
12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
|
agriesma@306
|
684 |
\>begin \>\>\>\>\>\>\>\>\>timestamp of begin of session\\
|
agriesma@306
|
685 |
\>provided-end\>\>\>\>\>\>\>\>\>e.g. for examinations\\
|
agriesma@306
|
686 |
\>actual-end \>\>\>\>\>\>\>\>\>empty, or timestamp of end of session\\
|
agriesma@306
|
687 |
\>group \>\>\>\>\>\>\>\>\>the user has started the session with\\
|
agriesma@306
|
688 |
\>interactions, for each: \\
|
agriesma@306
|
689 |
\>\>timestamp\\
|
agriesma@306
|
690 |
\>\>label of example\>\>\>\>\>\>\>\>empty if \sisac{} entered via KB\\
|
agriesma@306
|
691 |
\>\>input\>\>\>\>\>\>\>\>tactic, formula, command or label in KB\\
|
agriesma@306
|
692 |
\>\>response\>\>\>\>\>\>\>\>??? of which part of system ???\\
|
agriesma@306
|
693 |
\>\>pattern\>\>\>\>\>\>\>\>of dialog\\
|
agriesma@306
|
694 |
\>\>\>activity\\
|
agriesma@306
|
695 |
\>\>\>stepwidt\\
|
agriesma@306
|
696 |
\>\>\>\dots TODO \dots\\
|
agriesma@306
|
697 |
\end{tabbing}}
|
agriesma@306
|
698 |
The use of these fields is shown by use-case UC TODO.
|
agriesma@306
|
699 |
|
agriesma@306
|
700 |
|
neuper@4128
|
701 |
\section{The usermodel} consists of two parts: the settings of the
|
neuper@4128
|
702 |
personal preferences and the history of (condensed) dialogstates. The
|
neuper@4128
|
703 |
history is constructed from the dialogstates: before a dialogstate is
|
neuper@4128
|
704 |
being replaced at the start of a new session, its data are
|
neuper@4128
|
705 |
restructured and appended to the history.
|
neuper@4128
|
706 |
|
agriesma@306
|
707 |
{\bf\SR The usermodel has the attributes\label{}}
|
agriesma@306
|
708 |
{\small
|
agriesma@306
|
709 |
\begin{tabbing}
|
agriesma@306
|
710 |
12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
|
agriesma@306
|
711 |
\>settings\\
|
agriesma@306
|
712 |
\>\>patterns, for each:\>\>\>\>\>\>\>\>of dialog\\
|
agriesma@306
|
713 |
\>\>\>activity\\
|
agriesma@306
|
714 |
\>\>\>stepwidt\\
|
agriesma@306
|
715 |
\>\>\>\dots TODO \dots\\
|
agriesma@306
|
716 |
\>history, for each session:\>\>\>\>\>\>\>\>\>\\
|
agriesma@306
|
717 |
\>\>begin\_end\>\>\>\>\>\>\>\>2 timestamps\\
|
agriesma@306
|
718 |
\>\>group\>\>\>\>\>\>\>\> the user has started the session with\\
|
agriesma@306
|
719 |
\>\>kb\_touchs, for each:\>\>\>\>\>\>\>\>\\
|
agriesma@306
|
720 |
\>\>\>label of KB item\\
|
agriesma@306
|
721 |
\>\>\>timestamps\\
|
agriesma@306
|
722 |
\>\>examples, for each:\\
|
agriesma@306
|
723 |
\>\>\>label of example\\
|
agriesma@306
|
724 |
\>\>\>begin\_end\>\>\>\>\>\>\>2 timestamps\\
|
agriesma@306
|
725 |
\>\>\>finished\>\>\>\>\>\>\>yes/no\\
|
agriesma@306
|
726 |
\>\>\>performance\>\>\>\>\>\>\>from example.evaluation.TODO and\\
|
agriesma@306
|
727 |
\>\>\>\>\>\>\>\>\>\>from dialog.interactions\\
|
agriesma@306
|
728 |
\end{tabbing}}
|
agriesma@306
|
729 |
The use of these fields is shown by use-case UC TODO.
|
neuper@4108
|
730 |
\\
|
agriesma@306
|
731 |
|
neuper@4108
|
732 |
$\backslash------$ not revised since $1^{st}$ design phase in 2001 $------/$
|
agriesma@306
|
733 |
|
agriesma@306
|
734 |
|