Information Technology Reference
In-Depth Information
and
Thus, the whole behaviour of an infostation
is modelled as
≙.
(
2
)
|
.
(
8
)
|
.(9)
(10)
6.3.1 InfoStation centre
A model of the ISC encompasses ambients modelling users' accounts and named after the
users' IDs; an ambient named
Lectures
that contains all the lecture ambients, each named
after the corresponding lecture ID Each lecture ambient contains three persistent memory
cells named
Phone
,
PDA
and
PC
; each storing the lecture's version suitable for the
corresponding type of device. The mTest service is not represented as we are only dealing
with the mLecture service in this paper. These components of the ISC are formalised
below.
Users' accounts
An ambient modelling a user's account contains two ambients named
Loc
and
Utest
. Each of these two ambients models a persistent memory cell which stores, at any
time, the current location of that user (for the former) or a Boolean indicating whether that
user is taking a mTest or not (for the latter). We understand by location of a user the IS the
user is registered with. The behaviour of the
Loc
ambient and the
Utest
ambient are specified
exactly with appropriate initial values. The ISC requests the value of any of these cells by
sending the name
Loc
or
Utest
to the user's account ambient (see Eq. (14)) which then can
get
(i.e. read) the value of the corresponding child ambient as follows, where the parameter
is
the corresponding child ambient name:
!↑
(
)
.↓⟨⟩.↓
(
)
.↑
〈
〉
.0
(11)
The user's account ambient can also put (i.e. write) a value in any of its child ambients as
follows, where the parameter
is the corresponding child ambient name and the parameter
is that value:
!↑(,).↓⟨⟩.↓().↑〈,〉.0
(12)
So the whole behaviour of a user's account ambient named uid is specified as:
≙.
(
11
)
|.
(
12
)
Lectures
As mentioned above, this ambient contains all the lectures that are available in the
mLecture service. Each lecture has a unique ID and the corresponding ambient is named
