Eugene Akentyev
·
2017-02-22
BehaviouralSemantics.agda
1module BehaviouralSemantics where
2
3open import Relation.Binary.PropositionalEquality using (_≡_)
4open import Data.Vec using (Vec; toList) renaming (_∈_ to _∈-Vec_)
5open import Data.Bool using (true; false)
6open import Data.Product using (_×_; _,_)
7open import Type
8open import Behaviour
9open import Variable
10open import Expr
11
12
13data State : Set where
14
15data _⟨_⟩≔_ : Expr → State → Expr → Set where
16
17data Label : Set where
18 -- Behavioural layer
19 -- x = e
20 lb-assign : Variable → Expr → Label
21
22 -- read t
23 lb-read : State → Label
24
25 -- νr o@l(e)
26 lb-send : Channel → Operation → Location → Expr → Label
27
28 -- r : o(x)
29 lb-store : Channel → Operation → Variable → Label
30
31 -- (r, o)!x
32 lb-write : Channel → Operation → Variable → Label
33
34 -- (r, o@l)?x
35 lb-read-write : Channel → Operation → Location → Variable → Label
36
37data _↝_∶_ : Behaviour → Behaviour → Label → Set where
38 b-assign : {x : Variable} {e : Expr}
39 → (x ≃ e) ↝ nil ∶ lb-assign x e
40
41 b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable}
42 → wait r o l x ↝ nil ∶ lb-read-write r o l x
43
44 b-oneway : {o : Operation} {x : Variable} {r : Channel}
45 → input (o [ x ]) ↝ nil ∶ lb-store r o x
46
47 b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr}
48 → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e
49
50 b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable}
51 → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e
52
53 b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour}
54 → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x
55
56 b-end-exec : {r : Channel} {o : Operation} {x : Variable}
57 → exec r o x nil ↝ nil ∶ lb-write r o x
58
59 b-exec : {b b′ : Behaviour} {η : Label} {r : Channel} {o : Operation} {x : Variable}
60 → b ↝ b′ ∶ η
61 ----------------------------------
62 → exec r o x b ↝ exec r o x b′ ∶ η
63
64 b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label}
65 → b₁ ↝ b₁′ ∶ η
66 -----------------------------
67 → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η
68
69 b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label}
70 → b₁ ↝ b₁′ ∶ η
71 ----------------------------
72 → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η
73
74 b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label}
75 → b₁ ≡ b₂
76 → b₂ ↝ b₂′ ∶ η
77 → b₁′ ≡ b₂′
78 --------------
79 → b₁ ↝ b₁′ ∶ η
80
81 b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
82 → e ⟨ t ⟩≔ (constant (bool true))
83 -----------------------------------------
84 → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
85
86 b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
87 → e ⟨ t ⟩≔ (constant (bool false))
88 -----------------------------------------
89 → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
90
91 b-iteration : {e : Expr} {t : State} {b : Behaviour}
92 → e ⟨ t ⟩≔ (constant (bool true))
93 ---------------------------------------------------
94 → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
95
96 b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
97 → e ⟨ t ⟩≔ (constant (bool false))
98 ----------------------------------
99 → (while[ e ] b) ↝ nil ∶ lb-read t
100
101 b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour}
102 → (ηⱼ , bⱼ) ∈-Vec choices
103 → input ηⱼ ↝ bⱼ′ ∶ η
104 ----------------------------------------------
105 → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η
106