From 4b5225ee46f9d1ab2c832a043c5ccc7b73c5377f Mon Sep 17 00:00:00 2001
From: Ivan Perez <ivan.perezdominguez@nasa.gov>
Date: Thu, 7 May 2026 23:59:55 -0700
Subject: [PATCH 1/2] copilot-libraries: Add state machine module. Refs #728.

There is a need to have in Copilot a module that implements state
machines. Such functions have been useful in other projects, and they
could be added as part of Copilot's standard library so that they are
available to all users.

This commit adds a state machine module that enables simulating a state
machine using simple notation to describe the state machine.
---
 copilot-libraries/copilot-libraries.cabal     |  1 +
 .../src/Copilot/Library/StateMachines.hs      | 45 +++++++++++++++++++
 2 files changed, 46 insertions(+)
 create mode 100644 copilot-libraries/src/Copilot/Library/StateMachines.hs

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

From 32704d9c8ebb7bbed0a8c7d4a5bc9aeb15554079 Mon Sep 17 00:00:00 2001
From: Ivan Perez <ivan.perezdominguez@nasa.gov>
Date: Thu, 7 May 2026 23:59:55 -0700
Subject: [PATCH 2/2] copilot-libraries: Document changes in CHANGELOG. Refs
 #728.

---
 copilot-libraries/CHANGELOG | 1 +
 1 file changed, 1 insertion(+)

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)