1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
{-# OPTIONS --safe #-}
module Problem17 (Act : Set) where
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product hiding (map)
open import Data.Sum using (inj₁; inj₂)
open import Data.Unit
open import Function.Base using (id)
open import Relation.Binary.PropositionalEquality hiding ([_])
data Process : Set where
⟨_⟩ : Act → Process
skip : Process
abort : Process
-- not the normal semicolon, use \; and choose the correct option..
_;_ : Process → Process → Process
_+_ : Process → Process → Process
_∥_ : Process → Process → Process
infixr 60 _;_
infixr 70 _+_
infixr 80 _∥_
variable P P′ Q Q′ : Process
variable a b c x : Act
variable xs : List Act
NoPar : Process → Set
NoPar (P ; Q) = NoPar P × NoPar Q
NoPar (P + Q) = NoPar P × NoPar Q
NoPar (P ∥ Q) = ⊥
NoPar ⟨ _ ⟩ = ⊤
NoPar skip = ⊤
NoPar abort = ⊤
interleave : List Act → List Act → List (List Act)
interleave [] ys = [ ys ]
interleave xs [] = [ xs ]
interleave (x ∷ xs) (y ∷ ys) = map (x ∷_) (interleave xs (y ∷ ys)) ++ map (y ∷_) (interleave (x ∷ xs) ys)
⟦_⟧ : Process → List (List Act)
⟦ ⟨ a ⟩ ⟧ = [ [ a ] ]
⟦ skip ⟧ = [ [] ]
⟦ abort ⟧ = []
⟦ P + Q ⟧ = ⟦ P ⟧ ++ ⟦ Q ⟧
⟦ P ; Q ⟧ = concatMap (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧
⟦ P ∥ Q ⟧ = concatMap (λ p → concatMap (interleave p) ⟦ Q ⟧) ⟦ P ⟧
_≈_ : Process → Process → Set
P ≈ Q = ∀ xs → (xs ∈ ⟦ P ⟧ → xs ∈ ⟦ Q ⟧) × (xs ∈ ⟦ Q ⟧ → xs ∈ ⟦ P ⟧)
-- Helpers for dealing with sequential traces
;-trace : ∀ (P Q : Process) {xs ys} → xs ∈ ⟦ P ⟧ → ys ∈ ⟦ Q ⟧ → xs ++ ys ∈ ⟦ P ; Q ⟧
;-trace P Q {xs} xs∈⟦P⟧ ys∈⟦Q⟧ =
∈-concat⁺′ (∈-map⁺ (xs ++_) ys∈⟦Q⟧) (∈-map⁺ (λ p → map (p ++_) ⟦ Q ⟧) xs∈⟦P⟧)
;-trace⁻¹ :
∀ (P Q : Process) {xs} →
xs ∈ ⟦ P ; Q ⟧ → ∃₂ λ ys zs → xs ≡ ys ++ zs × ys ∈ ⟦ P ⟧ × zs ∈ ⟦ Q ⟧
;-trace⁻¹ P Q {xs} xs∈⟦P;Q⟧ with ∈-concat⁻′ (map (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧) xs∈⟦P;Q⟧
... | xss , xs∈xss , xss∈⟦P⟧++⟦Q⟧ with ∈-map⁻ (λ p → map (p ++_) ⟦ Q ⟧) xss∈⟦P⟧++⟦Q⟧
... | ys , ys∈⟦P⟧ , refl with ∈-map⁻ (ys ++_) xs∈xss
... | zs , zs∈⟦Q⟧ , refl = ys , zs , refl , ys∈⟦P⟧ , zs∈⟦Q⟧
-- Idea
-- Each trace has a canonical process---the list of actions. We can map a list
-- of possible traces to a canonical process by taking the sum of all individual
-- traces.
--
-- We show the canonical process for list of traces is correct (contains all
-- traces) and unique (contains only the desired traces).
canonical₁ : List Act → Process
canonical₁ [] = skip
canonical₁ (a ∷ as) = ⟨ a ⟩ ; canonical₁ as
canonical : List (List Act) → Process
canonical [] = abort
canonical (as ∷ ass) = canonical₁ as + canonical ass
canonical₁-correct : ∀ as → as ∈ ⟦ canonical₁ as ⟧
canonical₁-correct [] = here refl
canonical₁-correct (a ∷ as) = ;-trace ⟨ a ⟩ (canonical₁ as) (here refl) (canonical₁-correct as)
canonical₁-unique : ∀ as {xs} → xs ∈ ⟦ canonical₁ as ⟧ → xs ≡ as
canonical₁-unique [] (here prf) = prf
canonical₁-unique (a ∷ as) prf with ;-trace⁻¹ ⟨ a ⟩ (canonical₁ as) prf
... | .([ a ]) , xs , refl , here refl , prf = cong (a ∷_) (canonical₁-unique as prf)
canonical₁-NoPar : ∀ as → NoPar (canonical₁ as)
canonical₁-NoPar [] = _
canonical₁-NoPar (a ∷ as) = _ , canonical₁-NoPar as
canonical-correct : ∀ ass {as} → as ∈ ass → as ∈ ⟦ canonical ass ⟧
canonical-correct (as ∷ ass) (here refl) = ∈-++⁺ˡ (canonical₁-correct as)
canonical-correct (as ∷ ass) (there prf) = ∈-++⁺ʳ ⟦ canonical₁ as ⟧ (canonical-correct ass prf)
canonical-unique : ∀ ass {as} → as ∈ ⟦ canonical ass ⟧ → as ∈ ass
canonical-unique (as ∷ ass) prf with ∈-++⁻ ⟦ canonical₁ as ⟧ prf
... | inj₁ prf with refl ← canonical₁-unique as prf = here refl
... | inj₂ prf = there (canonical-unique ass prf)
canonical-NoPar : ∀ ass → NoPar (canonical ass)
canonical-NoPar [] = _
canonical-NoPar (as ∷ ass) = canonical₁-NoPar as , canonical-NoPar ass
goal : ∀ (P : Process) → ∃[ P′ ] (P′ ≈ P) × NoPar P′
goal P =
canonical ⟦ P ⟧
, (λ as → canonical-unique ⟦ P ⟧ , canonical-correct ⟦ P ⟧)
, canonical-NoPar ⟦ P ⟧
|
