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
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
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)