Finite State Machines in Copilot

[liamdiprose]

Is Copilot suitable for implementing Finite State Machines?

[ivanperez-keera]

Yes. We have done it before. Can you describe your use case more?

[liamdiprose]

Thank you for your reply. For an example, consider an air-lock on a spacecraft, two doors and an intermediate chamber. How does Copilot remember if the chamber is pressurizing or depressurizing?

You could have the trigger functions modify a state global variable. I was wondering if there was a better approach, say with Temporal Logic?

Edit: the use case is a charging protocol on an electric vehicle (i.e. voltage instead of pressure).

[ivanperez-keera]

I was hoping to have more time to clean this and improve it, but you've been patiently waiting for over 2 months now, so I'd rather keep things moving than stall this forever. Perfect is the enemy of good!

You can write state machines manually as follows. Let's imagine that you have an incoming stream of inputs with possible values 1, 2 and 3 ONLY:

input :: Stream Word8
input = extern "input" (Just [3,1,2,2,1,3,3,3,3,3])

The values in the list are just for testing purposes.

You can implement the following state machine:

graph TD;
    1-->|2|2;
    2-->|2|3;
    3-->|2|3;
    3-->|1|4;
    4-->|3|4;

Loading

With the code:

state :: Stream Word8
state = [1] ++ (ifThenElse (state == 1 && input == 1) 2
                (ifThenElse (state == 2 && input == 2) 3
                (ifThenElse (state == 3 && input == 2) 3
                (ifThenElse (state == 3 && input == 1) 4
                (ifThenElse (state == 4 && input == 3) 4 state)))))

More generally, here are three possible ways of implementing state machines, depending on whether you consider the existence of a state denoting an error or not, and whether you want all inputs to produce a transition or not.

{-# LANGUAGE DataKinds #-}
import Copilot.Language hiding (max, min)
import Language.Copilot hiding (max, min)
import Prelude          hiding ( not, until, (&&), (++), (/=), (==), (||), mod, (>), max, min)

-- Initial state, final state, states and transitions, wrong state indicator
type StateMachine = ( Word8, Word8, [Word8], [(Word8, Word8, Word8)], Word8 )

stateMachine :: StateMachine -> Stream Word8 -> Stream Word8
stateMachine (initialState, finalState, inputs, transitions, badState) inputSignal = state
  where
    state = [initialState] ++ ifThenElses inputs finalState transitions badState inputSignal

    ifThenElses :: [Word8] -> Word8 -> [(Word8, Word8, Word8)] -> Word8 -> Stream Word8 -> Stream Word8
    ifThenElses inputs finalState [] badState inputSignal =
      ifThenElse
        (state == constant finalState && noneOf inputSignal inputs)
        (constant finalState)
        (constant badState)

    ifThenElses inputs finalState ((s1,i,s2):ss) badState inputSignal =
      ifThenElse
        (state == constant s1 && inputSignal == constant i)
        (constant s2)
        (ifThenElses inputs finalState ss badState inputSignal)


-- Initial state, final state, transitions
type StateMachineG = ( Word8, Word8, [(Word8, Stream Bool, Word8)] )

stateMachineG :: StateMachineG -> Stream Word8
stateMachineG (initialState, finalState, transitions) = state
  where
    state = [initialState] ++ ifThenElses finalState transitions

    ifThenElses :: Word8 -> [(Word8, Stream Bool, Word8)] -> Stream Word8
    ifThenElses finalState [] = constant finalState

    ifThenElses finalState ((s1,i,s2):ss) =
      ifThenElse
        (state == constant s1 && i)
        (constant s2)
        (ifThenElses finalState ss)

-- Initial state, final state, no transition signal, transitions, bad state
type StateMachineGF = ( Word8, Word8, Stream Bool, [(Word8, Stream Bool, Word8)], Word8)

stateMachineGF :: StateMachineGF -> Stream Word8
stateMachineGF (initialState, finalState, noInputData, transitions, badState) = state
  where
    state = [initialState] ++ ifThenElses transitions

    ifThenElses :: [(Word8, Stream Bool, Word8)] -> Stream Word8
    ifThenElses [] =
      ifThenElse (state == constant finalState && noInputData)
        (constant finalState)
        (constant badState)

    ifThenElses ((s1,i,s2):ss) =
      ifThenElse (state == constant s1 && i) (constant s2) (ifThenElses ss)

noneOf :: Stream Word8 -> [Word8] -> Stream Bool
noneOf input [] = true
noneOf input (x:xs) = input /= constant x && noneOf input xs

You can use them as follows:

-- Using our API
stateMachine1 :: Stream Word8
stateMachine1 = stateMachine (initialState, finalState, validInputs, transitions, badState) input
  where
    initialState :: Word8
    initialState = 1

    finalState :: Word8
    finalState = 4

    validInputs :: [Word8]
    validInputs = [1, 2]

    badState :: Word8
    badState = 5

    transitions = [ (1, 1, 2)
                  , (2, 2, 3)
                  , (3, 2, 3)
                  , (3, 1, 4)
                  ]

-- Using our API
stateMachine1G :: Stream Word8
stateMachine1G = stateMachineG (initialState, finalState, transitions)
  where
    initialState :: Word8
    initialState = 1

    finalState :: Word8
    finalState = 4

    transitions = [ (1, input == 1, 2)
                  , (2, input == 2, 3)
                  , (3, input == 2, 3)
                  , (3, input == 1, 4)
                  ]

-- Using our API
stateMachine1GF :: Stream Word8
stateMachine1GF = stateMachineGF (initialState, finalState, noInputs, transitions, badState)
  where
    initialState :: Word8
    initialState = 1

    finalState :: Word8
    finalState = 4

    noInputs :: Stream Bool
    noInputs = noneOf input [1, 2]

    transitions = [ (1, input == 1, 2)
                  , (2, input == 2, 3)
                  , (3, input == 2, 3)
                  , (3, input == 1, 4)
                  ]

    badState :: Word8
    badState = 5

A good outcome of this discussion would be to extend copilot-libraries to support state machines.

[ivanperez-keera]

Before immediately including this, perhaps it would pay off to 1) pick a representation that allows us to analyze the state machine first and ensure it's defined correctly, and 2) pick a Copilot implementation that generates more optimal code.

