mellon-core-0.8.0.1: Control physical access devices

Copyright(c) 2017 Quixoftic LLC
LicenseBSD3
MaintainerDrew Hess <dhess-src@quixoftic.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe
LanguageHaskell2010

Mellon.StateMachine

Contents

Description

The mellon-core state machine is the heart of the locking protocol.

A user of the mellon-core package is not expected to interact directly with the state machine, as the state machine is pure and is not capable of setting timers or performing IO actions on physical access devices. In mellon-core, those operations are the responsibility of controllers, and controllers are what users should interact with; see the Mellon.Controller module. However, understanding the state machine model is useful for understanding the behavior of a mellon-core application.

The state machine's behavior is quite simple:

  • The locked state has indefinite duration.
  • The unlocked state has an expiration date (a UTCTime). The controller will inform the state machine when this date has passed (since the state machine cannot keep time), at which point the state machine will advise the controller to lock the device again.
  • The user can (via the controller) send a lock command at any time, which will immediately cancel any unlock currently in effect.
  • If the user (via the controller) sends an unlock command while a previous unlock command is still in effect, then the unlock with the later expiration date "wins"; i.e., if the new expiration date is later than the current one, the unlock period is effectively extended, otherwise the device remains unlocked until the previously-specified date.

Synopsis

The state machine types

data Input Source #

The state machine's inputs, i.e., commands sent to the machine by a controller, either in response to a user's command, or in response to an expired timer.

Constructors

InputLockNow

Lock immediately, canceling any unlock currently in effect

InputUnlockExpired !UTCTime

An unlock command has expired. The unlock's expiration date is given by the specified UTCTime timestamp. Note that in the mellon-core protocol, these commands are only ever sent by the controller, which manages timed events, and never by the user directly.

InputUnlock !UTCTime

Unlock until the specified time. If no existing unlock command with a later expiration is currently in effect when this command is executed, the controller managing the state machine must schedule a lock to run at the specified time (i.e., when the unlock expires).

Instances

Eq Input Source # 

Methods

(==) :: Input -> Input -> Bool #

(/=) :: Input -> Input -> Bool #

Data Input Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Input -> c Input #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Input #

toConstr :: Input -> Constr #

dataTypeOf :: Input -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Input) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Input) #

gmapT :: (forall b. Data b => b -> b) -> Input -> Input #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Input -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Input -> r #

gmapQ :: (forall d. Data d => d -> u) -> Input -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Input -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Input -> m Input #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Input -> m Input #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Input -> m Input #

Read Input Source # 
Show Input Source # 

Methods

showsPrec :: Int -> Input -> ShowS #

show :: Input -> String #

showList :: [Input] -> ShowS #

Generic Input Source # 

Associated Types

type Rep Input :: * -> * #

Methods

from :: Input -> Rep Input x #

to :: Rep Input x -> Input #

type Rep Input Source # 
type Rep Input = D1 (MetaData "Input" "Mellon.StateMachine" "mellon-core-0.8.0.1-HF8JPohkodP7q0cj4udgCc" False) ((:+:) (C1 (MetaCons "InputLockNow" PrefixI False) U1) ((:+:) (C1 (MetaCons "InputUnlockExpired" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 UTCTime))) (C1 (MetaCons "InputUnlock" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 UTCTime)))))

data Output Source #

The state machine's outputs, i.e., commands to be performed by a controller.

It's reasonable to wonder why the OutputUnlock and OutputRescheduleLock values take a UTCTime parameter, when the State they're both always associated with (StateUnlocked) also takes a UTCTime parameter. Indeed, their time values will always be the same. However, this redundancy permits an interface to the state machine where the state is implicit (e.g., in a state monad) and the controller only "sees" the Output.

Constructors

OutputLock

Lock the device now

OutputUnlock !UTCTime

Unlock the device now and schedule a lock to run at the given time

OutputRescheduleLock !UTCTime

The date for the currently scheduled lock has changed. Reschedule it for the specified date. Note that the new date is guaranteed to be later than the previously-scheduled time.

