repos / bachelor-thesis.git

NetworkAndService.lagda

 1\if{False}
 2\begin{code}
 3-- Imports
 4
 5open import Prelude
 6open import Syntax
 7open import Typesystem
 8open import Typingrules
 9\end{code}
10\fi
11
12\section{Service layer}
13
14The service layer contains the structures for handling communication, while entities are processes and services.
15
16At first, we need to define the \AgdaDatatype{MessageQueue}. It's simply just a queue of \AgdaDatatype{Message}s, where \AgdaDatatype{Message} is a tuple of three elements: \AgdaDatatype{Channel}, \AgdaDatatype{Operation} and \AgdaDatatype{String}. To simplify the representation of \AgdaDatatype{Message} I chose it to be a \AgdaDatatype{List} from standard library.
17
18\begin{code}
19Queue : (A : Set) → Set
20Queue A = List A
21
22Message : Set
23Message = Channel × Operation × String
24
25MessageQueue : Set
26MessageQueue = Queue Message
27\end{code}
28
29Now we can define the \AgdaDatatype{Process}:
30
31\begin{code}
32data Process : Set where
33  _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
34  nil : Process
35  _∥_ : Process → Process → Process
36\end{code}
37
38The first constructor \AgdaInductiveConstructor{\_∙\_∙\_} represents the process which consists of a behaviour, a list of variables and messages. 
39The \AgdaDatatype{Process} may be empty: \AgdaInductiveConstructor{nil}. It means that it does nothing at all, has no state and no message queue. It can't even receive messages. \AgdaInductiveConstructor{\_\textdoublevertline\_} is a constructor of the \AgdaDatatype{Process} type for parallel processes.
40
41Next, I define the \AgdaDatatype{Deployment}, which consists of \AgdaDatatype{AliasingFunction} and \AgdaDatatype{Context}. The deployment contains information about correlation sets for processes running by the service, while each set has variables which are used to identify a process. The \AgdaDatatype{AliasingFunction} is for extracting the location of correlation values for an operation from a message, but it's not required for this project, so it has no constructors. The \AgdaDatatype{Context} will be defined in chapter 3.
42
43\begin{code}
44data AliasingFunction : Set where
45
46Deployment : Set
47Deployment = AliasingFunction × Context
48\end{code}
49
50Finally, \AgdaDatatype{Service} can be defined. It has only one constructor which takes a behaviour, a deployment and a process.
51
52\begin{code}
53data Service : Set where
54  _▹_-_ : {m : ℕ} → Behaviour → Deployment → Process → Service
55\end{code}
56
57\AgdaDatatype{Service} may behave as a client or as a server. If its behaviour is \AgdaInductiveConstructor{nil}, the service will take a role of a client. If its behaviour is \textit{input choice}, the service will take a role of a server.
58
59\section{Network layer}
60
61The network layer describes the structure of a network in a Jolie program. A network is a one or more services running in parallel. Each service is running on a unique location.
62
63\begin{code}
64data Network : Set where
65  [_]_ : Service → Location → Network
66  νr : Network → Network
67  _∥_ : Network → Network → Network
68  nil : Network
69\end{code}