copilot-libraries: Add state machine module. Refs #728.

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)

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

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