FSM.agda

module FSM where

data Bool : Set where true false : Bool

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

----------------------------------------------------------------------

module ExplicitState (A : Set) (S : Set) where
  record FSM : Set where
    field
      initial : S
      final? : S → Bool
      next : S → A → S
  open FSM
  
  accept?' : FSM → S → List A → Bool
  accept?' m s [] = m .final? s 
  accept?' m s (a ∷ as) = accept?' m (m .next s a) as

  accept? : FSM → List A → Bool
  accept? m = accept?' m (m .initial)
  
  {- or w/o preserving the initial state:
  accept? : FSM → List A → Bool
  accept? m [] = m .final? (m .initial)
  accept? m (a ∷ as) = accept? (record m { initial = m .next (m . initial) a }) as
  -}

----------------------------------------------------------------------

module ImplicitState (A : Set) where
  record FSM : Set where
    coinductive
    field
      final? : Bool
      next : A → FSM
  open FSM
  
  accept? : FSM → List A → Bool
  accept? m [] = m .final?
  accept? m (a ∷ as) = accept? (m .next a) as
    
----------------------------------------------------------------------

{- 
Door Example FSM:
https://en.wikipedia.org/wiki/Finite-state_machine#/media/File:Fsm_Moore_model_door_control.svg
-}

data Action : Set where
  open! close! senseOpened! senseClosed! : Action

----------------------------------------------------------------------

module ExplicitStateExample where
  data Door : Set where
    closed opening opened closing : Door

  open ExplicitState Action Door

  inert? : Door → Bool
  inert? opened = true
  inert? closed = true
  inert? _ = false

  perform : Door → Action → Door
  perform closed open! = opening
  perform opening senseOpened! = opened
  perform opening close! = closing
  perform opened close! = closing
  perform closing open! = opening
  perform closing senseClosed! = closed
  perform x _ = x

  door : FSM
  door = record { initial = closed ; final? = inert? ; next = perform }

----------------------------------------------------------------------

module ImplicitStateExample where
  open ImplicitState Action
  open FSM

  closed opening opened closing : FSM
  closed .final? = true
  closed .next open! = opening
  closed .next _ = closed
  opening .final? = false
  opening .next senseOpened! = opened
  opening .next close! = closing
  opening .next _ = opening
  opened .final? = true
  opened .next close! = closing
  opened .next _ = opened
  closing .final? = false
  closing .next open! = opening
  closing .next senseClosed! = closed
  closing .next _ = closing

  door : FSM
  door = closed

----------------------------------------------------------------------