From: Eugene Akentyev Date: Thu, 26 Jan 2017 07:20:40 +0000 (+0300) Subject: Rename file and add remaining rules X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=eb93f60e8417eb8d5ce18c5d5a74c9833aa4da69;p=jolie.agda.git Rename file and add remaining rules --- diff --git a/src/BehaviouralSemantics.agda b/src/BehaviouralSemantics.agda new file mode 100644 index 0000000..cbc55ad --- /dev/null +++ b/src/BehaviouralSemantics.agda @@ -0,0 +1,100 @@ +module BehaviouralSemantics where + +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Data.Vec using (Vec; toList) renaming (_∈_ to _∈-Vec_) +open import Data.Bool using (true; false) +open import Data.Product using (_×_; _,_) +open import Type +open import Behaviour +open import Variable +open import Expr + + +data State : Set where + +data _⟨_⟩≔_ : Expr → State → Expr → Set where + +data Label : Set where + -- Behavioural layer + -- x = e + lb-assign : Variable → Expr → Label + + -- read t + lb-read : State → Label + + -- νr o@l(e) + lb-send : Channel → Operation → Location → Expr → Label + + -- r : o(x) + lb-store : Channel → Operation → Variable → Label + + -- (r, o)!x + lb-write : Channel → Operation → Variable → Label + + -- (r, o@l)?x + lb-read-write : Channel → Operation → Location → Variable → Label + +data _↝_∶_ : Behaviour → Behaviour → Label → Set where + b-assign : {x : Variable} {e : Expr} + → (x ≃ e) ↝ nil ∶ lb-assign x e + + b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable} + → wait r o l x ↝ nil ∶ lb-read-write r o l x + + b-oneway : {o : Operation} {x : Variable} {r : Channel} + → input (o [ x ]) ↝ nil ∶ lb-store r o x + + b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr} + → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e + + b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable} + → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e + + b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour} + → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x + + b-end-exec : {r : Channel} {o : Operation} {x : Variable} + → exec r o x nil ↝ nil ∶ lb-write r o x + + b-exec : {b b′ : Behaviour} {η : Label} {r : Channel} {o : Operation} {x : Variable} + → b ↝ b′ ∶ η + ---------------------------------- + → exec r o x b ↝ exec r o x b′ ∶ η + + b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label} + → b₁ ↝ b₁′ ∶ η + ----------------------------- + → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η + + b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label} + → b₁ ↝ b₁′ ∶ η + ---------------------------- + → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η + + b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label} + → b₁ ≡ b₂ + → b₂ ↝ b₂′ ∶ η + → b₁′ ≡ b₂′ + -------------- + → b₁ ↝ b₁′ ∶ η + + b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour} + → e ⟨ t ⟩≔ (constant (bool true)) + → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t + + b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour} + → e ⟨ t ⟩≔ (constant (bool false)) + → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t + + b-iteration : {e : Expr} {t : State} {b : Behaviour} + → e ⟨ t ⟩≔ (constant (bool true)) + → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t + + b-no-iteration : {e : Expr} {t : State} {b : Behaviour} + → e ⟨ t ⟩≔ (constant (bool false)) + → (while[ e ] b) ↝ nil ∶ lb-read t + + b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour} + → (ηⱼ , bⱼ) ∈-Vec choices + → input ηⱼ ↝ bⱼ′ ∶ η + → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η diff --git a/src/Interpreter.agda b/src/Interpreter.agda deleted file mode 100644 index 1b29e57..0000000 --- a/src/Interpreter.agda +++ /dev/null @@ -1,66 +0,0 @@ -module Interpreter where - -open import Type -open import Behaviour -open import Variable -open import Expr - - -data Label : Set where - -- Behavioural layer - -- x = e - lb-assign : Variable → Expr → Label - - -- read t - -- TODO: t - state of underlying process - lb-read : Label - - -- νr o@l(e) - lb-send : Channel → Operation → Location → Expr → Label - - -- r : o(x) - lb-store : Channel → Operation → Variable → Label - - -- (r, o)!x - lb-write : Channel → Operation → Variable → Label - - -- (r, o@l)?x - lb-read-write : Channel → Operation → Location → Variable → Label - - -- Service layer - -- τ - ls-interal : Label - - -- νr o@l(t) - ls-send : Channel → Operation → Location → Label - - -- νr o(t) - ls-store : Channel → Operation → Label - - -- (r, o)!t - ls-write : Channel → Operation → Label - - -- (r, o@l)?t - ls-read-write : Channel → Operation → Location → Label - -data _↝_∶_ : Behaviour → Behaviour → Label → Set where - b-assign : {x : Variable} {e : Expr} - → (x ≃ e) ↝ nil ∶ lb-assign x e - - b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable} - → wait r o l x ↝ nil ∶ lb-read-write r o l x - - b-oneway : {o : Operation} {x : Variable} {r : Channel} - → input (o [ x ]) ↝ nil ∶ lb-store r o x - - b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr} - → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e - - b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable} - → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e - - b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour} - → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x - - b-end-exec : {r : Channel} {o : Operation} {x : Variable} - → exec r o x nil ↝ nil ∶ lb-write r o x