Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid larrytheliquid/FSM.agda
Last active Jan 5, 2019

Embed
What would you like to do?
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
----------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.