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.