Merge branch 'next'

harmony_model_checker/charm/graph.h

@@ -44,6 +44,11 @@ struct access_info {
 // but, for memory efficiency, not the details of the microsteps themselves. If
 // a failure is found, that information is recovered by re-executing the path to
 // the faulty state.
+//
+// TODO. Can replace ctx with ctx_index into src->state, but should also
+// support, say, -1 for inv_context. after could be replaced with
+// an index into dst->state. choice could be the first entry in log
+// Doing all three could save around 20 bytes per edge.
 struct edge {
  struct edge *fwdnext; // forward linked list maintenance
  hvalue_t ctx, choice; // ctx that made the microstep, choice if any

harmony_model_checker/charm/ops.c

@@ -1374,6 +1374,7 @@ void op_Go(
  struct context *copy = (struct context *) buffer;
  ctx_push(copy, result);
  copy->stopped = false;
+ // TODO. Check success of context_add
  context_add(state, value_put_context(&step->engine, copy));
 #ifdef HEAP_ALLOC
  free(buffer);
@@ -2136,7 +2137,7 @@ void op_Spawn(
  }
  else {
  hvalue_t context = value_put_context(&step->engine, ctx);
- if (!context_add(state, context)) {
+ if (context_add(state, context) < 0) {
  value_ctx_failure(step->ctx, &step->engine, "spawn: too many threads");
  return;
  }