copilot-libraries: Add state machine module

Description

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.

Type

Feature: Add new module with state machine functionality.

Additional context

None.

Requester

Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

copilot-libraries includes a state machine module that provides ways to simulate a state machine using Copilot.

Desired result

copilot-libraries includes a state machine module that provides ways to simulate a state machine using Copilot.

Proposed solution

Add a new module to copilot-libraries that includes functions to simulate a state machine.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 4.7.1.

Fix assigned to: @ivanperez-keera .

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

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

Implementor: Solution implemented, review requested.

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

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

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

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/278086230

The solution proposed produces the expected result. Details:
The following Dockerfile uses the new state machine simulation capabilities to simulate several steps of a state machine and check that it matches the expectation of how it should transition between states, after which it prints the message "Success":

--- Dockerfile-verify-728
FROM ubuntu:jammy

WORKDIR /root
SHELL ["/bin/bash", "-c"]

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config \
      z3

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

RUN ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

ADD Diagram.hs /tmp/
ADD expectation /tmp/
ADD main.c /tmp/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && cabal v1-exec -- runhaskell /tmp/Diagram.hs \
  && gcc /tmp/main.c monitor.c -I$PWD -o main \
  && ./main | sed -n 's/.*new state: \([0-9]\+\).*/\1/p' | paste -sd' ' - > /tmp/output \
  && diff /tmp/expectation /tmp/output \
  && echo "Success"

--- Diagram.hs
module Diagram (main) where

import Prelude hiding ((&&), (/=), (<), (<=), (>), (>=))

import Copilot.Compile.C99
import Copilot.Language
import Copilot.Library.StateMachines
import Language.Copilot

main :: IO ()
main = reify spec >>= compile "monitor"

spec :: Spec
spec = do
  trigger "handler" true [ arg stateMachineS ]

stateMachineS :: Stream Word8
stateMachineS = stateMachine stateMachine1

stateMachine1 :: StateMachine Word8
stateMachine1 = (initialState, finalState, noInput, transitions, badState)
  where
    initialState :: Word8
    initialState = 0

    finalState :: Word8
    finalState = 2

    noInput :: Stream Bool
    noInput = false

    transitions :: [(Word8, Stream Bool, Word8)]
    transitions = [ (0, input >= 120 && input <= 180, 0)
                  , (0, input > 180, 1)
                  , (1, input <= 180, 0)
                  , (1, input > 180, 1)
                  , (0, input < 120, 2)
                  , (2, input >= 120, 0)
                  , (2, input < 120, 2)
                  ]

    badState :: Word8
    badState = 3

input :: Stream Word8
input = extern "input" Nothing

--- expectation
0 1 1 0 2 2 0

--- main.c
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>

#include "monitor.h"

uint8_t  input     = 150;
uint8_t  state     = 0;
uint64_t iteration = 0;

/**
 * Function called by the state machine to communicate its expected state.
 *
 * @param handler_arg0 The new state of the state machine.
 */
void handler(uint8_t handler_arg0)
{
  printf("[Calculated] Previous state: %d, input: %d, new state: %d\n",
         state, input, handler_arg0);

  iteration++;

  state = handler_arg0;
}

/**
 * Report the current, internally calculated input and state, and call the
 * state machine to calculate the new state. The function <code>step</code>
 * calls <code>handler</code> at each step.
 */
void next()
{
  printf("Executing step %ld: input %d, state %d\n", iteration, input, state);
  step();
  printf("--------------------------------------\n");
}

void main (int argc, char **argv)
{
  // We step with initial state 0 and input 150. The machine should remain in
  // state 0.
  next();

  // We step again with input greater than 180. The machine should now
  // transition to state 1.
  input = 185;
  next();

  // We step again with no changes. The machine should remain in state 1.
  next();

  // We step again with input lower than or equal to 180. The machine should
  // now transition to state 0.
  input = 110;
  next();

  // We step again with no changes. The machine should transition to state 2.
  next();

  // We step again with no changes. The machine should remain in state 2.
  next();

  // We step again with an input greater than 180. The machine should now
  // transition to state 0.
  input = 185;
  next();
}

Command (substitute variables based on new path after merge):

$ docker run -e REPO=https://github.com/ivanperez-keera/copilot -e NAME=copilot -e COMMIT=32704d9c8ebb7bbed0a8c7d4a5bc9aeb15554079 copilot-verify-728

Implementation is documented. Details:
The new module is documented.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; change does not affect existing examples.
Author is internal or has provided signed CLA.
Required version bumps are evaluated. Details:
Bump not needed; change adds definitions but does not alter existing ones.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-state-machines'. Close Copilot-Language#728.

Navigation Menu

Repository navigation

`copilot-libraries`: Add state machine module #728

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-libraries: Add state machine module #728

Description

Activity

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-libraries`: Add state machine module #728