X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp-builds.git;a=blobdiff_plain;f=src%2Flibpspp%2Fmodel-checker.h;h=205c3fac9a3713a806e31675083ccc55ee947fb0;hp=1e756119f5b7175860615f6a44938d5e75e6c08b;hb=d724fe4838db898a323102e4f2981af90c9ea132;hpb=72f4ef01cee853fd8e5bca96afad06397326ec76 diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h index 1e756119..205c3fac 100644 --- a/src/libpspp/model-checker.h +++ b/src/libpspp/model-checker.h @@ -150,14 +150,12 @@ mc_name_operation (mc, "do operation %s", ...); clone = clone_foo (state); do_operation (clone); - if (!mc_discard_dup_state (mc, hash_foo (clone))) - { - if (!state_is_consistent (clone)) - mc_error (mc, "inconsistent state"); - mc_add_state (mc, clone); - } - else + if (!state_is_consistent (clone)) + mc_error (mc, "inconsistent state"); + if (mc_discard_dup_state (mc, hash_foo (clone))) destroy_foo (clone); + else + mc_add_state (mc, clone); } } @@ -204,10 +202,10 @@ the metadata. mc_discard_dup_state may be called before or after - checking for consistency, but calling it first avoids - wasting time checking duplicate states for - consistency, which again can be a significant - performance boost. + checking for consistency. Calling it after checking + may make checking a given number of unique states + take longer, but it also ensures that all paths to a + given state produce correct results. - The mc_error function reports errors. It may be called as many times as desired to report each kind