Add Network, Queue and Service.

diff --git a/src/Network.agda b/src/Network.agda
new file mode 100644 (file)
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 (file)
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 (file)
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