X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flibpspp%2Fmodel-checker.h;h=205c3fac9a3713a806e31675083ccc55ee947fb0;hb=d724fe4838db898a323102e4f2981af90c9ea132;hp=dd42e2fd0f3bf771203bc80faf14e7dbd4025a7e;hpb=5060fdedfe17e843301ac0c738e12488af467378;p=pspp-builds.git diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h index dd42e2fd..205c3fac 100644 --- a/src/libpspp/model-checker.h +++ b/src/libpspp/model-checker.h @@ -1,20 +1,18 @@ -/* PSPP - computes sample statistics. - Copyright (C) 2007 Free Software Foundation, Inc. +/* PSPP - a program for statistical analysis. + Copyright (C) 2007, 2009 Free Software Foundation, Inc. - This program is free software; you can redistribute it and/or - modify it under the terms of the GNU General Public License as - published by the Free Software Foundation; either version 2 of the - License, or (at your option) any later version. + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. - This program is distributed in the hope that it will be useful, but - WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - General Public License for more details. + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. You should have received a copy of the GNU General Public License - along with this program; if not, write to the Free Software - Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA - 02110-1301, USA. */ + along with this program. If not, see . */ /* Implementation-level model checker. @@ -117,7 +115,7 @@ Here's an outline for writing the init function: - void + void init_foo (struct mc *mc) { struct foo *foo; @@ -144,7 +142,7 @@ { struct foo *state = state_; - for (...each operation...) + for (...each operation...) if (mc_include_state (mc)) { struct foo *clone; @@ -152,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); } } @@ -206,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 @@ -224,7 +220,7 @@ make it possible to reliably reproduce errors. 3. void destroy (struct mc *mc, void *data); - + This function is called to discard the client-specified DATA associated with a state. @@ -342,7 +338,7 @@ void *mc_get_aux (const struct mc *); /* A path of operations through a model to arrive at some particular state. */ -struct mc_path +struct mc_path { int *ops; /* Sequence of operations. */ size_t length; /* Number of operations. */ @@ -367,7 +363,7 @@ struct mc_options *mc_options_clone (const struct mc_options *); void mc_options_destroy (struct mc_options *); /* Search strategy. */ -enum mc_strategy +enum mc_strategy { MC_BROAD, /* Breadth-first search. */ MC_DEEP, /* Depth-first search. */ @@ -389,7 +385,7 @@ void mc_options_set_follow_path (struct mc_options *, const struct mc_path *); /* Strategy for dropped states from the queue when it overflows. */ -enum mc_queue_limit_strategy +enum mc_queue_limit_strategy { MC_DROP_NEWEST, /* Don't enqueue the new state at all. */ MC_DROP_OLDEST, /* Drop the oldest state in the queue. */ @@ -420,6 +416,10 @@ FILE *mc_options_get_output_file (const struct mc_options *); void mc_options_set_output_file (struct mc_options *, FILE *); typedef bool mc_progress_func (struct mc *); +mc_progress_func mc_progress_dots; +mc_progress_func mc_progress_fancy; +mc_progress_func mc_progress_verbose; + int mc_options_get_progress_usec (const struct mc_options *); void mc_options_set_progress_usec (struct mc_options *, int progress_usec); mc_progress_func *mc_options_get_progress_func (const struct mc_options *); @@ -429,7 +429,7 @@ void *mc_options_get_aux (const struct mc_options *); void mc_options_set_aux (struct mc_options *, void *aux); /* Reason that a model checking run terminated. */ -enum mc_stop_reason +enum mc_stop_reason { MC_CONTINUING, /* Run has not yet terminated. */ MC_SUCCESS, /* Queue emptied (ran out of states). */ @@ -462,4 +462,6 @@ struct timeval mc_results_get_start (const struct mc_results *); struct timeval mc_results_get_end (const struct mc_results *); double mc_results_get_duration (const struct mc_results *); +void mc_results_print (const struct mc_results *, FILE *); + #endif /* libpspp/model-checker.h */