EDIT: By representation, I mean a datatype.

[liamdiprose]

I was very glad to see your reply. Thank you very much for these examples, they're gold to someone just starting out with haskell.

In my use case, it turns out the FSM is managed by another controller and we just need to track its state and do stuff when some transitions occur. So the Copilot code turned out to be very simple; mostly externs and boolean operations.

Are there any downsides to tracking the state within Copilot, as opposed to updating a byte in the trigger functions? What if we want to resume the FSM from flash memory? Is the step() function normally stateless? My guess at the upside is the FSM operation can be proven easier?

[ivanperez-keera]

So the Copilot code turned out to be very simple; mostly externs and boolean operations.

Great!

Are there any downsides to tracking the state within Copilot, as opposed to updating a byte in the trigger functions?

What do you mean by "Updating a byte in the trigger function"?

What if we want to resume the FSM from flash memory?

This presents an interesting use case that, to the best of my knowledge, has never been studied within Copilot. My first thought is that it may be possible by enclosing any stateful streams in an ifThenElse as follows:

ifThenElse
  reset          -- condition
  initialValue   -- then branch
  normalBehavior -- else branch

The initial example I wrote could be extended with a reset or re-read from memory setting as follows:

state :: Stream Word8
state = [1] ++ (ifThenElse reset savedState
                (ifThenElse (state == 1 && input == 1) 2
                (ifThenElse (state == 2 && input == 2) 3
                (ifThenElse (state == 3 && input == 2) 3
                (ifThenElse (state == 3 && input == 1) 4
                (ifThenElse (state == 4 && input == 3) 4 state))))))

reset :: Stream Bool
reset = extern "reset" Nothing

savedState :: Stream Word8
savedState = extern "saved_state" Nothing

The idea being that, when you want to resume from Flash memory, you just need to set the saved state in a global saved_state, set reset to true, and then call step().

Is the step() function normally stateless?

In general, you cannot assume that successive calls to step() are stateless. Each call advances streams one step, and they can refer to past values, so they can be stateful. This is a property of all stream-based or reactive languages (e.g., FRP).

My guess at the upside is the FSM operation can be proven easier?

You'd have a guarantee that the code generated is hard realtime.

You might also be able to prove certain properties of your FSM if you write it in Copilot, by leveraging the facilities of copilot-theorem, but I haven't done it. I'd be interested to see which properties you might want to prove.

You could of course define FSMs in Haskell using an existing library or custom representation, prove whatever you want statically, and then synthesize a Copilot FSM.

If you are operating in a safety-critical environment, then I'd suggest going down the route of trying to prove your FSM correct.

[liamdiprose]

Thank you for your answers. Understanding Copilot as a FRP is really cool and it makes a lot more sense for implementing FSMs than what I led myself to believe. I'm looking forward to using and further understanding these FSM APIs you've shared here.

This question might on a bit of a tangent: is it possible/advisable to map Stream Word8 to Haskell's data types? (e.g. encode a state with Idle instead of 1)?

