Fri Nov 29 08:33:59 EST 2019

GOTO and traces

So event driven programs, state machines, are essentially programming
with GOTO.  Should I worry?  I don't think so.  It seems to be the
most natural way to do this.

The problem becomes documentation: add comments that illustrate some
practical protocol traces.

It would be nice to be able to program traces directly.  This is
essentially what "threaded programming" is, but it does not handle
forking traces well.

Why?  I think that making that explicit will shed some insight.

EDIT: Note that threads are not linear.  It is possible that inside a
thread, execution forks at a conditional statement.  But what is
different from raw state machines is that for a thread, there is
usually a join.  I.e. the forking of traces is temporary.

EDIT: So what is understood by "trace semantics"?

Somewhat in the ballpark:

But what I need is something simpler: a relation between a state
machine, and a linear time protocol sequence (test).