Adding a state machine module to copilot-libraries

[ivanperez-keera]

Ogma currently uses an implementation of state machines in Copilot.

I'd like to create a standard module for state machines that is included as part of copilot-libraries.

I've placed an initial example here:

https://github.com/ivanperez-keera/copilot/blob/develop-state-machines/Test.hs

Can I please get your input on 1) bugs in this implementation, 2) other uses cases not included, 3) other properties we could check about state machines (see checkDeterministic, completeMachine, etc.).

Funny enough, What4 and Z3 are capable of proving these properties for the state machine included with that example.

A prior thread discussed state machines as well: #529

[ivanperez-keera]

Tagging @RyanGlScott @fdedden @agoodloe for awareness.

[RyanGlScott]

I haven't tried using this code in-depth yet, but this appears to be a plausible way to encode state machines. I do wonder about the choice to encode states as Word8s however, since I could foresee different use cases wanting different integer types, or perhaps even arbitrary enum types (#699). I wonder if we should instead encode state machines like this:

type StateMachineGF state = (state, state, Stream Bool, [(state, Stream Bool, state)], state)

[ivanperez-keera]

In the same file, there's a type exactly for this:

https://github.com/ivanperez-keera/copilot/blob/a94010b99c02202552e8f88f9fc7a72167f3766a/Test.hs#L91

There's an implementation that works for any Typed that supports equality, and one specifically for Enum.

[RyanGlScott]

Oops, I clearly didn't read carefully enough! Thanks for the pointer.

Out of curiosity, is there a reason to have both StateMachineGF and StateMachineGFA? I notice that all of the properties you check are only defined in terms of the former, for instance, but I think they ought to work for StateMachineGFA as well.

[ivanperez-keera]

I don't think there's a benefit to having both, no. We could just keep the most abstract.

(This module was more of a drawing pad than for demonstration a finalized implementation.)

[ivanperez-keera]

I worked a little bit more on this module.

I moved the core functionality to: https://github.com/ivanperez-keera/copilot/blob/develop-state-machines/copilot-libraries/src/Copilot/Library/StateMachines.hs

I put an example here:

https://github.com/ivanperez-keera/copilot/blob/develop-state-machines/copilot/examples/StateMachines.hs

That example might be best split into two: one that shows how to simulate the machine, and one that shows how to prove properties about it.

@RyanGlScott @chathhorn Let me know if you have any thoughts on this.

[ivanperez-keera]

I welcome all feedback.

A few things I can think of that perhaps you see better than me are:

• More elegant solutions.
• Simpler solutions.
• More versatile solutions.
• Use cases not captured by this implementation.
• More efficient solutions (e.g., once we generate C from this).

Anything else that you think could be useful.

[ivanperez-keera]

Tagging also @fdedden in case he wants to take a look.

[RyanGlScott]

The thing that stands out to me about this implementation is that it must perform a number of ifThenElse checks that is linear in the size of the number of transitions. This isn't wrong, but it is potentially inefficient if you have lots of transitions. I think you could cut down on the number of ifThenElses by first checking the state number, and then dispatching on the particular transitions that match that state. In C pseudocode, this would look something like (adapting the example you posted above):

switch (state) {
  case 0:
    if (input >= 120 && input <= 180) {
      return 0;
    } else if (input > 180) {
      return 1;
    } else if (input < 120) {
      return 2;
    } else {
      return bad;
    }
  case 1:
    if (input <= 180) {
      return 0;
    } else if (input > 180) {
      return 1;
    } else {
      return bad;
    }
  case 2:
    if (input >= 120) {
      return 0;
    } else if (input < 120) {
      return 2;
    } else {
      return bad;
    }
  default:
    return bad;
}

Implementation-wise, I think this could be done by partitioning the transitions by the state they match on and generating two levels of ifThenElses based on the results (one for matching on the state, and another for matching on the transitions corresponding to that state).