1 #ifndef TRACE_ANALYSIS_H
2 #define TRACE_ANALYSIS_H
8 /** setExecution is called once after installation with a reference to
9 * the ModelExecution object. */
11 virtual void setExecution(ModelExecution * execution) = 0;
13 /** analyze is called once for each feasible trace with the complete
14 * action_list object. */
16 virtual void analyze(action_list_t *) = 0;
18 /** name returns the analysis name string */
20 virtual const char * name() = 0;
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" */
27 virtual bool option(char *) = 0;
29 /** The finish method is called once at the end. This should be
30 * used to print out results. */
32 virtual void finish() = 0;
34 /** This method is used to inspect the normal/abnormal model
36 virtual void inspectModelAction(ModelAction *act) {}
38 /** This method will be called by when a plugin is installed by the
40 virtual void actionAtInstallation() {}
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() {}