Mon Mar 6 12:07:28 EST 2017

State machine notation

I need a good notation to represent a state machine as a set of
equations in a way that allows some properties to be extracted, or at
least quick-checked.

I spend way to much time "hacking" machines using incomplete

Events "act on" states.  Events are operators, so let's represent them
with capitalized identifiers, leaving lower case identifiers to
represent states.

   s1 A = s2

At this level of abstraction, there are no simultaneous events.

Some possible extensions:

- To represent simultaneous events, compose two or more "proto events"
into one event.

- Not sure how to implement dependency in events, such as timeouts.

Example: a debounced trigger.

A - activating edge
R - releasing edge
T - timeout after a

i  - idle
w1 - active edge seen, waiting for releasing edge or timeout
w2 - timeout expired
t  - releasing edge seen, fully triggered

not modeled: after the occurance of A, a T is scheduled for a moment
in the future.  if multiple A happen, multiple T would be scheduled.
(not a good way to model this).

i  A = w1
w1 T = w2 (passed, waiting for release)
w1 R = i  (filtered)
w2 R = t  (fully passed)

t  _ = t  (once triggered, ignore events)