traceanalysis.h

   1 #ifndef TRACE_ANALYSIS_H
   2 #define TRACE_ANALYSIS_H
   3 #include "model.h"
   4
   5
   6 class TraceAnalysis {
   7 public:
   8         /** setExecution is called once after installation with a reference to
   9          *  the ModelExecution object. */
  10
  11         virtual void setExecution(ModelExecution * execution) = 0;
  12
  13         /** analyze is called once for each feasible trace with the complete
  14          *  action_list object. */
  15
  16         virtual void analyze(action_list_t *) = 0;
  17
  18         /** name returns the analysis name string */
  19
  20         virtual const char * name() = 0;
  21
  22         /** Each analysis option is passed into the option method.  This
  23          *      occurs before installation (i.e., you don't have a
  24          *      ModelExecution object yet).  A TraceAnalysis object should
  25          *      support the option "help"  */
  26
  27         virtual bool option(char *) = 0;
  28
  29         /** The finish method is called once at the end.  This should be
  30          *  used to print out results.  */
  31
  32         virtual void finish() = 0;
  33
  34         /** This method is used to inspect the normal/abnormal model
  35          * action. */
  36         virtual void inspectModelAction(ModelAction *act) {}
  37
  38         /** This method will be called by when a plugin is installed by the
  39          * model checker. */
  40         virtual void actionAtInstallation() {}
  41
  42         /** This method will be called when the model checker finishes the
  43          * executions; With this method, the model checker can alter the
  44          * state of the plugin and then the plugin can choose whether or not
  45          * restart the model checker. */
  46         virtual void actionAtModelCheckingFinish() {}
  47
  48         SNAPSHOTALLOC
  49 };
  50 #endif