OutputCancelLock

Cancel the currently scheduled lock and lock the device now

Instances

Eq Output Source # 

Methods

(==) :: Output -> Output -> Bool #

(/=) :: Output -> Output -> Bool #

Data Output Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Output -> c Output #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Output #

toConstr :: Output -> Constr #

dataTypeOf :: Output -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Output) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Output) #

gmapT :: (forall b. Data b => b -> b) -> Output -> Output #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Output -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Output -> r #

gmapQ :: (forall d. Data d => d -> u) -> Output -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Output -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Output -> m Output #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Output -> m Output #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Output -> m Output #

Read Output Source # 
Show Output Source # 
Generic Output Source # 

Associated Types

type Rep Output :: * -> * #

Methods

from :: Output -> Rep Output x #

to :: Rep Output x -> Output #

type Rep Output Source # 
type Rep Output = D1 (MetaData "Output" "Mellon.StateMachine" "mellon-core-0.8.0.1-HF8JPohkodP7q0cj4udgCc" False) ((:+:) ((:+:) (C1 (MetaCons "OutputLock" PrefixI False) U1) (C1 (MetaCons "OutputUnlock" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 UTCTime)))) ((:+:) (C1 (MetaCons "OutputRescheduleLock" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 UTCTime))) (C1 (MetaCons "OutputCancelLock" PrefixI False) U1)))

data State Source #

The state machine's states.

Constructors

StateLocked

The state machine is in the locked state

StateUnlocked !UTCTime

The state machine is unlocked until the specified date.

Instances

Eq State Source # 

Methods

(==) :: State -> State -> Bool #

(/=) :: State -> State -> Bool #

Data State Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> State -> c State #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c State #

toConstr :: State -> Constr #

dataTypeOf :: State -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c State) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c State) #

gmapT :: (forall b. Data b => b -> b) -> State -> State #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> State -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> State -> r #

gmapQ :: (forall d. Data d => d -> u) -> State -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> State -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> State -> m State #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> State -> m State #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> State -> m State #

Read State Source # 
Show State Source # 

Methods

showsPrec :: Int -> State -> ShowS #

show :: State -> String #

showList :: [State] -> ShowS #

Generic State Source # 

Associated Types

type Rep State :: * -> * #

Methods

from :: State -> Rep State x #

to :: Rep State x -> State #

type Rep State Source # 
type Rep State = D1 (MetaData "State" "Mellon.StateMachine" "mellon-core-0.8.0.1-HF8JPohkodP7q0cj4udgCc" False) ((:+:) (C1 (MetaCons "StateLocked" PrefixI False) U1) (C1 (MetaCons "StateUnlocked" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 UTCTime))))

The state machine implementation

transition :: State -> Input -> (Maybe Output, State) Source #

Run one iteration of the state machine.

Note that some transitions require no action by the controller, hence the first element of the returned pair (the Output value) is wrapped in Maybe.

Properties

transition StateLocked InputLockNow == (Nothing,StateLocked)
\date -> transition StateLocked (InputUnlockExpired date) == (Nothing,StateLocked)
\date -> transition StateLocked (InputUnlock date) == (Just $ OutputUnlock date,StateUnlocked date)
\date -> transition (StateUnlocked date) InputLockNow == (Just OutputCancelLock,StateLocked)
\date -> transition (StateUnlocked date) (InputUnlockExpired date) == (Just OutputLock,StateLocked)
\(date1, date2) -> date1 /= date2 ==> transition (StateUnlocked date1) (InputUnlockExpired date2) == (Nothing,StateUnlocked date1)
\date -> transition (StateUnlocked date) (InputUnlock date) == (Nothing,StateUnlocked date)
\(date1, date2) -> date2 > date1 ==> transition (StateUnlocked date1) (InputUnlock date2) == (Just $ OutputRescheduleLock date2,StateUnlocked date2)
\(date1, date2) -> not (date2 > date1) ==> transition (StateUnlocked date1) (InputUnlock date2) == (Nothing,StateUnlocked date1)