[ivanperez-keera]

We've historically used integers and constants instead of enums. You can already use them to some extent, so long as you reduce the final result to word/ints using fromEnum and toEnum.

I suspect extending Copilot to support any Enums would be simple; you'd mainly need to know what underlying type can be used to represent the enum based on its size. I'd have to look into it in more detail. Related to #36, #58.

Otherwise, how is the FSM work going?

[ivanperez-keera]

Circling back. Any updates, @liamdiprose ?

[liamdiprose]

Hey @ivanperez-keera,

It pains me to say this, but I haven't made any progress because the client has settled with IQANdesign for now. I haven't been able to convince them of the importance of verified, portable code.

I am considering using Copilot for my next project to interpret user-customizable control-flow models. However, my focus has been on the lower levels so far.

I've just looked back over your FSM API proposal and your post made a lot more sense to me this time. I can't think of anything else it could need. Does it handle nesting? Clock delays? Preemptive interruption? Is it an RTOS? 🦋

[ivanperez-keera]

It pains me to say this, but I haven't made any progress because the client has settled with IQANdesign for now. I haven't been able to convince them of the importance of verified, portable code.

That's absolutely ok. On the one hand, it may just be a better fit for their use case, and that's understandable. On the other, knowing more about this could help us improve in the future.

Has the reasoning behind this been one of user experience? Documentation? Anything else?

For what is worth, I've worked on automatically transforming SysML diagrams to Haskell code. I imagine IQANdesign's format must be different, but it may be possible to transform a state diagram into Copilot with very little work so that they could benefit from the verification aspect without compromising their usability needs.

I am considering using Copilot for my next project to interpret user-customizable control-flow models. However, my focus has been on the lower levels so far.

That's great! Let me know how it goes.

I've just looked back over your FSM API proposal and your post made a lot more sense to me this time. I can't think of anything else it could need.

Does it handle nesting? Clock delays? Preemptive interruption?

I don't know. We haven't done anything specially to handle these case, and I haven't tried it. What would examples of those look like specifically for the case of FSMs?

Is it an RTOS? 🦋

RTOS is not one of the OSs we currently support.

The code we produce is hard realtime, but we don't normally test it on an RTOS.

That being said, there's been prior work on running Copilot-generated code in an RTOS. We are asked about this frequently, so I'd be opening to revisiting this. Licensing can be tricky (VxWorks is expensive), but now we even have Ubuntu RTOS.

On a related note, we've also just started looking into running Copilot in the eBPF (in kernel space).

If this is a use case that would be useful for you, we could have a chat to better understand what would need to be done to support RTOS.

[liamdiprose]

I really appreciate your reply. I think my client has a large amount of trust in big companies (with a lot of users) to be supported long term. Visual representations are more familiar to them, so perceive them as safer.

I imagine IQANdesign's format must be different, but it may be possible to transform a state diagram into Copilot with very little work

This was the idea. Since IQANdesign can export projects to a txt file, I was able to write some rules for automatic testing. Copilot was on the radar, which is how this issue originated.

we don't normally test it on an RTOS.

I mean you could write an RTOS in Copilot; each task is a FSM nested inside a main event-loop FSM. I've been using embassy, an RTOS that uses Rust's async/await to construct this pattern. I only wanted to mention it as a "free idea".

I expect to be using Copilot on Linux next (eBPF support would be great). I'll let you know how it goes.

[ivanperez-keera]

I really appreciate your reply. I think my client has a large amount of trust in big companies (with a lot of users) to be supported long term.

I understand.

If this comes up in the future, you can tell them that Copilot has been around since 2010, and we have several projects that use Copilot, so we have no reason to believe that the project will stop any time soon.

This was the idea. Since IQANdesign can export projects to a txt file, I was able to write some rules for automatic testing.

If you have any code that can convert from that format to Copilot (even if WIP/incomplete), it'd be amazing if you could free it. That way, maybe others can use it.

But 100% understandable if that's not an option.

I mean you could write an RTOS in Copilot; each task is a FSM nested inside a main event-loop FSM.

Oh. I hadn't thought about looking at these systems that way. I'll take a look.

I expect to be using Copilot on Linux next (eBPF support would be great). I'll let you know how it goes.

Sounds good.

Whatever comes out of our eBPF work will hopefully also be made public.

[ivanperez-keera]

Even though this was not used for this project, I think it would still be useful to add this functionality to copilot-libraries. The need has come up in the past in work with LaRC.

Tagging @fdedden and @RyanGlScott for opinions. Also see the implementation above; there may be a better API we want to consider.