Index: vis_dev/dev/Makefile =================================================================== --- vis_dev/dev/Makefile (revision 19) +++ vis_dev/dev/Makefile (revision 20) @@ -3,10 +3,13 @@ INCVISDIR=${LIBVISDIR}/include/ INCGLUDIR=${LIBGLUDIR}/include/ +LIB=-lvis2 -lcu -lglu -lm -lbsd -lreadline -lfl -a.out : main.c utilities.o - gcc main.c -lm -L$(LIBGLUDIR) -lglu -L$(LIBVISDIR) -lvis2 -I$(INCVISDIR) -I$(INCGLUDIR) +a.out : main.o utilities.o + gcc -lm -L$(LIBGLUDIR) -L$(LIBVISDIR) main.o utilities.o $(LIB) +main.o : main.c + gcc -c main.c -I$(INCGLUDIR) -I$(INCVISDIR) utilities.o : utilities.c - gcc -c utilities.c -lm -L$(LIBGLUDIR) -lglu -L$(LIBVISDIR) -lvis2 -I$(INCVISDIR) -I$(INCGLUDIR) + gcc -c utilities.c -I$(INCGLUDIR) -I$(INCVISDIR) clean: rm *.o a.out Index: vis_dev/dev/main.c =================================================================== --- vis_dev/dev/main.c (revision 19) +++ vis_dev/dev/main.c (revision 20) @@ -1,9 +1,17 @@ #include "stdio.h" -#include "hrc.h" -#include "ntk.h" +#include "utilities.h" int main() { -Hrc_Manager_t * hmge; + Hrc_Manager_t * hmgr1; + FILE * file1; + file1 = fopen("example/and2.mv","r"); + hmgr1 = rlmv( file1); + if(hmgr1 !=NULL) + { + Hrc_Node_t * n = Hrc_ManagerReadRootNode(hmgr1); + printf("***** HRC : %s %d\n", Hrc_NodeReadModelName(n)); + } + return 0; } Index: vis_dev/dev/utilities.c =================================================================== --- vis_dev/dev/utilities.c (revision 19) +++ vis_dev/dev/utilities.c (revision 20) @@ -452,3 +452,2 @@ } - Index: vis_dev/dev/utilities.h =================================================================== --- vis_dev/dev/utilities.h (revision 19) +++ vis_dev/dev/utilities.h (revision 20) @@ -16,7 +16,16 @@ #include #include +/********************************************/ +/******* Vis magic formulae *****************/ +FILE *vis_stderr; +FILE *vis_stdout; +FILE *vis_historyFile; +FILE *vis_stdpipe; +array_t *vm_commandHistoryArray; +char *vm_programName; +/********************************************/ -static int +int nodenameCompare( const void * node1, @@ -33,5 +42,4 @@ return (strcmp(name1, name2)); } - // Read blifmv file Hrc_Manager_t * rlmv(FILE * file); Index: vis_dev/glu-2.3/src/cuPort/cuPort.c =================================================================== --- vis_dev/glu-2.3/src/cuPort/cuPort.c (revision 19) +++ vis_dev/glu-2.3/src/cuPort/cuPort.c (revision 20) @@ -706,5 +706,5 @@ ******************************************************************************/ bdd_t * -bdd_and_smooth( +dd_and_smooth( bdd_t *f, bdd_t *g, Index: vis_dev/vis-2.3/src/rob/tags =================================================================== --- vis_dev/vis-2.3/src/rob/tags (revision 19) +++ (revision ) @@ -1,129 +1,0 @@ -!_TAG_FILE_FORMAT 2 /extended format; --format=1 will not append ;" to lines/ -!_TAG_FILE_SORTED 1 /0=unsorted, 1=sorted, 2=foldcase/ -!_TAG_PROGRAM_AUTHOR Darren Hiebert /dhiebert@users.sourceforge.net/ -!_TAG_PROGRAM_NAME Exuberant Ctags // -!_TAG_PROGRAM_URL http://ctags.sourceforge.net /official site/ -!_TAG_PROGRAM_VERSION 5.6 // -CommandBmcRob robCmd.c /^CommandBmcRob( Hrc_Manager_t ** hmgr,$/;" f file: -CommandComposeGolden robCmd.c /^CommandComposeGolden(Hrc_Manager_t ** hmgr,$/;" f file: -CommandConvForbToProp robCmd.c /^CommandConvForbToProp (Hrc_Manager_t ** hmgr,$/;" f file: -CommandConvInitToProp robCmd.c /^CommandConvInitToProp (Hrc_Manager_t ** hmgr,$/;" f file: -CommandConvReachToProp robCmd.c /^CommandConvReachToProp (Hrc_Manager_t ** hmgr,$/;" f file: -CommandConvReqToProp robCmd.c /^CommandConvReqToProp (Hrc_Manager_t ** hmgr,$/;" f file: -CommandConvSafeToProp robCmd.c /^CommandConvSafeToProp (Hrc_Manager_t ** hmgr,$/;" f file: -CommandPrintForbidden robCmd.c /^CommandPrintForbidden( Hrc_Manager_t ** hmgr,$/;" f file: -CommandPrintRequired robCmd.c /^CommandPrintRequired( Hrc_Manager_t ** hmgr,$/;" f file: -CommandPrintSafe robCmd.c /^CommandPrintSafe( Hrc_Manager_t ** hmgr,$/;" f file: -CommandProtectGolden robCmd.c /^CommandProtectGolden(Hrc_Manager_t ** hmgr,$/;" f file: -CommandProtectOutput robCmd.c /^CommandProtectOutput(Hrc_Manager_t ** hmgr,$/;" f file: -CommandProtectRegister robCmd.c /^CommandProtectRegister(Hrc_Manager_t ** hmgr,$/;" f file: -CommandResLtlFile robCmd.c /^CommandResLtlFile (Hrc_Manager_t ** hmgr,$/;" f file: -CommandResetForbidden robCmd.c /^CommandResetForbidden( Hrc_Manager_t ** hmgr,$/;" f file: -CommandResetInitial robCmd.c /^CommandResetInitial( Hrc_Manager_t ** hmgr,$/;" f file: -CommandResetRequired robCmd.c /^CommandResetRequired( Hrc_Manager_t ** hmgr,$/;" f file: -CommandResetSafe robCmd.c /^CommandResetSafe( Hrc_Manager_t ** hmgr,$/;" f file: -CommandRobustness robCmd.c /^CommandRobustness( Hrc_Manager_t ** hmgr,$/;" f file: -CommandSetForbidden robCmd.c /^CommandSetForbidden( Hrc_Manager_t ** hmgr,$/;" f file: -CommandSetInitial robCmd.c /^CommandSetInitial(Hrc_Manager_t ** hmgr,$/;" f file: -CommandSetLtlFormula robCmd.c /^CommandSetLtlFormula (Hrc_Manager_t ** hmgr,$/;" f file: -CommandSetRequired robCmd.c /^CommandSetRequired( Hrc_Manager_t ** hmgr,$/;" f file: -CommandSetSafe robCmd.c /^CommandSetSafe( Hrc_Manager_t ** hmgr,$/;" f file: -CommandTestCount robCmd.c /^CommandTestCount (Hrc_Manager_t ** hmgr,$/;" f file: -CommandprintmddID robCmd.c /^CommandprintmddID (Hrc_Manager_t ** hmgr,$/;" f file: -Common_support SatCountAlgo.c /^Common_support(mdd_manager* mgr,$/;" f -ComposeCubes SatCountAlgo.c /^ComposeCubes(mdd_manager* mgr,$/;" f -D SatCountAlgo.c /^D(Formula_t Form){$/;" f -F SatCountAlgo.h /^ lsList F; $/;" m struct:form -Formula SatCountAlgo.h /^} Formula;$/;" t typeref:struct:form -Formula_t SatCountAlgo.h /^typedef Formula* Formula_t;$/;" t -Get_support SatCountAlgo.c /^Get_support(mdd_manager* mgr,mdd_t* l){$/;" f -K SatCountAlgo.c /^const int K=5;$/;" v -R SatCountAlgo.h /^ mdd_t* R;$/;" m struct:form -ReadCNF_For_Count SatCountAlgo.c /^ReadCNF_For_Count(Ntk_Network_t *network,$/;" f -ReadCNF_For_Count_ SatCountAlgo.c /^ReadCNF_For_Count_( char *filename) {$/;" f -Rob_End robCmd.c /^Rob_End(void)$/;" f -Rob_Init robCmd.c /^Rob_Init(void)$/;" f -V SatCountAlgo.h /^ mdd_t* V;$/;" m struct:form -WriteCNF__rel_sat SatCountAlgo.c /^WriteCNF__rel_sat(char *filename) {$/;" f -WriteIDL__rel_sat SatCountAlgo.c /^WriteIDL__rel_sat(char *filename) {$/;" f -_ROB_H Robust.h 35;" d -_SATCOUNT_H SatCountAlgo.h 35;" d -_d SatCountAlgo.c /^_d(Formula_t Form, mdd_t* x){$/;" f -_k_clause SatCountAlgo.c /^_k_clause(Formula_t Form, int k){$/;" f -_psi SatCountAlgo.c /^_psi(Formula_t For,mdd_t* d){$/;" f -build_golden_faulty_compo Robust.c /^Hrc_Node_t * build_golden_faulty_compo($/;" f -callBmcRob Robust.c /^callBmcRob( Ntk_Network_t *network,$/;" f -clone_formula SatCountAlgo.c /^clone_formula(Formula_t form){$/;" f -compute_error_states Robust.c /^mdd_t* compute_error_states(Fsm_Fsm_t *fsm, mdd_t* reachable, $/;" f -compute_fair Robust.c /^compute_fair(Fsm_Fsm_t *fsm,int verbosityLevel){$/;" f -conv_error_msg Robust.c /^conv_error_msg(FILE* f, char* cmd, type_err e){$/;" f -convert_dnf_cnf SatCountAlgo.c /^mdd_t* convert_dnf_cnf(Formula_t Form,$/;" f -couvert_dnf_to_cnf3 SatCountAlgo.c /^couvert_dnf_to_cnf3(Formula_t Form,$/;" f -createFormula SatCountAlgo.c /^createFormula(mdd_manager * mgr){$/;" f -determine_non_protected_registers Robust.c /^determine_non_protected_registers(Fsm_Fsm_t *fsm, FILE *f) {$/;" f -disjoint_formula SatCountAlgo.c /^disjoint_formula(Formula_t Form,$/;" f -earg Robust.h /^ earg,$/;" e enum:__anon1 -ecmd Robust.h /^ ecmd,$/;" e enum:__anon1 -eicmd Robust.h /^ eicmd,$/;" e enum:__anon1 -eiofile Robust.h /^ eiofile,$/;" e enum:__anon1 -enfile Robust.h /^ enfile,$/;" e enum:__anon1 -eofile Robust.h /^ eofile,$/;" e enum:__anon1 -ercmd Robust.h /^ ercmd$/;" e enum:__anon1 -error_msg Robust.c /^error_msg(FILE* f, char* cmd, type_err e){$/;" f -error_states Robust.c /^mdd_t* error_states(Fsm_Fsm_t *fsm, $/;" f -error_states_ms_mt Robust.c /^mdd_t* error_states_ms_mt(Fsm_Fsm_t *fsm, $/;" f -error_states_ms_ut Robust.c /^mdd_t* error_states_ms_ut(Fsm_Fsm_t *fsm, $/;" f -error_states_us_mt Robust.c /^mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, $/;" f -error_states_us_ut Robust.c /^mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, $/;" f -evaluate Robust.c /^mdd_t* evaluate(Fsm_Fsm_t *fsm,FILE* ctlfile,mdd_t* fairS,$/;" f -evaluate_AU Robust.c /^mdd_t* evaluate_AU(Fsm_Fsm_t *fsm, mdd_t* inv, $/;" f -evaluate_EF Robust.c /^mdd_t* evaluate_EF(Fsm_Fsm_t *fsm, mdd_t *target,$/;" f -evaluate_EG Robust.c /^mdd_t* evaluate_EG(Fsm_Fsm_t *fsm, mdd_t *invariant,$/;" f -evaluate_EU Robust.c /^mdd_t* evaluate_EU(Fsm_Fsm_t *fsm, mdd_t* inv, $/;" f -evaluate_Formula_AF_AF Robust.c /^evaluate_Formula_AF_AF (Fsm_Fsm_t *fsm,$/;" f -evaluate_Formula_AF_EF Robust.c /^evaluate_Formula_AF_EF (Fsm_Fsm_t *fsm,$/;" f -evaluate_Formula_EF_AF Robust.c /^evaluate_Formula_EF_AF (Fsm_Fsm_t *fsm,$/;" f -evaluate_Formula_EF_EF Robust.c /^evaluate_Formula_EF_EF (Fsm_Fsm_t *fsm,$/;" f -exit_ SatCountAlgo.c /^int exit_(Formula_t Form, mdd_t* n){$/;" f -form SatCountAlgo.h /^typedef struct form{ $/;" s -free_formula SatCountAlgo.c /^void free_formula(Formula_t F){$/;" f -generateProtectFile Robust.c /^int generateProtectFile($/;" f -getForbidden Robust.c /^getForbidden(Fsm_Fsm_t *fsm){$/;" f -getInitial Robust.c /^getInitial(Fsm_Fsm_t *fsm) {$/;" f -getReach Robust.c /^getReach(Fsm_Fsm_t *fsm) {$/;" f -getReachOrg Robust.c /^getReachOrg( Fsm_Fsm_t *fsm ){$/;" f -getRequired Robust.c /^getRequired(Fsm_Fsm_t *fsm){$/;" f -getSafe Robust.c /^getSafe( Fsm_Fsm_t *fsm ){$/;" f -get_max_degree_ SatCountAlgo.c /^get_max_degree_(Formula_t Form, mdd_t* clause){$/;" f -get_max_nhb_degre SatCountAlgo.c /^get_max_nhb_degre(Formula_t Form, $/;" f -get_neighbour SatCountAlgo.c /^get_neighbour(Formula_t Form, mdd_t* x,int * deg){$/;" f -get_number_of_states Robust.c /^void get_number_of_states(Fsm_Fsm_t *fsm, mdd_t* b, EpDouble* ep) {$/;" f -get_var_sup SatCountAlgo.c /^get_var_sup (Formula_t Form){$/;" f -get_w SatCountAlgo.c /^get_w(Formula_t Form,$/;" f -getbddvars Robust.c /^getbddvars( mdd_manager *mgr,$/;" f file: -greater_d SatCountAlgo.c /^greater_d(Formula_t Form,int k){$/;" f -inj_ms Robust.c /^mdd_t* inj_ms(mdd_manager *mddManager, $/;" f -inj_register Robust.c /^static mdd_t* inj_register(mdd_manager *mddManager, mdd_t* S, mdd_t* r) {$/;" f file: -inj_us Robust.c /^mdd_t* inj_us(mdd_manager *mddManager, array_t* bdd_not_protected, mdd_t* S) {$/;" f -is_empty_formula SatCountAlgo.c /^is_empty_formula(Formula_t Form){$/;" f -main_Count_test SatCountAlgo.c /^main_Count_test(Ntk_Network_t *network,$/;" f -main_Count_test_ SatCountAlgo.c /^main_Count_test_(Ntk_Network_t *network,$/;" f -main_Count_test_sharp SatCountAlgo.c /^main_Count_test_sharp(char *filename, int cnt){$/;" f -main_SatCount SatCountAlgo.c /^main_SatCount(char *filename){$/;" f -mdd_FunctionPrint Robust.c /^mdd_FunctionPrint(mdd_manager *mgr ,$/;" f -mdd_FunctionPrintMain Robust.c /^mdd_FunctionPrintMain(mdd_manager *mgr ,$/;" f -mdd_restrict Robust.c /^mdd_restrict(mdd_manager* mgr,$/;" f file: -mdd_restrict SatCountAlgo.c /^mdd_restrict(mdd_manager* mgr,$/;" f file: -mgr SatCountAlgo.h /^ mdd_manager * mgr;$/;" m struct:form -mymddGetVarById Robust.c 34;" d file: -nCl SatCountAlgo.c /^int nVar=0, nCl=0;$/;" v -nVar SatCountAlgo.c /^int nVar=0, nCl=0;$/;" v -pick_2_clause_w SatCountAlgo.c /^pick_2_clause_w(Formula_t Form, mdd_t* clause){$/;" f -pick_clause_w SatCountAlgo.c /^pick_clause_w(Formula_t Form){$/;" f -print_formula SatCountAlgo.c /^void print_formula(Formula_t F){$/;" f -print_number_of_states Robust.c /^void print_number_of_states(char* msg, Fsm_Fsm_t *fsm, mdd_t* b) {$/;" f -print_variables_info Robust.c /^void print_variables_info(Fsm_Fsm_t *fsm) {$/;" f -sat_Add_Blocking_Clauses Robust.c /^sat_Add_Blocking_Clauses( Ntk_Network_t *network,$/;" f -sat_Add_Blocking_Clauses_2 Robust.c /^sat_Add_Blocking_Clauses_2(Ntk_Network_t *network,$/;" f -timeOutEnv robCmd.c /^static jmp_buf timeOutEnv;$/;" v file: -type_err Robust.h /^} type_err;$/;" t typeref:enum:__anon1