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

[ivanperez-keera]

Add module implementing state machines and allowing them to be simulated in Copilot, as prescribed in the solution proposed for #728.

[ivanperez-keera]

Change Manager: The definitions in the module lack documentation.

[ivanperez-keera]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

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.