diff --git a/harmony_model_checker/charm/graph.h b/harmony_model_checker/charm/graph.h index f72a343f..c446650b 100644 --- a/harmony_model_checker/charm/graph.h +++ b/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 diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c index f028d08d..704eb394 100644 --- a/harmony_model_checker/charm/ops.c +++ b/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; }