From d364ed6481626c56925c426df950c32a72882307 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Wed, 26 Oct 2016 02:57:15 +0500
Subject: [PATCH] Add Network, Queue and Service.

---
 src/Network.agda | 11 +++++++++++
 src/Queue.agda   |  8 ++++++++
 src/Service.agda | 29 +++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+)
 create mode 100644 src/Network.agda
 create mode 100644 src/Queue.agda
 create mode 100644 src/Service.agda

diff --git a/src/Network.agda b/src/Network.agda
new file mode 100644
index 0000000..a02f9b7
--- /dev/null
+++ b/src/Network.agda
@@ -0,0 +1,11 @@
+module Network where
+
+open import Type
+open import Service
+
+
+data Network : Set where
+  [_]_ : Service → Location → Network
+  νr : Network → Network
+  _||_ : Network → Network → Network
+  nil : Network
diff --git a/src/Queue.agda b/src/Queue.agda
new file mode 100644
index 0000000..a1c2e32
--- /dev/null
+++ b/src/Queue.agda
@@ -0,0 +1,8 @@
+module Queue where
+
+open import Data.List using (List)
+
+
+data Queue (A : Set) : Set where
+  nil : Queue A
+  cons : List A → List A → Queue A
diff --git a/src/Service.agda b/src/Service.agda
new file mode 100644
index 0000000..4044788
--- /dev/null
+++ b/src/Service.agda
@@ -0,0 +1,29 @@
+module Service where
+
+open import Data.List using (List)
+open import Data.String using (String)
+open import Data.Product using (_×_)
+open import Type
+open import Behaviour
+open import Queue
+open import Variable
+
+
+Message : Set
+Message = Channel × Operation × String
+
+MessageQueue : Set
+MessageQueue = Queue Message
+
+data Process : Set where
+  _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
+  nil : Process
+  _||_ : Process → Process → Process
+
+data AliasingFunction : Set where
+
+Deployment : Set
+Deployment = AliasingFunction × Γ
+
+data Service : Set where
+  service : Behaviour → Deployment → Process → Service
-- 
2.50.1