Tue Aug 13 09:36:24 EDT 2019

State machines

I need a different way to express state machines.  Maybe start looking
into formal?

EDIT: What is the real problem actually?

I like the Erlang transactional model: message comes in and it changes
state.  Message can be anything, state can be anything.

Does this work for syncrhonous state machines as well?  A message in
this case is a clock edge.  Its contents is all the inputs at the
clock edge.  That is not very useful.

So where do these two differ, really?

It seems that the problem with clocked state machines is that the
input is everything and the state is everything.  This is just too
unstructured to say anything meaningful.  so how to abstract it?

It would be great to create logic state machines in the same terms.

EDIT: I wonder if the missing link is just missing knowlege, and not
so much bad integration of knowledge.  Maybe have a look at TLA+


Practical TLA+
Planning Driven Development
Authors: Wayne, Hillel