IpState.agda

open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import RSC

-- Basic data-types

data AssignState : Set where
  Available : AssignState
  Assigned  : AssignState
  ToRecycle : AssignState
  ToDisable : AssignState
  Disabled  : AssignState

UserId : Set
UserId = ℕ

data User : Set where
  NoUser   : User
  JustUser : UserId → User

someOne : ℕ
someOne = zero

IpState : Set
IpState = AssignState × User

_∧_ : Set → Set → Set
_∧_ = _×_

conj : {A : Set} {B : Set} → A → B → A ∧ B
conj = _,_

_∨_ : Set → Set → Set
_∨_ = _⊎_

-- Inductive specifications

infix 4 _⟹_

-- state transition
data _⟹_ : IpState → IpState → Set where
  AssignChunk     :                 (Available , NoUser)       ⟹ (Assigned  , NoUser)
  AssignUser      : ∀ (uid : _) → (Assigned  , NoUser)       ⟹ (Assigned  , JustUser uid)
  AssignTimeout   : ∀ (uid : _) → (Assigned  , JustUser uid) ⟹ (ToRecycle , JustUser uid)
  DisableAvail    :                 (Available , NoUser)       ⟹ (Disabled  , NoUser)
  DisableAssigned : ∀ (uid : _) → (Assigned  , JustUser uid) ⟹ (ToDisable , JustUser uid)
  DisableTimedout : ∀ (uid : _) → (ToRecycle , JustUser uid) ⟹ (ToDisable , JustUser uid)
  UnassignDisable : ∀ (uid : _) → (ToDisable , JustUser uid) ⟹ (Disabled  , NoUser)
  {- this transition cause loop -}
  Unassign        : ∀ (uid : _) → (ToRecycle , JustUser uid) ⟹ (Available , NoUser)

WellFormedTransition : IpState → IpState → Set
WellFormedTransition = _⟹_

transitionStateUpdate : ∀ {s t} → s ⟹ t → s ≢ t
transitionStateUpdate = update
  where
    update  : ∀ {s t} → s ⟹ t → s ≢ t
    update  AssignChunk          ()
    update (AssignUser uid)      ()
    update (AssignTimeout uid)   ()
    update  DisableAvail         ()
    update (DisableAssigned uid) ()
    update (DisableTimedout uid) ()
    update (UnassignDisable uid) ()
    update (Unassign uid)        ()

data WS : IpState → Set where
  IpUnassigned     :                 WS (Available , NoUser)
  IpChunkAssigned  :                 WS (Assigned  , NoUser)
  IpUserAssigned   : ∀ (uid : _) → WS (Assigned  , JustUser uid)
  IpTimedout       : ∀ (uid : _) → WS (ToRecycle , JustUser uid)
  IpDisabled       :                 WS (Disabled  , NoUser)
  IpToDisable      : ∀ (uid : _) → WS (ToDisable , JustUser uid)

WellFormedState : IpState → Set
WellFormedState = WS

transitionWS : ∀ {s t} → s ⟹ t → WS s ∧ WS t
transitionWS = tws
  where
    tws : ∀ {s t} → s ⟹ t → WS s ∧ WS t
    tws  AssignChunk          = IpUnassigned         , IpChunkAssigned
    tws (AssignUser uid)      = IpChunkAssigned      , (IpUserAssigned uid)
    tws (AssignTimeout uid)   = (IpUserAssigned uid) , (IpTimedout uid)
    tws  DisableAvail         = IpUnassigned         , IpDisabled
    tws (DisableAssigned uid) = (IpUserAssigned uid) , (IpToDisable uid)
    tws (DisableTimedout uid) = (IpTimedout uid)     , (IpToDisable uid)
    tws (UnassignDisable uid) = (IpToDisable uid)    , IpDisabled
    tws (Unassign uid)        = (IpTimedout uid)     , IpUnassigned

data StateStart : IpState → Set where
  AvailableIsStart : StateStart (Available , NoUser)

startWS : ∀ {s} → StateStart s → WS s
startWS AvailableIsStart = IpUnassigned

data StateEnd : IpState → Set where
  DisabledIsEnd : StateEnd (Disabled , NoUser)

endWS : ∀ {s} → StateEnd s → WS s
endWS DisabledIsEnd = IpDisabled

endDoesNotProgress : ∀ {es s} → StateEnd es → ¬ es ⟹ s
endDoesNotProgress DisabledIsEnd ()

fromWellFormedState :
  ∀ {s1} →
  WS s1   →
  (∃ λ s2 → WS s2 ∧ (s1 ⟹ s2)) ∨ StateEnd s1
