repos / jolie.agda.git

commit

d364ed6

parent

da9b32f

author

Eugene Akentyev

date

2016-10-26 01:57:15 +0400 +04

Add Network, Queue and Service.

 1@@ -0,0 +1,11 @@
 2+module Network where
 3+
 4+open import Type
 5+open import Service
 6+
 7+
 8+data Network : Set where
 9+  [_]_ : Service → Location → Network
10+  νr : Network → Network
11+  _||_ : Network → Network → Network
12+  nil : Network

1@@ -0,0 +1,8 @@
2+module Queue where
3+
4+open import Data.List using (List)
5+
6+
7+data Queue (A : Set) : Set where
8+  nil : Queue A
9+  cons : List A → List A → Queue A

 1@@ -0,0 +1,29 @@
 2+module Service where
 3+
 4+open import Data.List using (List)
 5+open import Data.String using (String)
 6+open import Data.Product using (_×_)
 7+open import Type
 8+open import Behaviour
 9+open import Queue
10+open import Variable
11+
12+
13+Message : Set
14+Message = Channel × Operation × String
15+
16+MessageQueue : Set
17+MessageQueue = Queue Message
18+
19+data Process : Set where
20+  _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
21+  nil : Process
22+  _||_ : Process → Process → Process
23+
24+data AliasingFunction : Set where
25+
26+Deployment : Set
27+Deployment = AliasingFunction × Γ
28+
29+data Service : Set where
30+  service : Behaviour → Deployment → Process → Service