Copyright	(c) 2018 Quixoftic LLC
License	BSD3
Maintainer	Drew Hess <dhess-src@quixoftic.com>
Stability	experimental
Portability	non-portable
Safe Haskell	Safe
Language	Haskell2010

Mellon.StateMachine

Contents

The state machine types
The state machine implementation

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 #
Methods readsPrec :: Int -> ReadS Input # readList :: ReadS [Input] # readPrec :: ReadPrec Input # readListPrec :: ReadPrec [Input] #
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.5-DnyB6oheJa3H3BKFM6HxYU" 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 #
Methods readsPrec :: Int -> ReadS Output # readList :: ReadS [Output] # readPrec :: ReadPrec Output # readListPrec :: ReadPrec [Output] #
Show Output Source #
Methods showsPrec :: Int -> Output -> ShowS # show :: Output -> String # showList :: [Output] -> ShowS #
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.5-DnyB6oheJa3H3BKFM6HxYU" 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 #
Methods readsPrec :: Int -> ReadS State # readList :: ReadS [State] # readPrec :: ReadPrec State # readListPrec :: ReadPrec [State] #
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.5-DnyB6oheJa3H3BKFM6HxYU" 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)