fromWellFormedState = from
  where
    from :
      ∀ {s1} →
      WS s1   →
      (∃ λ s2 → WS s2 ∧ (s1 ⟹ s2)) ∨ StateEnd s1
    from  IpUnassigned    =
      inj₁ (_ , conj  IpChunkAssigned          AssignChunk)
    from  IpChunkAssigned =
      inj₁ (_ , conj (IpUserAssigned someOne) (AssignUser someOne))
    from (IpUserAssigned uid) =
      inj₁ (_ , conj (IpTimedout uid)         (AssignTimeout uid))
    from (IpTimedout     uid) =
      inj₁ (_ , conj (IpUnassigned)           (Unassign uid))
    from  IpDisabled =
      inj₂ DisabledIsEnd
    from (IpToDisable    uid) =
      inj₁ (_ , conj IpDisabled               (UnassignDisable uid))

toWellFormedState :
  ∀ {s2} →
  WS s2   →
  (∃ λ s1 → WS s1 ∧ (s1 ⟹ s2))
toWellFormedState = to
  where
    to :
      ∀ {s2} →
      WS s2   →
      (∃ λ s1 → WS s1 ∧ (s1 ⟹ s2))
    to IpUnassigned =
      _ , conj (IpTimedout someOne)  (Unassign someOne)
    to IpChunkAssigned =
      _ , conj  IpUnassigned          AssignChunk
    to (IpUserAssigned uid) =
      _ , conj  IpChunkAssigned      (AssignUser uid)
    to (IpTimedout     uid) =
      _ , conj (IpUserAssigned uid)  (AssignTimeout uid)
    to IpDisabled =
      _ , conj (IpToDisable someOne) (UnassignDisable someOne)
    to (IpToDisable    uid) =
      _ , conj (IpTimedout     uid)  (DisableTimedout uid)

wellFormedStateTransition :
  ∀ s →
  WS s →
  (∃ λ t → WS t ∧ ((s ⟹ t) ∨ (t ⟹ s)))
wellFormedStateTransition s ws =
     _ , conj (proj₁ to₂) (inj₂ (proj₂ to₂))
  where
    to : ∃ λ t → WS t ∧ (t ⟹ s)
    to = toWellFormedState ws

    to₂ = proj₂ (toWellFormedState ws)

-- Reflexive Step Closure of Transition

transitionPreserveWellFormedState : preserve1 _⟹_ WS
transitionPreserveWellFormedState _ _ tr _ = proj₂ (transitionWS tr)

infix 4 _⟹*_

_⟹*_ : IpState → IpState → Set
_⟹*_ = ReflStepClosure WellFormedTransition

Reachable : IpState → Set
Reachable s = ∃ λ ss → StateStart ss ∧ (ss ⟹* s)

wellFormedStateReachable : ∀ s → WS s → Reachable s
wellFormedStateReachable = wsr
  where
    wsr : ∀ s → WS s → Reachable s
    wsr .(Available , NoUser) IpUnassigned =
      _ , conj AvailableIsStart (RscRefl _)
    wsr .(Assigned , NoUser) IpChunkAssigned =
      _ , conj AvailableIsStart (RscStep _ _ _ AssignChunk (RscRefl _))
    wsr .(Assigned , JustUser uid) (IpUserAssigned uid) =
      _ , conj AvailableIsStart (RscStep _ _ _ AssignChunk
                                (RscStep _ _ _ (AssignUser uid) (RscRefl _)))
    wsr .(ToRecycle , JustUser uid) (IpTimedout uid) =
      _ , conj AvailableIsStart (RscStep _ _ _ AssignChunk
                                (RscStep _ _ _ (AssignUser uid)
                                (RscStep _ _ _ (AssignTimeout uid) (RscRefl _))))
    wsr .(Disabled , NoUser) IpDisabled =
      _ , conj AvailableIsStart (RscStep _ _ _ DisableAvail (RscRefl _))
    wsr .(ToDisable , JustUser uid) (IpToDisable uid) =
      _ , conj AvailableIsStart (RscStep _ _ _ AssignChunk
                                (RscStep _ _ _ (AssignUser uid)
                                (RscStep _ _ _ (DisableAssigned uid) (RscRefl _))))

reachableWellFormedState : ∀ s → Reachable s → WS s
reachableWellFormedState s (_ , (AvailableIsStart , rsc)) =
  rscPreservation _⟹_ WS transitionPreserveWellFormedState _ s rsc IpUnassigned

wellFormedReachableToEnd :
  ∀ s es     →
  WS s        →
  StateEnd es →
  s ⟹* es
