diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 49779ea5..745bb1b6 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,5 +1,6 @@ 2026-05-07 * Add stream analysis module. (#726) + * Add state machine module. (#728) 2026-03-07 * Version bump (4.7). (#714) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 14588731..e59ff32f 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -49,6 +49,7 @@ library , Copilot.Library.Clocks , Copilot.Library.LTL , Copilot.Library.PTLTL + , Copilot.Library.StateMachines , Copilot.Library.Statistics , Copilot.Library.RegExp , Copilot.Library.Utils diff --git a/copilot-libraries/src/Copilot/Library/StateMachines.hs b/copilot-libraries/src/Copilot/Library/StateMachines.hs new file mode 100644 index 00000000..37121b1a --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/StateMachines.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE ScopedTypeVariables #-} +-- | Simulate state machines using streams. +module Copilot.Library.StateMachines where + +import Copilot.Language (Stream, Typed, constant, ifThenElse, (&&), (++), (==)) +import Prelude hiding ((&&), (++), (==)) + +-- | A definition of a state machine where some elements are defined +-- as streams. +-- +-- A state machine is defined by an initial state, a final state, a no +-- transition stream (true when tere is no input coming in), a list of +-- transitions, and a bad state. +type StateMachine a = (a, a, Stream Bool, [(a, Stream Bool, a)], a) + +-- | Produce a stream that, at any given time, contains the current state of +-- the state machine. +stateMachine :: forall a . (Eq a, Typed a) => StateMachine a -> Stream a +stateMachine (initial, final, noInputData, transitions, bad) = state + where + state = ifThenElses transitions + previousState = [initial] ++ state + + ifThenElses :: [(a, Stream Bool, a)] -> Stream a + ifThenElses [] = + ifThenElse (previousState == constant final && noInputData) + (constant final) + (constant bad) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse + (previousState == constant s1 && i) + (constant s2) + (ifThenElses ss) + +-- | Produce a stream that, at any given time, contains the current state of +-- the state machine as the numeric representation of an enum. +stateMachineEnum :: (Eq b, Typed b, Num b, Enum a) + => StateMachine a + -> Stream b +stateMachineEnum (initial, final, noInputData, transitions, bad) = + stateMachine (fe initial, fe final, noInputData, transitionsE, fe bad) + where + transitionsE = map (\(s1, t, s2) -> (fe s1, t, fe s2)) transitions + fe = fromIntegral . fromEnum