From d75e3af55ca5deadb76dd13cdd8148ad95eaad5f Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 29 Jul 2004 14:47:46 +0000 Subject: [PATCH] - Added the trace prefix cutter. Goody. --- src/main.c | 21 +++++++++--- src/modelchecker.c | 82 +++++++++++++++++++++++++++++++++------------- src/role.c | 42 ++++++++++++------------ src/system.c | 1 + src/system.h | 1 + 5 files changed, 99 insertions(+), 48 deletions(-) diff --git a/src/main.c b/src/main.c index dccf7f6..e84de81 100644 --- a/src/main.c +++ b/src/main.c @@ -85,6 +85,8 @@ main (int argc, char **argv) struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)"); struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)"); + struct arg_int *switch_scenario_size = + arg_int0 ("S", "scenario-size", NULL, "scenario size (fixed trace prefix length)"); struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL, "set traversal method, partial order reduction (default is 12)"); struct arg_int *switch_match_method = @@ -113,7 +115,7 @@ main (int argc, char **argv) struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions"); struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions"); struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions"); - struct arg_lit *switch_summary = arg_lit0 ("S", "summary", "show summary on stdout instead of stderr"); + struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", "show summary on stdout instead of stderr"); struct arg_lit *switch_echo = arg_lit0 ("E", "echo", "echo command line to stdout"); #ifdef DEBUG struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter"); @@ -132,6 +134,7 @@ main (int argc, char **argv) switch_empty, switch_state_space_graph, switch_scenario, + switch_scenario_size, switch_latex_output, switch_summary, switch_echo, @@ -178,6 +181,7 @@ main (int argc, char **argv) switch_por_parameter->ival[0] = 0; #endif switch_scenario->ival[0] = 0; + switch_scenario_size->ival[0] = 0; switch_traversal_method->ival[0] = 12; switch_match_method->ival[0] = 0; switch_prune_trace_length->ival[0] = -1; @@ -337,15 +341,24 @@ main (int argc, char **argv) * The scenario selector has an important side effect; when it is non-null, * any scenario traversing selects chooses first. */ - sys->switchScenario = switch_scenario->ival[0]; /* scenario selector */ + sys->switchScenario = switch_scenario->ival[0]; /* scenario selector */ + sys->switchScenarioSize = switch_scenario_size->ival[0]; /* scenario size */ + if (sys->switchScenario == 0 && sys->switchScenarioSize > 0) + { + /* no scenario, but a size is set. so override */ +#ifdef DEBUG + warning ("Scanning scenarios."); +#endif + sys->switchScenario = -1; + } if (sys->switchScenario < 0) { sys->output = SCENARIOS; } - if (sys->switchScenario != 0) + if (sys->switchScenario != 0 && sys->switchScenarioSize == 0) { #ifdef DEBUG - warning ("Scenario selection implies --choose-first."); + warning ("Scenario selection without trace prefix length implies --choose-first."); #endif sys->switchChooseFirst = 1; } diff --git a/src/modelchecker.c b/src/modelchecker.c index f43b44f..0d17101 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -554,48 +554,84 @@ explorify (const System sys, const int run) */ if (sys->switchScenario != 0) { - /* only after chooses */ - if (myStep == 0 && - rd->type == READ) + /* two variants. If scenario size is 0, we operate on the old method involving chooses */ + if (sys->switchScenarioSize == 0) { - if (run == sys->lastChooseRun) + /* only after chooses */ + if (myStep == 0 && + rd->type == READ) { - /* We are just after the last choose instance */ - /* count this instance */ - if (sys->countScenario < INT_MAX) + if (run == sys->lastChooseRun) { - sys->countScenario++; + /* We are just after the last choose instance */ + /* count this instance */ + if (sys->countScenario < INT_MAX) + { + sys->countScenario++; + } + /* If we are displaying scenarios, print it */ + if (sys->output == SCENARIOS) + { + printf ("%i\t", sys->countScenario); + scenarioPrint (sys); + printf ("\n"); + } + /* If it is not the selected one, abort */ + if (sys->switchScenario != sys->countScenario) + { + /* this branch is not interesting */ + /* unfortunately, it is also not drawn in the state graph because of this */ + if (sys->output == STATESPACE) + { + graphScenario (sys, run, rd); + } + /* act as if executed, but don't really explore it. */ + return 1; + } + } + } + } + else + { + /* scenario size is not zero */ + + //!@todo Optimization: if the good scenario is already traversed, other trace prefixes need not be explored any further. + if (sys->step+1 == sys->switchScenarioSize) + { + /* Now, the prefix has been set. Count it */ + if (sys->countScenario < INT_MAX) + { + sys->countScenario++; } - /* If we are displaying scenarios, print it */ if (sys->output == SCENARIOS) { - printf ("%i\t", sys->countScenario); - scenarioPrint (sys); - printf ("\n"); + /* apparently we want the output */ + int index; + eprintf ("%i\t", sys->countScenario); + index = 0; + while (index < sys->switchScenarioSize) + { + roledefPrint (sys->traceEvent[index]); + eprintf ("#%i; ", sys->traceRun[index]); + index++; + } + eprintf ("\n"); } - /* If it is not the selected one, abort */ + /* Is this the selected one? */ if (sys->switchScenario != sys->countScenario) { - /* this branch is not interesting */ /* unfortunately, it is also not drawn in the state graph because of this */ if (sys->output == STATESPACE) { graphScenario (sys, run, rd); } - return 0; + /* act as if executed, but don't really explore it. */ + return 1; } } } } - /* if there are chooses, and they are to go first, we must always wait for them */ - if (myStep == 1 && sys->switchChooseFirst && sys->lastChooseRun >= 0) - { - /* we only explore this if all chooses have been done, and will be doing stuff */ - if (sys->runs[sys->lastChooseRun].step == 0) - return 0; - } - /** * -------------------------------------------- * Now we assume the event is indeed enabled ! diff --git a/src/role.c b/src/role.c index 107f5b4..6f60604 100644 --- a/src/role.c +++ b/src/role.c @@ -25,56 +25,56 @@ makeRoledef () return (Roledef) memAlloc (sizeof (struct roledef)); } -//! Print a role event list. +//! Print a role event. void roledefPrint (Roledef rd) { if (rd == NULL) { - printf ("[Empty roledef]\n"); + eprintf ("[Empty roledef]"); return; } if (rd->type == READ && rd->internal) { /* special case: internal read == choose ! */ - printf ("CHOOSE("); + eprintf ("CHOOSE("); termPrint (rd->message); - printf (")"); + eprintf (")"); return; } if (rd->type == READ) - printf ("READ"); + eprintf ("READ"); if (rd->type == SEND) - printf ("SEND"); + eprintf ("SEND"); if (rd->type == CLAIM) - printf ("CLAIM"); + eprintf ("CLAIM"); if (rd->label != NULL) { if (globalLatex) { - printf ("$_{"); + eprintf ("$_{"); termPrint (rd->label); - printf ("}$"); + eprintf ("}$"); } else { - printf ("_"); + eprintf ("_"); termPrint (rd->label); } } if (globalLatex) - printf ("$"); - printf ("("); + eprintf ("$"); + eprintf ("("); termPrint (rd->from); - printf (","); + eprintf (","); if (rd->type == CLAIM) - printf (" "); + eprintf (" "); termPrint (rd->to); - printf (", "); + eprintf (", "); termPrint (rd->message); - printf (" )"); + eprintf (" )"); if (globalLatex) - printf ("$"); + eprintf ("$"); } //! Duplicate a single role event node. @@ -204,16 +204,16 @@ rolePrint (Role r) return; indent (); - printf ("[[Role : "); + eprintf ("[[Role : "); termPrint (r->nameterm); - printf ("]]\n"); + eprintf ("]]\n"); locVarPrint (r->locals); rd = r->roledef; while (rd != NULL) { roledefPrint (rd); - printf ("\n"); + eprintf ("\n"); rd = rd->next; } } @@ -224,7 +224,7 @@ rolesPrint (Role r) { if (r == NULL) { - printf ("Empty role."); + eprintf ("Empty role."); } else { diff --git a/src/system.c b/src/system.c index 6fd4578..353b026 100644 --- a/src/system.c +++ b/src/system.c @@ -58,6 +58,7 @@ systemInit () sys->porparam = 0; // multi-purpose parameter sys->latex = 0; // latex output? sys->switchScenario = 0; + sys->switchScenarioSize = 0; sys->switchForceChoose = 1; // force explicit chooses by default sys->switchChooseFirst = 0; // no priority to chooses by default sys->switchReadSymm = 0; // don't force read symmetries by default diff --git a/src/system.h b/src/system.h index 5bf7297..cc9bccc 100644 --- a/src/system.h +++ b/src/system.h @@ -121,6 +121,7 @@ struct system int switchS; //!< Progress display switch. (traversed states) int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. int switchScenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario + int switchScenarioSize; //!< Scenario size, also called fixed trace prefix length int switchForceChoose; //!< Force chooses for each run, even if involved in first read int switchChooseFirst; //!< Priority to chooses, implicit and explicit int switchReadSymm; //!< Enable read symmetry reduction