wellFormedReachableToEnd = wsre
  where
    wsre : ∀ s es → WS s → StateEnd es → s ⟹* es
    wsre .(Available , NoUser)       _  IpUnassigned        DisabledIsEnd =
      RscStep _ _ _ DisableAvail (RscRefl _)
    wsre .(Assigned , NoUser)        _  IpChunkAssigned     DisabledIsEnd =
      RscStep _ _ _ (AssignUser someOne)
      (RscStep _ _ _ (DisableAssigned someOne)
       (RscStep _ _ _ (UnassignDisable someOne) (RscRefl _)))
    wsre .(Assigned , JustUser uid)  _ (IpUserAssigned uid) DisabledIsEnd =
      RscStep _ _ _ (DisableAssigned uid)
      (RscStep _ _ _ (UnassignDisable uid) (RscRefl _))
    wsre .(ToRecycle , JustUser uid) _ (IpTimedout uid)     DisabledIsEnd =
      RscStep _ _ _ (DisableTimedout uid)
      (RscStep _ _ _ (UnassignDisable uid) (RscRefl _))
    wsre .(Disabled , NoUser)        _  IpDisabled          DisabledIsEnd =
      RscRefl _
    wsre .(ToDisable , JustUser uid) _ (IpToDisable uid)    DisabledIsEnd =
      RscStep _ _ _ (UnassignDisable uid) (RscRefl _)

wsReachable : ∀ s → WS s → Reachable s
wsReachable = wellFormedStateReachable

transitionStateReachable :
  ∀ s t  →
  s ⟹ t →
  Reachable s ∧ Reachable t
transitionStateReachable = tsr
  where
    tsr : ∀ s t  → s ⟹ t → Reachable s ∧ Reachable t
    tsr .(Available , NoUser)       .(Assigned , NoUser)         AssignChunk =
      conj (wsReachable _ IpUnassigned) (wsReachable _ IpChunkAssigned)
    tsr .(Assigned , NoUser)        .(Assigned , JustUser uid)  (AssignUser uid) =
      conj (wsReachable _ IpChunkAssigned) (wsReachable _ (IpUserAssigned uid))
    tsr .(Assigned , JustUser uid)  .(ToRecycle , JustUser uid) (AssignTimeout uid) =
      conj (wsReachable _ (IpUserAssigned uid)) (wsReachable _ (IpTimedout uid))
    tsr .(Available , NoUser)       .(Disabled , NoUser)         DisableAvail =
      conj (wsReachable _ IpUnassigned) (wsReachable _ IpDisabled)
    tsr .(Assigned , JustUser uid)  .(ToDisable , JustUser uid) (DisableAssigned uid) =
      conj (wsReachable _ (IpUserAssigned uid)) (wsReachable _ (IpToDisable uid))
    tsr .(ToRecycle , JustUser uid) .(ToDisable , JustUser uid) (DisableTimedout uid) =
      conj (wsReachable _ (IpTimedout uid)) (wsReachable _ (IpToDisable uid))
    tsr .(ToDisable , JustUser uid) .(Disabled , NoUser)        (UnassignDisable uid) =
      conj (wsReachable _ (IpToDisable uid)) (wsReachable _ IpDisabled)
    tsr .(ToRecycle , JustUser uid) .(Available , NoUser)       (Unassign uid) =
      conj (wsReachable _ (IpTimedout uid)) (wsReachable _ IpUnassigned)

reachableTransitionState :
  ∀ s        →
  Reachable s →
  ∃ λ t → WS t ∧ ((s ⟹ t) ∨ (t ⟹ s))
reachableTransitionState s r =
  wellFormedStateTransition s (reachableWellFormedState s r)

progress : ∀ s1 → Reachable s1 →
           (∃ λ s2 → WS s2 ∧ (s1 ⟹ s2)) ∨ StateEnd s1
progress s1 r = fromWellFormedState (reachableWellFormedState _ r)

endTransitionsIsRefl :
  ∀ es s              →
  StateEnd es          →
  ∀ (ess : es ⟹* s) →
  (ReflRsc _⟹_ es s ess)
endTransitionsIsRefl _ _ DisabledIsEnd (RscRefl .(Disabled , NoUser)) = RscIsRefl
endTransitionsIsRefl _ _ DisabledIsEnd (RscStep .(Disabled , NoUser) y _ () ess)

∃-loop : IpState → Set
∃-loop from = ∃ (λ s → ∃ λ (c : from ⟹* s) → RscLoop _⟹_ c)

