00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00039 #ifndef __NUSMV_CORE_HRC_DUMPERS_HRC_DUMPER_H__
00040 #define __NUSMV_CORE_HRC_DUMPERS_HRC_DUMPER_H__
00041
00042
00043 #include "nusmv/core/utils/object.h"
00044
00045 #include "nusmv/core/hrc/HrcNode.h"
00046 #include "nusmv/core/compile/symb_table/SymbTable.h"
00047 #include "nusmv/core/node/node.h"
00048 #include "nusmv/core/prop/Prop.h"
00049 #include "nusmv/core/utils/utils.h"
00050
00057 typedef struct HrcDumper_TAG* HrcDumper_ptr;
00058
00065 #define HRC_DUMPER(self) \
00066 ((HrcDumper_ptr) self)
00067
00073 #define HRC_DUMPER_CHECK_INSTANCE(self) \
00074 (nusmv_assert(HRC_DUMPER(self) != HRC_DUMPER(NULL)))
00075
00076
00077
00084 typedef enum HrcDumperSnippet_TAG {
00085
00086 HDS_HRC_TOP,
00087
00088 HDS_LIST_MODS,
00089
00090 HDS_MOD,
00091
00092 HDS_MOD_NAME,
00093
00094 HDS_LIST_MOD_FORMAL_PARAMS,
00095 HDS_MOD_FORMAL_PARAM,
00096
00097 HDS_LIST_MOD_INSTANCES,
00098
00099
00100 HDS_MOD_INSTANCE,
00101
00102 HDS_MOD_INSTANCE_VARNAME,
00103
00104 HDS_MOD_INSTANCE_MODNAME,
00105
00106 HDS_LIST_MOD_INSTANCE_ACTUAL_PARAMS,
00107
00108 HDS_MOD_INSTANCE_ACTUAL_PARAM,
00109
00110 HDS_LIST_SYMBOLS,
00111
00112 HDS_SYMBOL,
00113
00114
00115 HDS_LIST_ASSIGNS,
00116 HDS_ASSIGN_INIT,
00117 HDS_ASSIGN_INVAR,
00118 HDS_ASSIGN_NEXT,
00119
00120 HDS_LIST_CONSTRAINTS,
00121 HDS_CONSTRAINT_INIT,
00122 HDS_CONSTRAINT_INVAR,
00123 HDS_CONSTRAINT_TRANS,
00124
00125 HDS_LIST_FAIRNESS,
00126 HDS_JUSTICE,
00127 HDS_COMPASSION,
00128
00129 HDS_LIST_SPECS,
00130 HDS_SPEC,
00131
00132 HDS_LIST_COMPILER_INFO,
00133 HDS_LIST_SYNTAX_ERRORS,
00134 HDS_ERROR,
00135
00136 } HrcDumperSnippet;
00137
00138
00139
00146 typedef struct HrcDumperInfo_TAG {
00147
00148 enum {
00149 HRC_STAGE_BEGIN = 1,
00150 HRC_STAGE_END = 2,
00151 HRC_STAGE_BEGIN_END = HRC_STAGE_BEGIN | HRC_STAGE_END,
00152 } stage;
00153
00154 union {
00155 node_ptr name;
00156 node_ptr value;
00157 node_ptr expr;
00158 } n1;
00159
00160 union {
00161 node_ptr type;
00162 node_ptr body;
00163 node_ptr expr;
00164 int lineno;
00165 } n2;
00166
00167 struct {
00168 int lineno;
00169 const char* filename;
00170 const char* message;
00171 const char* token;
00172 } error;
00173
00174 SymbCategory symb_cat;
00175 Prop_Type spec_type;
00176
00177
00178 boolean last_in_list;
00179
00180 boolean list_is_empty;
00181
00182 HrcNode_ptr hrcNode;
00183
00184 void* user;
00185 } HrcDumperInfo;
00186
00187
00188
00191
00192
00193
00194
00204 HrcDumper_ptr HrcDumper_create(const NuSMVEnv_ptr env,
00205 FILE* fout);
00206
00216 void HrcDumper_destroy(HrcDumper_ptr self);
00217
00226 VIRTUAL void HrcDumper_dump_snippet(HrcDumper_ptr self,
00227 HrcDumperSnippet snippet,
00228 const HrcDumperInfo* info);
00229
00236 void HrcDumper_enable_indentation(HrcDumper_ptr self,
00237 boolean flag);
00238
00247 void HrcDumper_inc_indent(HrcDumper_ptr self);
00248
00259 void HrcDumper_dec_indent(HrcDumper_ptr self);
00260
00268 void HrcDumper_enable_mod_suffix(HrcDumper_ptr self,
00269 boolean flag);
00270
00271
00276 #endif