fromStartHasLoop : ∃-loop (Available , NoUser)
fromStartHasLoop =
  (Available , NoUser) ,
  (RscStep _ _ _ AssignChunk
   (RscStep _ _ _ (AssignUser someOne)
    (RscStep _ _ _ (AssignTimeout someOne)
     (RscStep _ _ _ (Unassign someOne)
      (RscRefl _))))) ,
  RscHasLoop AssignChunk _
   (RscTailHas (λ ()) _ (AssignUser someOne)
    (RscTailHas (λ ()) _ (AssignTimeout someOne)
     (RscTailHas (λ ()) _ (Unassign someOne)
      (RscHeadHas _ RscHeadReflIs))))

disabledDoesNotHaveLoop : ¬ ∃-loop (Disabled , NoUser)
disabledDoesNotHaveLoop (_ , (RscRefl (Disabled , NoUser)) , ())
disabledDoesNotHaveLoop (_ , (RscStep (Disabled , NoUser) y _ () c) , _)

toDisableDoesNotHaveLoop : ∀ uid → ¬ ∃-loop (ToDisable , JustUser uid)
toDisableDoesNotHaveLoop uid (_ , (RscRefl (ToDisable , JustUser .uid)) , ())
toDisableDoesNotHaveLoop uid
  (_ ,
  (RscStep
    (ToDisable , JustUser .uid)
    (Disabled , NoUser) _ _
    (RscStep (Disabled , NoUser) _ _ () _)) ,
  (RscHasLoop
    (UnassignDisable .uid)
    (RscStep (Disabled , NoUser) _ _ () _)
    (RscTailHas _ _ () _)) )

RSC.agda

module RSC where

import Level as LV using (zero)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≢_)

-- Reflexive Step Closure

relation : ∀ {a} → Set a → Set _
relation X = Rel X LV.zero

preserve1 : {X : Set} → relation X → (X → Set) → Set
preserve1 {X} R P = ∀ (x y : X) → R x y → P x → P y

data ReflStepClosure {X : Set} (R : relation X) : X → X → Set where
  RscRefl : ∀ (x : X) →
            ReflStepClosure R x x
  RscStep : ∀ (x y z : X) →
            R x y          →
            ReflStepClosure R y z →
            ReflStepClosure R x z

rscR : ∀ {X : Set} (R : relation X) (x y : X) →
       R x y                                   →
       ReflStepClosure R x y
rscR _ x y r = RscStep x y y r (RscRefl y)

rscTrans : ∀ {X : Set} (R : relation X) (x y z : X) →
           ReflStepClosure R x y                     →
           ReflStepClosure R y z                     →
           ReflStepClosure R x z
rscTrans _ x .x z (RscRefl .x)                 cxz =
  cxz
rscTrans _ x y z  (RscStep .x x₁ .y rxx₁ cx₁y) cyz =
  RscStep x x₁ z rxx₁ (rscTrans _ x₁ y z cx₁y cyz)

rscPreservation :
  ∀ {X : Set} (R : relation X) (P : X → Set) →
  preserve1 R P                                →
  ∀ (x y : X)                                 →
  ReflStepClosure R x y                        →
  P x → P y
rscPreservation R P p1 x .x (RscRefl .x)                 px =
  px
rscPreservation R P p1 x  y (RscStep .x x₁ .y rxx₁ cx₁y) px =
  rscPreservation R P p1 x₁ y cx₁y (p1 x x₁ rxx₁ px)

data ReflRsc {X : Set} (R : relation X) (x : X) :
  ∀ (y : X) → ReflStepClosure R x y → Set where
  RscIsRefl : ReflRsc R x x (RscRefl x)

data RscHeadIs {X : Set} (R : relation X) (x : X) :
  ∀ (z : X) → ReflStepClosure R x z → Set where
  RscHeadReflIs : RscHeadIs R x x (RscRefl x)
  RscHeadStepIs :
    ∀ {y z} (r : R x y)        →
    (c : ReflStepClosure R y z) →
    RscHeadIs R x z (RscStep x y z r c)

data RscHas {X : Set} (R : relation X) (y : X) :
  ∀ {x z : X} → ReflStepClosure R x z → Set where
  RscHeadHas :
    {z : X} (hrsc : ReflStepClosure R y z) →
    RscHeadIs R y z hrsc                   →
    RscHas R y hrsc
  RscTailHas :
    {x x₁ z : X}                    →
    x ≢ y                           →
    (trsc : ReflStepClosure R x₁ z) →
    (r₁ : R x x₁)                   →
    RscHas R y trsc                 →
    RscHas R y (RscStep x x₁ z r₁ trsc)

data RscLoop {X : Set} (R : relation X) :
  ∀ {x z : X} → ReflStepClosure R x z → Set where
  RscHasLoop :
    {x y z : X}                    →
    (r : R x y)                    →
    (hasC : ReflStepClosure R y z) →
    RscHas R x hasC                →
    RscLoop R (RscStep x y z r hasC)