Index: /cegar_dev/cegar/Makefile =================================================================== --- /cegar_dev/cegar/Makefile (revision 3) +++ /cegar_dev/cegar/Makefile (revision 3) @@ -0,0 +1,74 @@ + VIS_PATH=/dsk/l1/misc/Soft + LIB_VIS=$(VIS_PATH)/lib + LIB_OPT= -lMonvis -lcu -lglu -lm -lbsd -lreadline -ltermcap -lfl + GCC_OPT = -g -O6 -mcpu=pentiumpro -malign-double + D_OPT = -DBDDcu + INCLUDE= -I$(VIS_PATH)/include + LIB_GLU = $(VIS_PATH)/lib + VIS_OBJ_PATH=$(VIS_PATH)/vis-2.3/obj + + VIS_OBJ= $(VIS_OBJ_PATH)/ctlpRead.o $(VIS_OBJ_PATH)/ctlspRead.o\ + $(VIS_OBJ_PATH)/ioYacc.o $(VIS_OBJ_PATH)/absCatalog.o $(VIS_OBJ_PATH)/absCmd.o\ + $(VIS_OBJ_PATH)/absEvaluate.o $(VIS_OBJ_PATH)/absInternal.o $(VIS_OBJ_PATH)/absRefine.o \ + $(VIS_OBJ_PATH)/absTranslate.o $(VIS_OBJ_PATH)/absUtil.o $(VIS_OBJ_PATH)/amcBlock.o \ + $(VIS_OBJ_PATH)/amcCmd.o $(VIS_OBJ_PATH)/amcAmc.o $(VIS_OBJ_PATH)/baigCmd.o\ + $(VIS_OBJ_PATH)/baigNode.o $(VIS_OBJ_PATH)/baigBddSweep.o\ + $(VIS_OBJ_PATH)/baigTimeframe.o $(VIS_OBJ_PATH)/baigAllSat.o $(VIS_OBJ_PATH)/bmcUtil.o\ + $(VIS_OBJ_PATH)/bmcCmd.o $(VIS_OBJ_PATH)/bmcBmc.o\ + $(VIS_OBJ_PATH)/bmcCirCUsUtil.o $(VIS_OBJ_PATH)/bmcCirCUs.o $(VIS_OBJ_PATH)/bmcAutSat.o $(VIS_OBJ_PATH)/bmcAutUtil.o\ + $(VIS_OBJ_PATH)/cmdCmd.o $(VIS_OBJ_PATH)/cmdFile.o $(VIS_OBJ_PATH)/cmdMisc.o\ + $(VIS_OBJ_PATH)/ctlpCmd.o $(VIS_OBJ_PATH)/ctlpUtil.o\ + $(VIS_OBJ_PATH)/ctlspCmd.o $(VIS_OBJ_PATH)/ctlspUtil.o \ + $(VIS_OBJ_PATH)/eqvCmd.o $(VIS_OBJ_PATH)/eqvMisc.o\ + $(VIS_OBJ_PATH)/eqvVerify.o\ + $(VIS_OBJ_PATH)/fsmCmd.o $(VIS_OBJ_PATH)/fsmFair.o \ + $(VIS_OBJ_PATH)/fsmFsm.o $(VIS_OBJ_PATH)/fsmReach.o $(VIS_OBJ_PATH)/fsmHD.o\ + $(VIS_OBJ_PATH)/fsmArdc.o $(VIS_OBJ_PATH)/grabUtil.o\ + $(VIS_OBJ_PATH)/grabBMC.o $(VIS_OBJ_PATH)/grabGrab.o $(VIS_OBJ_PATH)/grab.o\ + $(VIS_OBJ_PATH)/hrcCmd.o $(VIS_OBJ_PATH)/hrcHierarchy.o\ + $(VIS_OBJ_PATH)/hrcInOut.o $(VIS_OBJ_PATH)/hrcMemUtil.o\ + $(VIS_OBJ_PATH)/hrcMisc.o\ + $(VIS_OBJ_PATH)/hrcModify.o $(VIS_OBJ_PATH)/imcCmd.o $(VIS_OBJ_PATH)/imcImc.o\ + $(VIS_OBJ_PATH)/imgLinear.o $(VIS_OBJ_PATH)/imgHybrid.o \ + $(VIS_OBJ_PATH)/imgIwls95.o $(VIS_OBJ_PATH)/imgMlp.o\ + $(VIS_OBJ_PATH)/imgMonolithic.o $(VIS_OBJ_PATH)/imgTfm.o \ + $(VIS_OBJ_PATH)/imgTfmBwd.o $(VIS_OBJ_PATH)/imgTfmCache.o\ + $(VIS_OBJ_PATH)/imgTfmFwd.o $(VIS_OBJ_PATH)/imgTfmUtil.o \ + $(VIS_OBJ_PATH)/imgUtil.o $(VIS_OBJ_PATH)/ioCheck.o $(VIS_OBJ_PATH)/ioCmd.o\ + $(VIS_OBJ_PATH)/ioParse.o $(VIS_OBJ_PATH)/ioReadBlifMv.o $(VIS_OBJ_PATH)/ioTable.o\ + $(VIS_OBJ_PATH)/ioWriteBlif.o $(VIS_OBJ_PATH)/ioWriteBlifUtil.o\ + $(VIS_OBJ_PATH)/ioWriteBlifIo.o $(VIS_OBJ_PATH)/ioWriteBlifMv.o \ + $(VIS_OBJ_PATH)/ioWriteSmv.o $(VIS_OBJ_PATH)/ltl.o $(VIS_OBJ_PATH)/ltlSet.o\ + $(VIS_OBJ_PATH)/ltlTableau.o $(VIS_OBJ_PATH)/ltlAutomaton.o\ + $(VIS_OBJ_PATH)/ltlMinimize.o $(VIS_OBJ_PATH)/ltlCompose.o \ + $(VIS_OBJ_PATH)/ltlUtil.o $(VIS_OBJ_PATH)/maigUtil.o\ + $(VIS_OBJ_PATH)/mark.o $(VIS_OBJ_PATH)/markFPSolve.o\ + $(VIS_OBJ_PATH)/markGetScc.o $(VIS_OBJ_PATH)/markInProb.o\ + $(VIS_OBJ_PATH)/mcCmd.o $(VIS_OBJ_PATH)/mcCover.o $(VIS_OBJ_PATH)/mcDbg.o \ + $(VIS_OBJ_PATH)/mcDnC.o $(VIS_OBJ_PATH)/mcGFP.o $(VIS_OBJ_PATH)/mcMc.o\ + $(VIS_OBJ_PATH)/mcSCC.o $(VIS_OBJ_PATH)/mcUtil.o $(VIS_OBJ_PATH)/mcVacuum.o\ + $(VIS_OBJ_PATH)/mvfMvf.o $(VIS_OBJ_PATH)/mvfaigUtil.o $(VIS_OBJ_PATH)/ntkCmd.o\ + $(VIS_OBJ_PATH)/ntkFlt.o $(VIS_OBJ_PATH)/ntkGraph.o $(VIS_OBJ_PATH)/ntkNode.o\ + $(VIS_OBJ_PATH)/ntkNtk.o $(VIS_OBJ_PATH)/ntkSweep.o $(VIS_OBJ_PATH)/ntm.o\ + $(VIS_OBJ_PATH)/ntmaig.o $(VIS_OBJ_PATH)/ntmaigCmd.o $(VIS_OBJ_PATH)/ordCmd.o\ +$(VIS_OBJ_PATH)/ordIo.o $(VIS_OBJ_PATH)/ordMain.o $(VIS_OBJ_PATH)/ordNodes.o\ + $(VIS_OBJ_PATH)/ordPerm.o $(VIS_OBJ_PATH)/ordRoots.o $(VIS_OBJ_PATH)/partCmd.o\ + $(VIS_OBJ_PATH)/partCollapse.o $(VIS_OBJ_PATH)/partInOut.o $(VIS_OBJ_PATH)/partPart.o\ + $(VIS_OBJ_PATH)/partPartial.o $(VIS_OBJ_PATH)/partTotal.o $(VIS_OBJ_PATH)/partFrontier.o $(VIS_OBJ_PATH)/partBoundary.o $(VIS_OBJ_PATH)/partGroup.o $(VIS_OBJ_PATH)/partFine.o $(VIS_OBJ_PATH)/puresatUtil.o $(VIS_OBJ_PATH)/puresatBMC.o $(VIS_OBJ_PATH)/puresatRefine.o $(VIS_OBJ_PATH)/puresat.o $(VIS_OBJ_PATH)/puresatMain.o $(VIS_OBJ_PATH)/puresatIPAbRf.o $(VIS_OBJ_PATH)/puresatAig.o $(VIS_OBJ_PATH)/puresatArosat.o $(VIS_OBJ_PATH)/puresatIPUtil.o $(VIS_OBJ_PATH)/puresatIPRefine.o $(VIS_OBJ_PATH)/puresatTFrame.o $(VIS_OBJ_PATH)/puresatFlatIP.o $(VIS_OBJ_PATH)/rst.o $(VIS_OBJ_PATH)/rstGroup.o $(VIS_OBJ_PATH)/resLayer.o $(VIS_OBJ_PATH)/resCompose.o $(VIS_OBJ_PATH)/resSmartVarUse.o $(VIS_OBJ_PATH)/res.o $(VIS_OBJ_PATH)/resCmd.o $(VIS_OBJ_PATH)/resRes.o $(VIS_OBJ_PATH)/restrCProj.o $(VIS_OBJ_PATH)/restrCmd.o $(VIS_OBJ_PATH)/restrDebug.o $(VIS_OBJ_PATH)/restrFaninout.o $(VIS_OBJ_PATH)/restrHammingD.o $(VIS_OBJ_PATH)/restrRestructure.o $(VIS_OBJ_PATH)/restrUtil.o $(VIS_OBJ_PATH)/rtMain.o $(VIS_OBJ_PATH)/satConflict.o $(VIS_OBJ_PATH)/satImplication.o $(VIS_OBJ_PATH)/satMain.o $(VIS_OBJ_PATH)/satUtil.o $(VIS_OBJ_PATH)/satDecision.o $(VIS_OBJ_PATH)/satInc.o $(VIS_OBJ_PATH)/satDebug.o $(VIS_OBJ_PATH)/satInterface.o $(VIS_OBJ_PATH)/satBDD.o $(VIS_OBJ_PATH)/satCore.o $(VIS_OBJ_PATH)/simIo.o $(VIS_OBJ_PATH)/simMain.o $(VIS_OBJ_PATH)/simSim.o $(VIS_OBJ_PATH)/simUtil.o $(VIS_OBJ_PATH)/spfdAPI.o $(VIS_OBJ_PATH)/spfdClean.o $(VIS_OBJ_PATH)/spfdCmd.o $(VIS_OBJ_PATH)/spfdCommon.o $(VIS_OBJ_PATH)/spfdOpt.o $(VIS_OBJ_PATH)/spfdProg.o $(VIS_OBJ_PATH)/spfdReg.o $(VIS_OBJ_PATH)/spfdSpfd.o $(VIS_OBJ_PATH)/spfdUtil.o $(VIS_OBJ_PATH)/synth.o $(VIS_OBJ_PATH)/synthCount.o $(VIS_OBJ_PATH)/synthDiv.o $(VIS_OBJ_PATH)/synthFactor.o $(VIS_OBJ_PATH)/synthGen.o $(VIS_OBJ_PATH)/synthOpt.o $(VIS_OBJ_PATH)/synthSimple.o $(VIS_OBJ_PATH)/synthSynth.o $(VIS_OBJ_PATH)/synthUtil.o $(VIS_OBJ_PATH)/synthWrite.o $(VIS_OBJ_PATH)/tblEntryUtil.o $(VIS_OBJ_PATH)/tblTest.o $(VIS_OBJ_PATH)/tblUtil.o $(VIS_OBJ_PATH)/tblSweep.o $(VIS_OBJ_PATH)/tblAigUtil.o $(VIS_OBJ_PATH)/tblAigEntryUtil.o $(VIS_OBJ_PATH)/tblIdentity.o $(VIS_OBJ_PATH)/truesimCmd.o $(VIS_OBJ_PATH)/truesimMain.o $(VIS_OBJ_PATH)/truesimSim.o $(VIS_OBJ_PATH)/truesimUtil.o $(VIS_OBJ_PATH)/truesimZero.o $(VIS_OBJ_PATH)/tst.o $(VIS_OBJ_PATH)/varVariable.o $(VIS_OBJ_PATH)/vmInit.o $(VIS_OBJ_PATH)/vmVers.o + + + all: exec + + # Create libMonVis + libMonvis.a: + rm -f $(LIB_VIS)/$@ + umask 2; ar cq $(LIB_VIS)/$@ $(VIS_OBJ) + ranlib $(LIB_VIS)/$@ + + + # exec + + exec: main.c + gcc $(GCC_OPT) $(D_OPT) $(INCLUDE) -L$(LIB_GLU) -L$(LIB_VIS) main.c $(LIB_OPT) + + Index: /cegar_dev/cegar/main.c =================================================================== --- /cegar_dev/cegar/main.c (revision 3) +++ /cegar_dev/cegar/main.c (revision 3) @@ -0,0 +1,7092 @@ + +#include "io.h" +#include "ioInt.h" +#include "ntk.h" +#include "ord.h" +#include "part.h" +#include "maig.h" +#include "ntmaig.h" +#include "fsm.h" +#include "ctlp.h" +#include "ctlsp.h" +#include "mc.h" +#include "mcInt.h" +#include "grabInt.h" +#include "bmc.h" +#include "bmcInt.h" +#include +#include + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ +/* + * States of the state machine used to parse the input variable name list file. + */ +#define STATE_TEST 0 /* next char is in first column */ +#define STATE_WAIT 1 /* wait until end of line '\n' is reached */ +#define STATE_IN 2 /* parsing a variable name */ + +/* + * Maximum permissible length of a variable name in the input variable name list file. + */ +#define MAX_NAME_LENGTH 200 +#define LENGTH_1 255 +#define SIZE_1 100 + +/* + * INPUT FILES + */ +/*********************************************************/ + +#define BLIF_MV_FILE_C1 "EX_C1/Concret_Main.mv" +#define FAIRNESS_FILE_C1 "EX_C1/machine_concret.fair" +#define CTL_FILE_C1 "EX_C1/machine_concret.ctl" +#define CNF_FILE_C1 "EX_C1/SATcnf_c1.cnf" +#define CNF_FILE_C1_BIS "EX_C1/SATcnf_c1_bis.cnf" +#define DEBUG_FILE_C1 "EX_C1/TEST_debug_trace" + + +#define BLIF_MV_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/main_abstract.mv" +#define FAIRNESS_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/main_abstract.fair" +#define CTL_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/machine_concret.ctl" +#define CNF_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/SATcnf_a1.cnf" +#define DEBUG_FILE_A1 "TEST_debug_trace" + +/*****************************************************/ +/* +#define BLIF_MV_FILE_C1 "PBS_VCI_PI/new_main.mv" +#define FAIRNESS_FILE_C1 "PBS_VCI_PI/main_mod.fair" +#define CTL_FILE_C1 "PBS_VCI_PI/propri_mod.ctl" +#define CNF_FILE_C1 "PBS_VCI_PI/SATcnf_c1.cnf" +#define CNF_FILE_C1_BIS "PBS_VCI_PI/SATcnf_c1_bis.cnf" +#define DEBUG_FILE_C1 "PBS_VCI_PI/debug_trace" + + +#define BLIF_MV_FILE_A1 "PBS_VCI_PI/new_main.mv" +#define FAIRNESS_FILE_A1 "PBS_VCI_PI/main_mod.fair" +#define CTL_FILE_A1 "PBS_VCI_PI/propri_mod.ctl" +#define CNF_FILE_A1 "PBS_VCI_PI/SATcnf_a1.cnf" +#define DEBUG_FILE_A1 "PBS_VCI_PI/debug_trace" +*/ + +//#define BLIF_MV_FILE_C1 "VCI_PI/Concrete/main_concret.mv" +//#define FAIRNESS_FILE_C1 "VCI_PI/Concrete/main_concret.fair" +//#define CTL_FILE_C1 "VCI_PI/Concrete/main_concret.ctl" +//#define CNF_FILE_C1 "VCI_PI/Concrete/SATcnf_c1.cnf" +//#define DEBUG_FILE_C1 "VCI_PI/Concrete/debug_trace" + +//#define BLIF_MV_FILE_A1 "VCI_PI/Concrete/main_concret.mv" +//#define FAIRNESS_FILE_A1 "VCI_PI/Concrete/main_concret.fair" +//#define CTL_FILE_A1 "VCI_PI/Concrete/main_concret.ctl" +//#define CNF_FILE_A1 "VCI_PI/Concrete/SATcnf_a1.cnf" +//#define DEBUG_FILE_A1 "VCI_PI/Concrete/debug_trace" + +//#define BLIF_MV_FILE_A1 "VCI_PI/main_abstract.mv" +//#define FAIRNESS_FILE_A1 "VCI_PI/main_abstract.fair" +//#define CTL_FILE_A1 "VCI_PI/main_concret.ctl" +//#define CNF_FILE_A1 "VCI_PI/SATcnf_a1.cnf" +//#define DEBUG_FILE_A1 "VCI_PI/debug_trace" + +// #define BLIF_MV_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2/main_abstract.mv" +// #define FAIRNESS_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2/main_abstract.fair" +// #define CTL_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2/machine_concret.ctl" +// #define CNF_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2/SATcnf_a1.cnf" +// #define DEBUG_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2/debug_trace" + +// #define BLIF_MV_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED2/main_abstract.mv" +// #define FAIRNESS_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED2/main_abstract.fair" +// #define CTL_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED2/machine_concret.ctl" +// #define CNF_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED2/SATcnf_a1.cnf" +// #define DEBUG_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED2/debug_trace" + +// #define BLIF_MV_FILE_C1 "METRONOME/metronome.mv" +// #define FAIRNESS_FILE_C1 "METRONOME/metronome.fair" +// #define CTL_FILE_C1 "METRONOME/metronome.ctl" +// #define CNF_FILE_C1 "METRONOME/SATcnf_c2.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/NOT/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/NOT/not.fair" +// #define CTL_FILE_C1 "GATES/NOT/not.ctl" +// #define CNF_FILE_C1 "GATES/NOT/SATcnf_not.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/NOT2/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/NOT2/not2.fair" +// #define CTL_FILE_C1 "GATES/NOT2/not2.ctl" +// #define CNF_FILE_C1 "GATES/NOT2/SATcnf_not2.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/NOT4/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/NOT4/not4.fair" +// #define CTL_FILE_C1 "GATES/NOT4/not4.ctl" +// #define CNF_FILE_C1 "GATES/NOT4/SATcnf_not4.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/AND/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/AND/and.fair" +// #define CTL_FILE_C1 "GATES/AND/and.ctl" +// #define CNF_FILE_C1 "GATES/AND/SATcnf_and.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/AND2/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/AND2/and2.fair" +// #define CTL_FILE_C1 "GATES/AND2/and2.ctl" +// #define CNF_FILE_C1 "GATES/AND2/SATcnf_and2.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/OR/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/OR/or.fair" +// #define CTL_FILE_C1 "GATES/OR/or.ctl" +// #define CNF_FILE_C1 "GATES/OR/SATcnf_or.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/OR2/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/OR2/or2.fair" +// #define CTL_FILE_C1 "GATES/OR2/or2.ctl" +// #define CNF_FILE_C1 "GATES/OR2/SATcnf_or2.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/SFM2006_Circuit/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/SFM2006_Circuit/sfm.fair" +// #define CTL_FILE_C1 "GATES/SFM2006_Circuit/sfm.ctl" +// #define CNF_FILE_C1 "GATES/SFM2006_Circuit/SATcnf_sfm.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/SFM2006_Circuit2/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/SFM2006_Circuit2/sfm2.fair" +// #define CTL_FILE_C1 "GATES/SFM2006_Circuit2/sfm2.ctl" +// #define CNF_FILE_C1 "GATES/SFM2006_Circuit2/SATcnf_sfm2.cnf" + +// #define BLIF_MV_FILE_C1 "GATES/SFM2006_Circuit3/Concret_Main.mv" +// #define FAIRNESS_FILE_C1 "GATES/SFM2006_Circuit3/sfm3.fair" +// #define CTL_FILE_C1 "GATES/SFM2006_Circuit3/sfm3.ctl" +// #define CNF_FILE_C1 "GATES/SFM2006_Circuit3/SATcnf_sfm3.cnf" + +//#define BLIF_MV_FILE_A2 "MEE/metronome.mv" +//#define FAIRNESS_FILE_A2 "EC1/machine_concret.fair" +//#define CTL_FILE_A1 "EX1/machine_concret.ctl" +//#define CNF_FILE_A2 "EX1/SATcnf_a2.cnf" + +/*---------------------------------------------------------------------------*/ +/* Structure declarations */ +/*---------------------------------------------------------------------------*/ +/**Struct********************************************************************** + Synopsis [A struct to store a string of characters] +******************************************************************************/ +typedef char string1 [255]; + + +/**Struct********************************************************************** + Synopsis [A struct to store of variables in the counter-example.] +******************************************************************************/ +typedef struct { + int varIndex; // not really necessary + int varId; + int varValue; +// char *varName +// char *symbolicValue + string1 varName; // change to dynamic allocation later + string1 symbolicValue; // change to dynamic allocation later +} CEXVarStruct; + + +/**Struct********************************************************************** + Synopsis [A struct to store counter-example data.] +******************************************************************************/ +typedef struct { + int pathIndex; + int n_outputVar; + int n_inputVar; + CEXVarStruct *outputVar; + CEXVarStruct *inputVar; +}CEXStruct; + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ +Hrc_Manager_t *hmgrGlobalC; + +FILE *vis_stderr; +FILE *vis_stdout; +FILE *vis_historyFile; +FILE *vis_stdpipe; +array_t *vm_commandHistoryArray; +char *vm_programName; +static int mcTimeOut; //Time-out value for model-checking +static jmp_buf timeOutEnv; +static long alarmLapTime; /* starting CPU time for timeout */ +static jmp_buf env; + +extern FILE *IoYyin; +extern int globalCurrentStackDepth; +#ifdef IODEBUG +extern int IoYydebug; +#endif /*IODEBUG */ + +char currentPath [LENGTH_1]; +static CEXVarStruct *testCEXVar; +static CEXStruct *testCEX; + + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static Hrc_Manager_t *read_blif_mvMine (FILE *fp, Hrc_Manager_t *hmgr, boolean isCanonical, boolean isIncremental, boolean isVerbose); +static int read_fairnessMine (Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int init_verifyMine (Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int flatten_hierarchyMine (Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int static_orderMine (Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int build_partition_mddsMine (Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int build_partition_maigsMine(Hrc_Manager_t ** hmgr, int argc, char ** argv); +static int print_ioMine (Hrc_Manager_t **hmgr, int argc, char **argv); +static int model_checkMine (Hrc_Manager_t **hmgr, int argc, char **argv); +static int print_modelsMine(Hrc_Manager_t **hmgr, int argc, char **argv); +static int print_fairnessMine(Hrc_Manager_t ** hmgr, int argc, char ** argv); +static Hrc_Node_t *cdMine(Hrc_Manager_t **hmgr, int argc, char **argv); //returns child or parent node +static Hrc_Node_t *lsMine(Hrc_Manager_t **hmgr, int argc, char **argv); //returns current node +static char *pwdMine(Hrc_Manager_t **hmgr, int argc, char **argv); //returns the path of the current node +static int print_latchesMine(Hrc_Manager_t **hmgr, int argc, char **argv); + +static boolean McPrintPassFailMine (mdd_manager *mddMgr, Fsm_Fsm_t *modelFsm, Mc_FwdBwdAnalysis traversalDirection, Ctlp_Formula_t *ctlFormula, mdd_t *ctlFormulaStates, mdd_t *modelInitialStates, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity); +static int McFsmDebugFormulaMine (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray); +static array_t * McFsmStateDebugFormulaMine( McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, array_t *prevCExArray); +static array_t * FsmStateDebugConvertedFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray, array_t **preCExArray); + +static void DebugIDMine(McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm); +static void DebugTrueFalseMine(Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm); +static array_t * DebugBooleanMine(McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, array_t **preCExArray); +static McPath_t * DebugEXMine (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray); +static McPath_t * DebugEUMine (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray); +static McPath_t * DebugEGMine (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, McOptions_t *options); + +static array_t * FsmPathDebugEXFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugEUFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugEGFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugEFFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray, array_t **preCExArray); + +static array_t * FsmPathDebugAXFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugAFFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugAGFormulaMine(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray, array_t **preCExArray); +static array_t * FsmPathDebugAUFormulaMine(McOptions_t *options, mdd_t *aState, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray, array_t **preCExArray); + +static int Mc_PrintPathMine (array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput); +static void McPrintTransitionMine (mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, CEXStruct *CEXPath, int seqNumber, BmcCnfClauses_t *cnfClauses); +static void Mc_MintermPrintMine (mdd_t *aMinterm, array_t *support, Ntk_Network_t *aNetwork); +static char *Mc_MintermToStringMine( mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork, CEXStruct *CEXPath, int seqNumber, boolean inOutIndicator, BmcCnfClauses_t *cnfClauses); +static array_t *McConvertMintermToValueArrayMine( mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr); +static void McStatePassesOrFailsFormulaMine ( mdd_t *aState, Ctlp_Formula_t *formula, int pass, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm); +static void McStateFailsFormulaMine (mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm); +static void McStatePassesFormulaMine( mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel,Fsm_Fsm_t *modelFsm); + +static int _HrcStringCmp(const void * s1, const void * s2); +static McOptions_t *ParseMcOptions( int argc, char **argv); +static void TimeOutHandle(void); +static Ord_OrderType StringConvertToOrderType(char *string); +static boolean NetworkCheckSuppliedNodeList(Ntk_Network_t * network, lsList suppliedNodeList, Ord_OrderType orderType); +static boolean FileReadNameList(FILE * fp, lsList * nameList, int verbose); +static void _IoGlobalVariablesInitialize(void); +static void _IoGlobalVariablesFree(void); +static void _IoGlobalSubcktInfoFree(void); +static void _IoSubcktArrayFree(array_t *array); +static void _IoSubcktFree(IoSubckt_t *subckt); +static void _IoGlobalResetInfoFree(void); +static boolean _IoNodeTestCompatibilityAux(Hrc_Manager_t *hmgr, Hrc_Node_t *hnode1, Hrc_Node_t *hnode2, boolean mode); +static void _IoManagerCanonicalize(Hrc_Manager_t *hmgr); +static int nodenameCompare(const void * node1, const void * node2); +static void PrintNodeStats(Hrc_Node_t *node, boolean isHnode); +static void NodeListChildren(Hrc_Node_t *hnode, boolean recursiveFlag, int depth); +static array_t *NodeListChildrenMine(Hrc_Node_t *hnode, boolean recursiveFlag, int depth); +static void PrintSpace(int depth); +static int cmp(const void * s1, const void * s2); +static boolean MintermCheckWellFormed(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr); +static boolean SetCheckSupport(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr); + +static char *CNFVariableNameConstructor(char *varName, int varEncoding, int pathIndex); +static void BmcCnfGenerateClausesForPathMine (Ntk_Network_t *network, int from, int to, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); +static void BmcGenerateClausesFromStateTostateMine (bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex); +static void BmcWriteClausesMine( mAig_Manager_t *maigManager, FILE *cnfFile, BmcCnfClauses_t *cnfClauses, BmcOption_t *options); +static int *DecBinConverter (int decValue, int size, int *binValue); +static int SATSolverFileGen (Hrc_Manager_t **hmgr, char *fileName, int steps, BmcOption_t *options); +static int SATSolver (int steps, BmcOption_t *options); +static void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses); +static array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore, satArray_t *clauseIndexInCore); +static st_table * generateAllLatches(Ntk_Network_t * ntk); +static void printSATAssig( array_t* result); +static int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName); + + +/********************************************************/ +/* Main */ +/********************************************************/ + +int main(int argc, char **argv) +{ + vis_stderr =stderr; + vis_stdout = stdout; + + Hrc_Manager_t *hmgrC; + Hrc_Manager_t *hmgrA; + + (void)fprintf(vis_stderr,"\n============= VIS ============= \n\n"); + + + /**** CONCRETE MODEL *****/ + (void)fprintf(vis_stderr,">>>>>>>>>>>>>>>>> CONCRETE MODEL : LOAD & SET UP... \n\n"); + // --- read_blif_mv --- + FILE *fpC; + fpC = Cmd_FileOpen(BLIF_MV_FILE_C1, "r", NIL(char *), 1); + boolean isCanonicalC = 0; + boolean isIncrementalC = 0; + boolean isVerboseC = 0; + hmgrC = read_blif_mvMine (fpC, hmgrC, isCanonicalC, isIncrementalC, isVerboseC); + (void) fprintf(vis_stderr, "*** 'read_blif_mv' of the concrete model completed. *** \n"); + + hmgrGlobalC = hmgrC; + + // --- print_io (display inputs and outputs) --- + int print_ioExecC; + int argcIOC = 1; + char *argvIOC[1] = {"print_io"}; + + print_ioExecC = print_ioMine (&hmgrC, argcIOC, argvIOC); + (void) fprintf(vis_stderr, "*** 'print_io' for concrete model completed. *** \n"); + + // --- init_verify --- + int init_verifyExecC; + int argcIVC = 1; + char *argvIVC[1] = {"init_verify"}; + init_verifyExecC = init_verifyMine (&hmgrC, argcIVC, argvIVC); + (void) fprintf(vis_stderr, "*** 'init_verify' for concrete model completed. *** \n"); + + // --- build_partition_maigs --- + int build_part_maigsExecC; + int argcBPMAIGSC = 1; + char *argvBPMAIGSC[1] = {"build_partition_maigs"}; + build_part_maigsExecC = build_partition_maigsMine (&hmgrC, argcBPMAIGSC, argvBPMAIGSC); + (void) fprintf(vis_stderr, "*** 'build_partition_maigs' for concrete model completed. *** \n"); + + // --- read_fairness --- + int fairnessReadC; + int argcFC = 2; + char *argvFC[2] = {"read_fairness", FAIRNESS_FILE_C1}; + fairnessReadC = read_fairnessMine (&hmgrC, argcFC, argvFC); + (void) fprintf(vis_stderr, "*** 'read_fairness' for concrete model completed. *** \n"); + + // --- print_fairness --- + int fairnessPrintC; + int argcFPC = 1; + char *argvFPC[1] = {"print_fairness"}; + fairnessPrintC = print_fairnessMine (&hmgrC, argcFPC, argvFPC); + (void) fprintf(vis_stderr, "*** 'print_fairness' for concrete model completed. *** \n"); + + +// // --- print_latches (display latches in current node) --- +// int print_latchesExec; +// int argcPL = 1; +// char *argvPL[1]= {"print_latches"}; +// +// print_latchesExec = print_latchesMine (&hmgr, argcPL, argvPL); +// (void) fprintf(vis_stderr, "*** 'print_latches' completed. *** \n"); + + (void)fprintf(vis_stderr,"\n... CONCRETE MODEL : LOAD & SET UP DONE! <<<<<<<<<<<<<<<<\n\n"); + + + + /**** ABSTRACT MODEL *****/ + (void)fprintf(vis_stderr,">>>>>>>>>>>>>>>>> ABSTRACT MODEL : LOAD & SET UP...\n"); + // --- read_blif_mv --- + FILE *fpA; + fpA = Cmd_FileOpen(BLIF_MV_FILE_A1, "r", NIL(char *), 1); + boolean isCanonicalA = 0; + boolean isIncrementalA = 0; + boolean isVerboseA = 0; + hmgrA = read_blif_mvMine (fpA, hmgrA, isCanonicalA, isIncrementalA, isVerboseA); + (void) fprintf(vis_stderr, "*** 'read_blif_mv' of the abstract model completed. *** \n"); + + + // --- print_io (display inputs and outputs) --- + int print_ioExecA; + int argcIOA = 1; + char *argvIOA[1] = {"print_io"}; + + print_ioExecA = print_ioMine (&hmgrA, argcIOA, argvIOA); + (void) fprintf(vis_stderr, "*** 'print_io' for abstract model completed. *** \n"); + + // --- init_verify --- + int init_verifyExecA; + int argcIVA = 1; + char *argvIVA[1] = {"init_verify"}; + init_verifyExecA = init_verifyMine (&hmgrA, argcIVA, argvIVA); + (void) fprintf(vis_stderr, "*** 'init_verify' for abstract model completed. *** \n"); + + // --- read_fairness --- + int fairnessReadA; + int argcFA = 2; + char *argvFA[2] = {"read_fairness", FAIRNESS_FILE_A1}; + fairnessReadA = read_fairnessMine (&hmgrA, argcFA, argvFA); + (void) fprintf(vis_stderr, "*** 'read_fairness' for abstract model completed. *** \n"); + + // --- print_fairness --- + int fairnessPrintA; + int argcFPA = 1; + char *argvFPA[1] = {"print_fairness"}; + fairnessPrintA = print_fairnessMine (&hmgrA, argcFPA, argvFPA); + (void) fprintf(vis_stderr, "*** 'print_fairness' for abstract model completed. *** \n"); + + (void)fprintf(vis_stderr,"\n... ABSTRACT MODEL : LOAD & SET UP DONE! <<<<<<<<<<<<<<<<\n\n"); + + // --- model_check --- + int model_checkExecA; + int argcMCA = 4; +// char *argvMC[2]= {"model_check", "EX_C1/machine_concret.ctl"}; +// char *argvMC[4]= {"model_check", "-d", "3", "EX_C1/machine_concret.ctl"}; +// char *argvMCA[2]= {"model_check", CTL_FILE_A1}; +// char *argvMCA[4]= {"model_check", "-d", "1", CTL_FILE_A1}; + char *argvMCA[4]= {"model_check", "-d", "2", CTL_FILE_A1}; +// char *argvMCA[4]= {"model_check", "-d", "3", CTL_FILE_A1}; +// char *argvMCA[5]= {"model_check", "-i", "-d", "3", CTL_FILE_A1}; +// char *argvMC[6]= {"model_check", "-i", "-W", "-d", "2", "EX_C1/machine_concret.ctl"}; +// char *argvMCA[6]= {"model_check", "-d", "2", "-f", DEBUG_FILE_A1, CTL_FILE_A1}; +// char *argvMC[6]= {"model_check", "-v", "2", "-d", "2", "EX_C1/machine_concret.ctl"}; +// char *argvMC[7]= {"model_check", "-i", "-w", "EX_C1/w_node_file", "-d", "2", "EX_C1/machine_concret.ctl"}; +// char *argvMC[7]= {"model_check", "-d", "3", "-f", DEBUG_FILE_A1, "-i", CTL_FILE_A1}; +// char *argvMC[8]= {"model_check", "-d", "3", "-f", "EX_C1/debug_trace", "-v", "2", "EX_C1/machine_concret.ctl"}; +// char *argvMC[9]= {"model_check", "-d", "3", "-f", "EX_C1/debug_trace", "-i", "-v", "2", "EX_C1/machine_concret.ctl"}; + + model_checkExecA = model_checkMine (&hmgrA, argcMCA, argvMCA); + (void) fprintf(vis_stderr, "*** 'model_check' of abstract model completed. *** \n"); + + + (void) fprintf(vis_stderr,"\n========== END OF VIS ========= \n\n"); + + return 0; + +} + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'Hrc_Manager_t * Io_BlifMvRead( FILE *fp, + Hrc_Manager_t *hmgr, boolean isCanonical, boolean isIncremental, + boolean isVerbose)' in ntkCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static Hrc_Manager_t *read_blif_mvMine (FILE *fp, Hrc_Manager_t *hmgr, + boolean isCanonical, boolean isIncremental, boolean isVerbose) +{ + +(void) fprintf(vis_stderr, "*** 'read_blif_mv' begins. *** \n"); + + Hrc_Node_t *root; + static Hrc_Manager_t *newHmgr; + + if (isIncremental == 0){ + newHmgr = Hrc_ManagerAlloc(); + } + else { /* isIncremental == 1 */ + if (Hrc_ManagerReadCurrentNode(hmgr) == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"No hierarchy has been created. Cannot do inremental read-in.\n"); + return NIL(Hrc_Manager_t); + } + newHmgr = hmgr; + } + + if (setjmp(env)){ + if (isIncremental == 0){ + Hrc_ManagerFree(newHmgr); + } + else { + int i; + /* free all the new models defined in an incremental file */ + for (i=0; i < array_n(globalNewModelArray); i++){ + Hrc_ModelDelete(hmgr,Hrc_ModelReadName(array_fetch(Hrc_Model_t *,globalNewModelArray,i))); + } + } + _IoGlobalVariablesFree(); + return NIL(Hrc_Manager_t); + } + else { + _IoGlobalVariablesInitialize(); + if (isIncremental == 0){ + globalYaccHmgr = newHmgr; + } + else { + globalYaccHmgr = hmgr; + } +#ifdef IODEBUG + IoYydebug = 1; +#endif /* IODEBUG */ + IoYyin = fp; + IoYyrestart(IoYyin); + if (IoYyparse() == 1){ + IoError(); + } + + /* globalNewModelArray contains all the models defined in the previous + IoYyparse(). If isIncremental==0, then they are simply all the models. + If isIncremental==1, then they are new models defined in the file. */ + + if (IoNetworkTestConsistency(newHmgr,globalNewModelArray,globalParserSubcktInfo,globalParserResetInfo,isVerbose) == 0){ + IoError(); + } + + if (globalRootModel == NIL(Hrc_Model_t)){ + globalRootModel = globalFirstModel; + globalRootInstanceName = util_strsav(Hrc_ModelReadName(globalRootModel)); + } + else if (globalRootInstanceName == NIL(char)){ + globalRootInstanceName = util_strsav(Hrc_ModelReadName(globalRootModel)); + } + + if (isCanonical == 1){ + _IoManagerCanonicalize(newHmgr); + } + + root = Hrc_ModelCreateHierarchy(newHmgr,globalRootModel,globalRootInstanceName); + FREE(globalRootInstanceName); + + if (isIncremental == 0){ + Hrc_ManagerSetRootNode(newHmgr,root); + Hrc_ManagerSetCurrentNode(newHmgr,root); + _IoGlobalVariablesFree(); + return newHmgr; + } + else { /* isIncremental == 1, note that newHmgr == hmgr */ + if (_IoNodeTestCompatibility(hmgr,Hrc_ManagerReadCurrentNode(hmgr),root) == 0){ + int i; + (void)fprintf(vis_stderr,"The blif-mv file is not compatible with the existing hierarchy.\n"); + Hrc_TreeReplace(NIL(Hrc_Node_t),root); + /* free all the new models defined in an incremental file */ + for (i=0; i < array_n(globalNewModelArray); i++){ + Hrc_ModelDelete(hmgr,Hrc_ModelReadName(array_fetch(Hrc_Model_t *,globalNewModelArray,i))); + } + _IoGlobalVariablesFree(); + return NIL(Hrc_Manager_t); + } + Hrc_TreeReplace(Hrc_ManagerReadCurrentNode(hmgr),root); + Hrc_ManagerSetCurrentNode(hmgr,root); + _IoGlobalVariablesFree(); + return hmgr; + } + } + + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandInitVerify(Hrc_Manager_t ** hmgr, + int argc, char ** argv);' in ntkCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int init_verifyMine (Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'init_verify' begins. *** \n"); + + int c; + Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + + /* + * Parse the command line. + */ + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "bh")) != EOF) { + switch (c) { + case 'b': + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if (currentNode == NIL(Hrc_Node_t)) { + (void) fprintf(vis_stdout, "The hierarchy manager is empty. Read in design.\n"); + return 1; + } + + +// ++ add condition to test if the functions failed + (void) fprintf(vis_stderr, "---- 'init_verify' : (1) "); + // --- init_verify : (1) flatten_hierarchy --- + int flatten_hierarchyExec; + int argcFH = 1; + char *argvFH[1]= {"flatten_hierarchy"}; + flatten_hierarchyExec = flatten_hierarchyMine (hmgr, argcFH, argvFH); +// flatten_hierarchyExec = flatten_hierarchyMine (&(*hmgr), argcFH, argvFH); + (void) fprintf(vis_stderr, "---- 'init_verify' : (1) *** 'flatten_hierarchy' completed. *** \n"); + + // --- init_verify : (2) static_order --- + (void) fprintf(vis_stderr, "---- 'init_verify' : (2) "); + int static_orderExec; + int argcSO = 1; + char *argvSO[1]= {"static_order"}; + static_orderExec = static_orderMine (hmgr, argcSO, argvSO); + (void) fprintf(vis_stderr, "---- 'init_verify' : (2) *** 'static_order' completed. *** \n"); + + // --- init_verify : (3) build_partition_mdds --- + (void) fprintf(vis_stderr, "---- 'init_verify' : (3) "); + int build_part_mddsExec; + int argcBPMDDS = 1; + char *argvBPMDDS[1]= {"build_partition_mdds"}; + build_part_mddsExec = build_partition_mddsMine (hmgr, argcBPMDDS, argvBPMDDS); + (void) fprintf(vis_stderr, "---- 'init_verify' : (3) *** 'build_partition_mdds' completed. *** \n"); + + return 0; /* normal exit */ + + +usage: + (void) fprintf(vis_stderr, "usage: init_verify [-b] [-h]\n"); + (void) fprintf(vis_stderr, " -b not used any longer.\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + return 1; /* error exit */ + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandFlattenHierarchy(Hrc_Manager_t ** + hmgr, int argc, char ** argv);' in ntkCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int flatten_hierarchyMine (Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'flatten_hierarchy' begins. *** \n"); + + int c; + Ntk_Network_t *network; + char *fileName = NIL(char); + int verbose = 0; /* default */ + int sweep = 1; + lsList varNameList = (lsList) NULL; + Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + + /* + * Parse the command line. + */ + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "a:bhsv:")) != EOF) { + switch (c) { + case 'a': + fileName = util_optarg; + break; + case 'b': + break; + case 'h': + goto usage; + case 's': + sweep = 0; + break; + case 'v': + verbose = atoi(util_optarg); + break; + default: + goto usage; + } + } + + if (currentNode == NIL(Hrc_Node_t)) { + (void) fprintf(vis_stdout, "The hierarchy manager is empty. Read in design.\n"); + return 1; + } + + /* + * Process the file containing the variable names. + */ + if (fileName != NIL(char)) { + FILE *fp = Cmd_FileOpen(fileName, "r", NIL(char *), 0); + if (fp == NIL(FILE)) { + return 1; + } + else { + boolean status; + + error_init(); + status = FileReadNameList(fp, &varNameList, verbose); + (void) fclose(fp); + if (status == FALSE) { + (void) fprintf(vis_stderr, "Error reading variable name file:\n"); + (void) fprintf(vis_stderr, "%s", error_string()); + (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n"); + return 1; + } + } + } + + + /* + * If a network already exists, delete it. Then create the new one, and + * register it with the hrcNode. + */ + network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode, + NTK_HRC_NODE_APPL_KEY); + if (network != NIL(Ntk_Network_t)) { + (void) fprintf(vis_stdout, "Deleting current network and creating new one.\n"); + Hrc_NodeFreeApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY); + } + + error_init(); + + network = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList); + + /* Clean up the varNameList. */ + if (varNameList != (lsList) NULL) { + lsGen gen; + char *varName; + + lsForEachItem(varNameList, gen, varName) { + FREE(varName); + } + (void) lsDestroy(varNameList, (void (*) (lsGeneric)) NULL); + } + /* sweep network */ + if (network != NIL(Ntk_Network_t) && sweep ==1) { + Ntk_NetworkSweep(network, verbose); + } + + if (network == NIL(Ntk_Network_t)) { + (void) fprintf(vis_stderr, "%s", error_string()); + (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n"); + return 1; + } + + Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY, + (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback, + (Hrc_ApplInfoChangeFn) NULL, /* not currently used by hrc */ + (void *) network); + + return 0; /* normal exit */ + +usage: + (void) fprintf(vis_stderr, "usage: flatten_hierarchy [-a file] [-b] [-h] [-s] [-v #]\n"); + (void) fprintf(vis_stderr, " -a file variables to abstract\n"); + (void) fprintf(vis_stderr, " -b not used any longer\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + (void) fprintf(vis_stderr, " -s do not perform a sweep\n"); + (void) fprintf(vis_stderr, " -v # verbosity level\n"); + return 1; /* error exit */ +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandStaticOrder(Hrc_Manager_t ** hmgr, + int argc, char ** argv);' in ordCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int static_orderMine (Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'static_order' begins. *** \n"); + + int c; + FILE *fp; + static int timeOutPeriod; + static int verbose; + static Ord_NodeMethod nodeMethod; + static Ord_RootMethod rootMethod; + static Ord_OrderType suppliedOrderType; + static Ord_OrderType generatedOrderType; + static boolean nsAfterSupport; + lsList suppliedNodeList = (lsList) NULL; + /* list of Ntk_Node_t * */ + Ntk_Network_t *network; + + /* + * These are the default values. These variables must be declared static + * to avoid lint warnings. Since they are static, we must reinitialize + * them outside of the variable declarations. + */ + timeOutPeriod = 0; + verbose = 0; + nodeMethod = Ord_NodesByDefault_c; + rootMethod = Ord_RootsByDefault_c; + suppliedOrderType = Ord_Unassigned_c; /* default */ + generatedOrderType = Ord_InputAndLatch_c;/* default */ + nsAfterSupport = FALSE; /* default */ + + /* + * Parse the command line. + */ + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "av:o:s:t:n:r:h")) != EOF) { + switch (c) { + case 'a': + nsAfterSupport = TRUE; + break; + case 'h': + goto usage; + case 'v': + verbose = atoi(util_optarg); + break; + case 't': + timeOutPeriod = atoi(util_optarg); + break; + case 'o': + generatedOrderType = StringConvertToOrderType(util_optarg); + if ((generatedOrderType == Ord_NextStateNode_c) + || (generatedOrderType == Ord_Partial_c)) { + (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg); + goto usage; + } + else if (generatedOrderType == Ord_Unassigned_c) { + (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg); + goto usage; + } + break; + case 's': + suppliedOrderType = StringConvertToOrderType(util_optarg); + if (suppliedOrderType == Ord_Unassigned_c) { + (void) fprintf(vis_stderr, "unknown input order type: %s\n", util_optarg); + goto usage; + } + break; + case 'n': + if (strcmp("interleave", util_optarg) == 0) { + nodeMethod = Ord_NodesByInterleaving_c; + } + else if (strcmp("merge_left", util_optarg) == 0) { + nodeMethod = Ord_NodesByMergingLeft_c; + } + else if (strcmp("merge_right", util_optarg) == 0) { + nodeMethod = Ord_NodesByMergingRight_c; + } + else if (strcmp("append", util_optarg) == 0) { + nodeMethod = Ord_NodesByAppending_c; + } + else { + (void) fprintf(vis_stderr, "unknown node order method: %s\n", util_optarg); + goto usage; + } + break; + case 'r': + if (strcmp("depth", util_optarg) == 0) { + rootMethod = Ord_RootsByDepth_c; + } + else if (strcmp("mincomm", util_optarg) == 0) { + rootMethod = Ord_RootsByPerm_c; + } + else { + (void) fprintf(vis_stderr, "unknown root order method: %s\n", util_optarg); + goto usage; + } + break; + default: + goto usage; + } + } + + network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + if (network == NIL(Ntk_Network_t)) { + return 1; + } + + if ((suppliedOrderType == Ord_InputAndLatch_c) && (generatedOrderType == Ord_All_c)) { + (void) fprintf(vis_stderr, "-o all -s input_and_latch not currently supported\n"); + return 1; + } + + /* + * The minimum set of variables that can be ordered are those specified by + * Ord_InputAndLatch_c. If these have already been ordered, then just return. + */ + if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) { + (void) fprintf(vis_stderr, "Variables already ordered. "); + (void) fprintf(vis_stderr, "Reinvoke flatten_hierarchy to undo variable ordering.\n"); + return 1; + } + + + /* + * Process the input ordering file. + */ + if (suppliedOrderType == Ord_Unassigned_c) { + if (argc - util_optind > 0) { + (void) fprintf(vis_stderr, "must specify -s if supplying order file\n"); + goto usage; + } + } + else { + if (argc - util_optind == 0) { + (void) fprintf(vis_stderr, "order file not provided\n"); + goto usage; + } + else if (argc - util_optind > 1) { + (void) fprintf(vis_stderr, "too many arguments\n"); + goto usage; + } + + fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + if (fp == NIL(FILE)) { + (void) fprintf(vis_stderr, "File %s is not readable, please check if it exists\n", argv[util_optind]); + return 1; + } + else { + boolean status; + + error_init(); + status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose); + if (status == FALSE) { + (void) fprintf(vis_stderr, "Error reading ordering file:\n"); + (void) fprintf(vis_stderr, "%s", error_string()); + (void) fprintf(vis_stderr, "Cannot perform static ordering.\n"); + (void) fclose(fp); + return 1; + } + else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList, + suppliedOrderType) == FALSE) { + (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n"); + (void) fprintf(vis_stderr, "%s", error_string()); + (void) fprintf(vis_stderr, "Cannot perform static ordering.\n"); + (void) fclose(fp); + (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); + return 1; + } + else { + (void) fclose(fp); + if (verbose > 0) { + (void) fprintf(vis_stdout, "\nNodes supplied in ordering file, "); + (void) fprintf(vis_stdout, "according to -s option: \n"); + OrdNodeListWrite(vis_stdout, suppliedNodeList); + } + } + } + } + + + /* + * In order for static ordering to proceed, network must not have any + * combinational cycles. + */ + error_init(); + if(Ntk_NetworkTestIsAcyclic(network) == 0) { + (void) fprintf(vis_stderr, "Combinational cycle found: "); + (void) fprintf(vis_stderr, "%s\n", error_string()); + (void) fprintf(vis_stderr, "cannot perform static ordering\n"); + if (suppliedOrderType != Ord_Unassigned_c) { + (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); + } + return 1; + } + + /* Start the timer before calling the variable ordering routine. */ + if (timeOutPeriod > 0){ + (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); + (void) alarm(timeOutPeriod); + if (setjmp(timeOutEnv) > 0) { + (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod); + alarm(0); + return 1; + } + } + + /* + * Order the variables. + */ + Ord_NetworkOrderVariables(network, rootMethod, nodeMethod, nsAfterSupport, + generatedOrderType, suppliedOrderType, + suppliedNodeList, verbose); + + if (suppliedOrderType != Ord_Unassigned_c) { + (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); + } + + /* + * As a sanity check, make sure that all the variables in generatedOrderType + * have an MDD id. + */ + assert(Ord_NetworkTestAreVariablesOrdered(network, generatedOrderType)); + + alarm(0); + return 0; /* Everything okay */ + + usage: + (void) fprintf(vis_stderr, "usage: static_order [-a] [-h] [-n method] [-o type] [-r method] -s type [-t time] [-v #] file\n"); + (void) fprintf(vis_stderr, " -a order NS variables after support\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + (void) fprintf(vis_stderr, " -n method node ordering method\n"); + (void) fprintf(vis_stderr, " (interleave (default), append, merge_left, merge_right)\n"); + (void) fprintf(vis_stderr, " -o type nodes to order (all, input_and_latch (default))\n"); + (void) fprintf(vis_stderr, " -r method root ordering method (depth, mincomm (default for < 30 latches))\n"); + (void) fprintf(vis_stderr, " -s type nodes in file (all, input_and_latch, next_state_node, partial)\n"); + (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); + (void) fprintf(vis_stderr, " -v # verbosity level\n"); + (void) fprintf(vis_stderr, " file supplied ordering of nodes\n"); + + return 1; + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandBuildPartitionMdds(Hrc_Manager_t ** + hmgr, int argc, char ** argv);' in partCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int build_partition_mddsMine (Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'build_partition_mdds' begins. *** \n"); + + static Part_PartitionMethod method; + static boolean inTermsOfLeaves; + lsList nodeList = lsCreate(); + graph_t *partition; + static int verbose; + static int sanityCheck; + static int timeOutPeriod; + int c; + int length; + char *methodString; + char *modelName; + Hrc_Node_t *currentNode; + Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + char *nodeName; + char *tmpNodeName; + char *realName; + FILE *nodeFile; + static boolean fileUsed; + + fileUsed = FALSE; + inTermsOfLeaves = FALSE; + verbose = 0; + sanityCheck = 0; + timeOutPeriod = 0; + + nodeFile = NIL(FILE); + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "f:hvin:s:t:")) != EOF) { + switch(c) { + case 'f': + fileUsed = TRUE; + nodeFile = Cmd_FileOpen(util_optarg, "r", &realName, 1); + FREE(realName); + if (nodeFile == NIL(FILE)){ + (void)fprintf(vis_stderr,"Cannot open %s\n", util_optarg); + lsDestroy(nodeList, (void (*)(lsGeneric))0); + return 1; + } + else{ + tmpNodeName = ALLOC(char, 512); + while(fscanf(nodeFile, "%s\n", tmpNodeName) != EOF){ + if(*tmpNodeName != '#'){ + nodeName = ALLOC(char, strlen(tmpNodeName) + 2); + sprintf(nodeName, "%s", tmpNodeName); + lsNewEnd(nodeList, (lsGeneric)nodeName, NIL(lsHandle)); + } + } + FREE(tmpNodeName); + } + break; + case 'h': + goto usage; + case 'i': + inTermsOfLeaves = TRUE; + break; + case 'v': + verbose = 1; + break; + case 's': + sanityCheck = atoi(util_optarg); + break; + case 't': + timeOutPeriod = atoi(util_optarg); + break; + case 'n': + length = strlen(util_optarg); + for(c = 0; c < length; c++) { + if (util_optarg[c] == ',') { + util_optarg[c] = 0; + } /* End of if */ + } /* End of for */ + c = 0; + while (c < length) { + lsNewEnd(nodeList, &util_optarg[c], NIL(lsHandle)); + while (util_optarg[c++] != 0); + } /* End of while */ + break; + default: + goto usage; + } + } + + if (argc == util_optind) { + /* No method specified. Choosing default */ + methodString = Cmd_FlagReadByName("partition_method"); + if (methodString == NIL(char)) { + methodString = "default"; + } + } + else { + methodString = argv[util_optind]; + } + + if (strcmp(methodString,"inout") == 0) { + method = Part_InOut_c; + if (lsLength(nodeList) != 0) { + (void) fprintf(vis_stderr, "Ignoring provided list of nodes in "); + (void) fprintf(vis_stderr, " method\n"); + } /* End of if */ + if (inTermsOfLeaves) { + (void) fprintf(vis_stderr, "Ignoring -i flag in the method\n"); + } /* End of if */ + } + else if (strcmp(methodString,"partial") == 0) { + method = Part_Partial_c; + /* Make sure a list of nodes has been provided */ + if (lsLength(nodeList) == 0) { + (void) fprintf(vis_stderr, "Method requires a non-empty list"); + (void) fprintf(vis_stderr, " of nodes\n"); + + lsDestroy(nodeList, (void (*)(lsGeneric))0); + goto usage; + } /* End of if */ + } + else if (strcmp(methodString,"total") == 0) { + method = Part_Total_c; + if (lsLength(nodeList) != 0) { + (void) fprintf(vis_stderr, "Ignoring provided list of nodes in "); + (void) fprintf(vis_stderr, " method\n"); + } /* End of if */ + } + else if (strcmp(methodString,"frontier") == 0) { + method = Part_Frontier_c; + } + else if (strcmp(methodString,"boundary") == 0) { + method = Part_Boundary_c; + } + else if (strcmp(methodString, "fine") == 0) { + method = Part_Fine_c; + } + else if (strcmp(methodString, "default") == 0) { + method = Part_Default_c; + } + else { + goto usage; + } + + + /* Check if the network has been read in */ + if (network == NIL(Ntk_Network_t)) { + lsDestroy(nodeList, (void (*)(lsGeneric))0); + return 1; + } + + /* Check if the network has the variables ordered */ + if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == + FALSE) { + (void) fprintf(vis_stdout, "The MDD variables have not been ordered. Use static_order.\n"); + + lsDestroy(nodeList, (void (*)(lsGeneric))0); + return 1; + } + + /* Check if there is already a partition attached to the network */ + partition = (graph_t *) Ntk_NetworkReadApplInfo(network, + PART_NETWORK_APPL_KEY); + + /* If there is, just return. */ + if (partition != NIL(graph_t)) { + (void) fprintf(vis_stderr, "partition already built; reinvoke "); + (void) fprintf(vis_stderr, "flatten_hierarchy to remove the current partition\n"); + return 1; + } + + /* Read the name of the model to be passed to Part_NetworkCreatePartition */ + currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + modelName = Hrc_NodeReadModelName(currentNode); + + /* Set the timeout */ + if (timeOutPeriod > 0) { + (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); + (void) alarm(timeOutPeriod); + if (setjmp(timeOutEnv) > 0) { + (void) fprintf(vis_stdout, "Partition: timeout occurred after "); + (void) fprintf(vis_stdout, "%d seconds\n", timeOutPeriod); + alarm(0); + + /* Partial clean up */ + lsDestroy(nodeList, (void (*)(lsGeneric))0); + return 1; + } + } + + /* + * Execute the partition algorithm. The two nil pointers is to indicate + * that the graph must represent the complete network. + */ + partition = Part_NetworkCreatePartition(network, currentNode, modelName, (lsList)0, + (lsList)0, NIL(mdd_t), method, nodeList, + inTermsOfLeaves, verbose, + sanityCheck); + + /* Register the partition in the network if any */ + Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY, + (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, + (void *) partition); + + /* Deactivate the alarm */ + alarm(0); + + /* Clean up */ + if(fileUsed){ + lsDestroy(nodeList, PartNameFree); + } + else{ + lsDestroy(nodeList, (void (*)(lsGeneric))0); + } + return 0; + +usage: + (void) fprintf(vis_stderr, "usage: build_partition_mdds [options] [method]\n"); + (void) fprintf(vis_stderr, "Options:\n"); + (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); + (void) fprintf(vis_stderr, " -i\t\tBuild the functions in the partition in terms of the\n"); + (void) fprintf(vis_stderr, " \t\tcombinational inputs of the system. This option is redundant if\n"); + (void) fprintf(vis_stderr, " \t\tthe inout partition is chosen.\n"); + (void) fprintf(vis_stderr, " -n \tComma separated list of network nodes to preserve in the\n"); + (void) fprintf(vis_stderr, " \tpartitioning. It only matters if the partial method has been\n"); + (void) fprintf(vis_stderr, " \tselected.\n"); + (void) fprintf(vis_stderr, " -f \tSpecifies the file containing names of network nodes\n"); + (void) fprintf(vis_stderr, " \tto preserve while partitioning. This option matters only \n"); + (void) fprintf(vis_stderr, " \tif the partial method has been selected. Each node name must\n"); + (void) fprintf(vis_stderr, " \tbe listed on a new line. Comments in must begin with '#'.\n"); + (void) fprintf(vis_stderr, " -s \tLevel of severity check applied after computation. 0 being no\n"); + (void) fprintf(vis_stderr, " \t\tcheck, 1 begin simple check and >1 being exhaustive check.\n"); + (void) fprintf(vis_stderr, " -t \tTime in seconds allowed to build the partition. If the\n"); + (void) fprintf(vis_stderr, " \tcomputation time goes above that limit, the process of building\n"); + (void) fprintf(vis_stderr, " \tthe partition is aborted.\n"); + (void) fprintf(vis_stderr, " -v\t\tverbose\n"); + (void) fprintf(vis_stderr, "Methods\n"); + (void) fprintf(vis_stderr, " inout\tIt represents the network with one MDD for\n"); + (void) fprintf(vis_stderr, " \teach combinational output as a function of the combinational\n"); + (void) fprintf(vis_stderr, " \tinputs\n"); + (void) fprintf(vis_stderr, " total\tPartitions the network preserving its structure. Every node in\n"); + (void) fprintf(vis_stderr, " \tthe network will produce a vertex in the partition graph. The\n"); + (void) fprintf(vis_stderr, " \tflag -i explained above controls the support of\n"); + (void) fprintf(vis_stderr, " \tthe functions attached to the vertices.\n"); + (void) fprintf(vis_stderr, " frontier\tThe default method. Partitions the network creating vertices for intermediate nodes\n"); + (void) fprintf(vis_stderr, " \tas necessary to control the BDD size. The threshold value of the\n"); + (void) fprintf(vis_stderr, " \tBDD can be specified by partition_threshold.\n"); + (void) fprintf(vis_stderr, " partial\tPartitions the network preserving certain nodes specified with\n"); + (void) fprintf(vis_stderr, " \tthe option -n or -f.\n"); + (void) fprintf(vis_stderr, " boundary\tPartitions the network preserving all nodes that are \n"); + (void) fprintf(vis_stderr, " \tsubcircuit IOs.\n"); + + lsDestroy(nodeList, (void (*)(lsGeneric))0); + + return 1; /* Error exit */ +} /* End of CommandBuildPartitionMdds */ + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandBuildPartitionMAigs(Hrc_Manager_t + ** hmgr, int argc, char ** argv);' in ntmaigCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int build_partition_maigsMine(Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'build_partition_maigs' begins. *** \n"); + + Ntk_Node_t *node, *latch; + lsGen gen; + array_t *result; /* array of MvfAig_Function_t* */ + array_t *roots; + st_table *leaves; + array_t *inputs; + Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + mAig_Manager_t *manager; + MvfAig_Function_t *mvfAig; + st_table *nodeToMvfAigTable; /* mapes each node with its mvfAig */ + int c, sweepFlag, DFSFlag; + int i; + + sweepFlag = 1; + DFSFlag = 0; + util_getopt_reset(); + while ((c = util_getopt(argc,argv,"sdnh")) != EOF){ + switch(c){ + case 's': + sweepFlag = 1; + break; + case 'd': + DFSFlag = 1; + break; + case 'n': + sweepFlag = 0; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if (network == NIL(Ntk_Network_t)) { + return 1; + } + + manager = Ntk_NetworkReadMAigManager(network); + + if (manager == NIL(mAig_Manager_t)) { + manager = mAig_initAig(); + Ntk_NetworkSetMAigManager(network, manager); + /* + mAig_mAigSetNetwork(manager, network); + */ + } + + /* Check if there is already a MvfAigs Table attached to the network */ + nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, + MVFAIG_NETWORK_APPL_KEY); + + if (nodeToMvfAigTable != NIL(st_table)){ + /* + st_foreach_item(nodeToMvfAigTable, stGen, (char **) &node, (char **) &MvfAig) { + printf("\nNode name = %s :",Ntk_NodeReadName(node)); + for (j=0; j< array_n(MvfAig); j++){ + printf(" %d ",array_fetch(bAigEdge_t, (array_t *) MvfAig, j)); + } + } + */ + (void) fprintf(vis_stderr, "maig partition already built; reinvoke\n"); + (void) fprintf(vis_stderr, "flatten_hierarchy to remove the current maig partition\n"); + return 1; + } + + roots = array_alloc(Ntk_Node_t *, 0); + Ntk_NetworkForEachCombOutput(network, gen, node) { + array_insert_last(Ntk_Node_t *, roots, node); + } + Ntk_NetworkForEachNode(network, gen, node) { + if(Ntk_NodeTestIsShadow(node)) continue; + if(Ntk_NodeTestIsCombInput(node)) continue; + if(Ntk_NodeTestIsCombOutput(node))continue; + + if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) { + /** + fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node)); + **/ + array_insert_last(Ntk_Node_t *, roots, node); + } + } + + leaves = st_init_table(st_ptrcmp, st_ptrhash); + + inputs = array_alloc(Ntk_Node_t *, 16); + Ntk_NetworkForEachCombInput(network, gen, node) { + array_insert_last(Ntk_Node_t *, inputs, node); + } + array_sort(inputs, nodenameCompare); + for(i=0; inum = 0; + Ntk_NetworkForEachLatch(network, gen, latch) { + if(!st_lookup(nodeToMvfAigTable, latch, &mvfAig)) + array_insert_last(Ntk_Node_t *, roots, latch); + } + result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves); + + array_free(roots); + array_free(inputs); + st_free_table(leaves); + + /* + * Free the array of MvfAigs. + */ + MvfAig_FunctionArrayFree(result); + + if(sweepFlag) + bAig_BddSweepMain(network, 0); + + return 0; + +usage: + (void) fprintf(vis_stderr, "usage: build_partition_maig [-h]\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + (void) fprintf(vis_stderr, " -n disable bdd sweeping\n"); + (void) fprintf(vis_stderr, " -d build AIG DFS manner\n"); + return 1; /* error exit */ + +} + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandReadFairness(Hrc_Manager_t ** hmgr, + int argc, char ** argv)' in fsmCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static int read_fairnessMine (Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + +(void) fprintf(vis_stderr, "*** 'read_fairness' begins. *** \n"); + + int c; + FILE *fp; + array_t *formulaArray; + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + + /* + * Parse command line options. + */ + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c) { + case 'h': + goto usage; + default: + goto usage; + } + /* NOT REACHED */ + } + + if (fsm == NIL(Fsm_Fsm_t)) { + (void) fprintf(vis_stderr, "** fair error: Fairness constraint not recorded.\n"); + return 1; + } + + /* + * Open the fairness file. + */ + if (argc - util_optind == 0) { + (void) fprintf(vis_stderr, "** fair error: fairness file not provided\n"); + goto usage; + } + else if (argc - util_optind > 1) { + (void) fprintf(vis_stderr, "** fair error: too many arguments\n"); + goto usage; + } + + fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + if (fp == NIL(FILE)) { + return 1; + } + + /* + * Parse the formulas in the file. + */ + formulaArray = Ctlp_FileParseFormulaArray(fp); + (void) fclose(fp); + + if (formulaArray == NIL(array_t)) { + (void) fprintf(vis_stderr, "** fair error: error reading fairness conditions.\n"); + return 1; + } + else if (array_n(formulaArray) == 0) { + (void) fprintf(vis_stderr, "** fair error: fairness file is empty.\n"); + (void) fprintf(vis_stderr, "** fair error: Use reset_fairness to reset the fairness constraint."); + return 1; + } + else { + int j; + Fsm_Fairness_t *fairness; + Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm); + + /* + * First check that each formula is semantically correct wrt the network. + */ + error_init(); + for (j = 0; j < array_n(formulaArray); j++) { + Ctlp_Formula_t *formula; + boolean status; + + formula = array_fetch(Ctlp_Formula_t *, formulaArray, j); + status = Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE); + + if (status == FALSE) { + (void) fprintf(vis_stderr, + "** fair error: error reading fairness constraint "); + Ctlp_FormulaPrint(vis_stderr, formula); + (void) fprintf(vis_stderr, ":\n"); + (void) fprintf(vis_stderr, "%s", error_string()); + (void) fprintf(vis_stderr, "\n"); + return 1; + } + } + + + /* + * Interpret the array of CTL formulas as a set of Buchi conditions. + * Hence, create a single disjunct, consisting of k conjuncts, where k is + * the number of CTL formulas read in. The jth conjunct has the jth + * formula as its finallyInf component, and NULL as its globallyInf + * component. + */ + fairness = FsmFairnessAlloc(fsm); + for (j = 0; j < array_n(formulaArray); j++) { + Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j); + + FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j); + } + array_free(formulaArray); /* Don't free the formulas themselves. */ + + /* + * Remove any existing fairnessInfo associated with the FSM, and update + * the fairnessInfo.constraint with the new fairness just read. + */ + FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t)); + + return 0; + } + + usage: + (void) fprintf(vis_stderr, "usage: read_fairness [-h] file\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + (void) fprintf(vis_stderr, " file file containing the list of conditions\n"); + return 1; + +} + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandPrintFairness(Hrc_Manager_t ** hmgr, + int argc, char ** argv)' in fsmCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static int print_fairnessMine(Hrc_Manager_t ** hmgr, int argc, char ** argv) +{ + + (void) fprintf(vis_stderr, "*** 'print_fairness' begins. *** \n"); + + int c; + Fsm_Fairness_t *constraint; + int numDisjuncts; + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + + /* + * Parse command line options. + */ + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c) { + case 'h': + goto usage; + default: + goto usage; + } + /* NOT REACHED */ + } + + if (fsm == NIL(Fsm_Fsm_t)) { + return 1; + } + + /* + * Print the fairness constraint. It is assumed that there is at least one + * disjunct present. Currently, only Buchi constraints can be printed out. + */ + constraint = Fsm_FsmReadFairnessConstraint(fsm); + assert(constraint != NIL(Fsm_Fairness_t)); + numDisjuncts = Fsm_FairnessReadNumDisjuncts(constraint); + assert(numDisjuncts != 0); + + if (numDisjuncts > 1) { + (void) fprintf(vis_stdout, "Fairness constraint not Buchi..."); + (void) fprintf(vis_stdout, "don't know how to print.\n"); + } + else { + int i; + int numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(constraint, 0); + + (void) fprintf(vis_stdout, "Fairness constraint:\n"); + for (i = 0; i < numConjuncts; i++) { + if (Fsm_FairnessReadGloballyInfFormula(constraint, 0, i) != + NIL(Ctlp_Formula_t)) { + (void) fprintf(vis_stdout, "Fairness constraint not Buchi..."); + (void) fprintf(vis_stdout, "don't know how to print.\n"); + } + + Ctlp_FormulaPrint(vis_stdout, + Fsm_FairnessReadFinallyInfFormula(constraint, 0, i)); + (void) fprintf(vis_stdout, ";\n"); + } + } + + return 0; + + usage: + (void) fprintf(vis_stderr, "usage: print_fairness [-h]\n"); + (void) fprintf(vis_stderr, " -h print the command usage\n"); + return 1; + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandPrintIo(Hrc_Manager_t **hmgr, int + argc, char **argv);' in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static int print_ioMine (Hrc_Manager_t **hmgr, int argc, char **argv) +{ + +(void) fprintf(vis_stderr, "*** 'print_io' begins. *** \n"); + + int c, i; + Hrc_Node_t *node; + Var_Variable_t *var; + array_t *tmpArray; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c){ + case 'h': + goto usage; + default: + goto usage; + } + } + /* if there are some arguments left */ + if (argc != util_optind){ + goto usage; + } + node = Hrc_ManagerReadCurrentNode(*hmgr); + if (node == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"No file has been read in.\n"); + return 1; + } + + if (Hrc_NodeReadNumFormalInputs(node) == 0){ + fprintf(vis_stdout,"No inputs\n"); + } + else { + tmpArray = array_alloc(char *,0); + Hrc_NodeForEachFormalInput(node,i,var){ + array_insert_last(char *,tmpArray,Var_VariableReadName(var)); + } + array_sort(tmpArray,_HrcStringCmp); + fprintf(vis_stdout,"inputs:"); + for (i=0; i < array_n(tmpArray); i++){ + fprintf(vis_stdout," %s",array_fetch(char *,tmpArray,i)); + } + fprintf(vis_stdout,"\n"); + array_free(tmpArray); + } + + if (Hrc_NodeReadNumFormalOutputs(node) == 0){ + fprintf(vis_stdout,"No outputs\n"); + } + else { + tmpArray = array_alloc(char *,0); + Hrc_NodeForEachFormalOutput(node,i,var){ + array_insert_last(char *,tmpArray,Var_VariableReadName(var)); + } + array_sort(tmpArray,_HrcStringCmp); + fprintf(vis_stdout,"outputs:"); + for (i=0; i < array_n(tmpArray); i++){ + fprintf(vis_stdout," %s",array_fetch(char *,tmpArray,i)); + } + fprintf(vis_stdout,"\n"); + array_free(tmpArray); + } + return 0; + +usage: + (void) fprintf(vis_stderr,"usage: print_io [-h]\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + return 1; + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandMc (Hrc_Manager_t **hmgr, int argc, + char **argv)' function in mcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int model_checkMine (Hrc_Manager_t **hmgr, int argc, char **argv) +{ + +(void) fprintf(vis_stderr, "*** 'model_check' begins. *** \n"); + +/* options */ + McOptions_t *options; + Mc_VerbosityLevel verbosity; + Mc_DcLevel dcLevel; + FILE *ctlFile; + int timeOutPeriod = 0; + Mc_FwdBwdAnalysis traversalDirection; + int buildOnionRings = 0; + FILE *guideFile; + FILE *systemFile; + Mc_GuidedSearch_t guidedSearchType = Mc_None_c; + Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t); + array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */ + st_table *systemVarBddIdTable; + boolean noShare = 0; + Mc_GSHScheduleType GSHschedule; + boolean checkVacuity; + boolean performCoverageHoskote; + boolean performCoverageImproved; + + /* CTL formulae */ + array_t *ctlArray; + array_t *ctlNormalFormulaArray; + int i; + int numFormulae; + /* FSM, network and image */ + Fsm_Fsm_t *totalFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *modelFsm = NIL(Fsm_Fsm_t); + Fsm_Fsm_t *reducedFsm = NIL(Fsm_Fsm_t); + Ntk_Network_t *network; + mdd_t *modelCareStates = NIL(mdd_t); + array_t *modelCareStatesArray = NIL(array_t); + mdd_t *modelInitialStates; + mdd_t *fairStates; + Fsm_Fairness_t *fairCond; + mdd_manager *mddMgr; + array_t *bddIdArray; + Img_ImageInfo_t *imageInfo; + Mc_EarlyTermination_t *earlyTermination; + /* Coverage estimation */ + mdd_t *totalcoveredstates = NIL(mdd_t); + array_t *signalTypeList = array_alloc(int,0); + array_t *signalList = array_alloc(char *,0); + array_t *statesCoveredList = array_alloc(mdd_t *,0); + array_t *newCoveredStatesList = array_alloc(mdd_t *,0); + array_t *statesToRemoveList = array_alloc(mdd_t *,0); + + /* Early termination is only partially implemented right now. It needs + distribution over all operators, including limited cases of temporal + operators. That should be relatively easy to implement. */ + + /* time keeping */ + long totalInitialTime; /* for model checking */ + long initialTime, finalTime; /* for model checking */ + + error_init(); + Img_ResetNumberOfImageComputation(Img_Both_c); + + /* read options */ + if (!(options = ParseMcOptions(argc, argv))) { + return 1; + } + verbosity = McOptionsReadVerbosityLevel(options); + dcLevel = McOptionsReadDcLevel(options); + ctlFile = McOptionsReadCtlFile(options); + timeOutPeriod = McOptionsReadTimeOutPeriod(options); + traversalDirection = McOptionsReadTraversalDirection(options); + buildOnionRings = + (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); + noShare = McOptionsReadUseFormulaTree(options); + GSHschedule = McOptionsReadSchedule(options); + checkVacuity = McOptionsReadVacuityDetect(options); + /* for the command mc -C foo.ctl */ + performCoverageHoskote = McOptionsReadCoverageHoskote(options); + /* for the command mc -I foo.ctl */ + performCoverageImproved = McOptionsReadCoverageImproved(options); + + /* Check for incompatible options and do some option-specific + * intializations. + */ + + if (traversalDirection == McFwd_c) { + if (checkVacuity) { + fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n"); + McOptionsFree(options); + return 1; + } + } + + if (checkVacuity) { + if (performCoverageHoskote || performCoverageImproved) { + fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n"); + McOptionsFree(options); + return 1; + } + } + + guideFile = McOptionsReadGuideFile(options); + + if(guideFile != NIL(FILE) ){ + guidedSearchType = Mc_ReadGuidedSearchType(); + if(guidedSearchType == Mc_None_c){ /* illegal setting */ + fprintf(vis_stderr, "** mc error: Unknown hint type\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(traversalDirection == McFwd_c){ /* illegal combination */ + fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + if(Img_UserSpecifiedMethod() != Img_Iwls95_c && + Img_UserSpecifiedMethod() != Img_Monolithic_c && + Img_UserSpecifiedMethod() != Img_Mlp_c){ + fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n"); + fclose(guideFile); + McOptionsFree(options); + return 1; + } + + hintsArray = Mc_ReadHints(guideFile); + fclose(guideFile); guideFile = NIL(FILE); + if( hintsArray == NIL(array_t) ){ + McOptionsFree(options); + return 1; + } + + } /* if guided search */ + + /* If don't-cares are used, -r implies -c. Note that the satisfying + sets of a subformula are only in terms of propositions therein + and their cone of influence. Hence, we can share satisfying sets + among formulae. I don't quite understand what the problem with + don't-cares is (RB) */ + if (McOptionsReadReduceFsm(options)) + if (dcLevel != McDcLevelNone_c) + McOptionsSetUseFormulaTree(options, TRUE); + + if (traversalDirection == McFwd_c && + McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { + McOptionsSetDbgLevel(options, McDbgLevelNone_c); + (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n"); + } + + /* Read CTL formulae */ + ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile); + fclose(ctlFile); ctlFile = NIL(FILE); + if (ctlArray == NIL(array_t)) { + (void) fprintf(vis_stderr, + "** mc error: error in parsing formulas from file\n"); + McOptionsFree(options); + return 1; + } + + /* read network */ + network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + if (network == NIL(Ntk_Network_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* read fsm */ + totalFsm = Fsm_NetworkReadOrCreateFsm(network); + if (totalFsm == NIL(Fsm_Fsm_t)) { + fprintf(vis_stdout, "%s\n", error_string()); + error_init(); + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + + /* Assign variables to system if doing FAFW */ + systemVarBddIdTable = NIL(st_table); + systemFile = McOptionsReadSystemFile(options); + if (systemFile != NIL(FILE)) { + systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile); + fclose(systemFile); systemFile = NIL(FILE); + if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */ + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + return 1; + } + } /* if FAFW */ + + if(options->FAFWFlag && systemVarBddIdTable == 0) { + systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm); + } + + if (verbosity > McVerbosityNone_c) + totalInitialTime = util_cpu_time(); + else /* to remove uninitialized variable warning */ + totalInitialTime = 0; + + if(traversalDirection == McFwd_c){ + mdd_t *totalInitialStates; + double nInitialStates; + + totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm); + nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm), + totalInitialStates, + Fsm_FsmReadPresentStateVars(totalFsm)); + mdd_free(totalInitialStates); + + /* If the number of initial states is only one, we can use both + * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE), + * however, if we have multiple initial states, we should use + * p0 ^ !f == FALSE. + */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0), + noShare); + /* end conversion for forward traversal */ + } else if (noShare) { /* conversion for backward, no sharing */ + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + }else{ /* conversion for backward, with sharing */ + /* Note that converting to DAG after converting to existential form would + lead to more sharing, but it cannot be done since equal subformula that + are converted from different formulae need different pointers back to + their originals */ + if (checkVacuity) { + ctlNormalFormulaArray = + Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray); + } + else { + array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray ); + array_free( ctlArray ); + ctlArray = temp; + ctlNormalFormulaArray = + Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray); + } + } + /* At this point, ctlNormalFormulaArray contains the formulas that are + actually going to be checked, and ctlArray contains the formulas from + which the conversion has been done. Both need to be kept around until the + end, for debugging purposes. */ + + numFormulae = array_n(ctlNormalFormulaArray); + + /* time out */ + if (timeOutPeriod > 0) { + /* Set the static variables used by the signal handler. */ + mcTimeOut = timeOutPeriod; + alarmLapTime = util_cpu_ctime(); + (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); + (void) alarm(timeOutPeriod); + if (setjmp(timeOutEnv) > 0) { + (void) fprintf(vis_stdout, + "# MC: timeout occurred after %d seconds.\n", timeOutPeriod); + (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n"); + if (verbosity > McVerbosityNone_c) { + fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + } + alarm(0); + return 1; + } + } + + + /* Create reduced fsm, if necessary */ + if (!McOptionsReadReduceFsm(options)){ + /* We want to minimize only when "-r" option is not specified */ + /* reduceFsm would be NIL, if there is no reduction observed */ + assert (reducedFsm == NIL(Fsm_Fsm_t)); + reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray); + if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + } + + /************** for all formulae **********************************/ + for(i = 0; i < numFormulae; i++) { + int nImgComps, nPreComps; + boolean result; + Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *, + ctlNormalFormulaArray, i); + + modelFsm = NIL(Fsm_Fsm_t); + + /* do a check */ + if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) { + (void) fprintf(vis_stdout, + "** mc error: error in parsing Atomic Formula:\n%s\n", + error_string()); + error_init(); + Ctlp_FormulaFree(ctlFormula); + continue; + } + + /* Create reduced fsm */ + if (McOptionsReadReduceFsm(options)) { + /* We have not done top level reduction. */ + /* Using the same variable reducedFsm here */ + array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1); + + assert(reducedFsm == NIL(Fsm_Fsm_t)); + array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula); + reducedFsm = McConstructReducedFsm(network, oneFormulaArray); + array_free(oneFormulaArray); + + if (reducedFsm && verbosity != McVerbosityNone_c) { + mddMgr = Fsm_FsmReadMddManager(reducedFsm); + bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, + Fsm_FsmReadPresentStateVars(reducedFsm)); + (void)fprintf(vis_stdout,"Local system includes "); + (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n", + array_n(Fsm_FsmReadPresentStateVars(reducedFsm)), + array_n(bddIdArray)); + array_free(bddIdArray); + } + }/* if readreducefsm */ + + /* Let us see if we got any reduction via top level or via "-r" */ + if (reducedFsm == NIL(Fsm_Fsm_t)) + modelFsm = totalFsm; /* no reduction */ + else + modelFsm = reducedFsm; /* some reduction at some point */ + + /* compute initial states */ + modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm); + if (modelInitialStates == NIL(mdd_t)) { + int j; + (void) fprintf(vis_stdout, + "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n", + error_string()); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + + alarm(0); + + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + + Ctlp_FormulaArrayFree( ctlArray ); + + McOptionsFree(options); + + return 1; + } + + earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates); + + if(hintsArray != NIL(Ctlp_FormulaArray_t)) { + hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray); + if( hintsStatesArray == NIL(array_t) || + (guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) { + int j; + + if( guidedSearchType == Mc_Global_c && + Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c) + fprintf(vis_stderr, "** mc error: global hints incompatible with " + "mixed formulae\n"); + + Mc_EarlyTerminationFree(earlyTermination); + mdd_free(modelInitialStates); + if (modelFsm != totalFsm) + Fsm_FsmFree(reducedFsm); + alarm(0); + for(j = i; j < numFormulae; j++) + Ctlp_FormulaFree( + array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) ); + array_free( ctlNormalFormulaArray ); + Ctlp_FormulaArrayFree( ctlArray ); + McOptionsFree(options); + return 1; + } /* problem with hints */ + } /* hints exist */ + + /* stats */ + if (verbosity > McVerbosityNone_c) { + initialTime = util_cpu_time(); + nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); + nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); + } else { /* to remove uninitialized variable warnings */ + initialTime = 0; + nImgComps = 0; + nPreComps = 0; + } + mddMgr = Fsm_FsmReadMddManager(modelFsm); + + /* compute don't cares. */ + if (modelCareStatesArray == NIL(array_t)) { + long iTime; /* starting time for reachability analysis */ + if (verbosity > McVerbosityNone_c && i == 0) + iTime = util_cpu_time(); + else /* to remove uninitialized variable warnings */ + iTime = 0; + + /* ardc */ + if (dcLevel == McDcLevelArdc_c) { + Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options); + + modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates( + modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions); + if (verbosity > McVerbosityNone_c && i == 0) + Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime); + + /* rch dc */ + } else if (dcLevel >= McDcLevelRch_c) { + modelCareStates = + Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0, + Fsm_Rch_Default_c, 0, 0, + NIL(array_t), FALSE, NIL(array_t)); + if (verbosity > McVerbosityNone_c && i == 0) { + Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime, + Fsm_Rch_Default_c); + } + + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } else { + modelCareStates = mdd_one(mddMgr); + modelCareStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates); + } + } + + Fsm_MinimizeTransitionRelationWithReachabilityInfo( + modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c, + verbosity > 1); + + /* fairness conditions */ + fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray, + verbosity, dcLevel, GSHschedule, + McBwd_c, FALSE); + fairCond = Fsm_FsmReadFairnessConstraint(modelFsm); + + if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) { + (void)fprintf(vis_stdout, + "** mc warning: There are no fair initial states\n"); + } + else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) { + (void)fprintf(vis_stdout, + "** mc warning: Some initial states are not fair\n"); + } + + /* some user feedback */ + if (verbosity != McVerbosityNone_c) { + (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1); + Ctlp_FormulaPrint(vis_stdout, + Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void)fprintf (vis_stdout, "\n"); + if (traversalDirection == McFwd_c) { + (void)fprintf(vis_stdout, "Forward formula : "); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + (void)fprintf(vis_stdout, "\n"); + } + } + + /************** the actual computation **********************************/ + if (checkVacuity) { + McVacuityDetection(modelFsm, ctlFormula, i, + fairStates, fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, modelInitialStates, + options); + } + else { /* Normal Model Checking */ + mdd_t *ctlFormulaStates = + Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, + fairCond, modelCareStatesArray, + earlyTermination, hintsStatesArray, + guidedSearchType, verbosity, dcLevel, + buildOnionRings, GSHschedule); + + McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond, + modelCareStatesArray, earlyTermination, + hintsStatesArray, guidedSearchType, verbosity, + dcLevel, buildOnionRings, GSHschedule, + traversalDirection, modelInitialStates, + ctlFormulaStates, &totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + newCoveredStatesList, statesToRemoveList, + performCoverageHoskote, performCoverageImproved); + + Mc_EarlyTerminationFree(earlyTermination); + if(hintsStatesArray != NIL(array_t)) + mdd_array_free(hintsStatesArray); + /* Set up things for possible FAFW analysis of counterexample. */ + Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag); + Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable); + /* user feedback on succes/fail */ + result = McPrintPassFailMine(mddMgr, modelFsm, traversalDirection, + ctlFormula, ctlFormulaStates, + modelInitialStates, modelCareStatesArray, + options, verbosity); + Fsm_FsmSetFAFWFlag(modelFsm, 0); + Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL); + mdd_free(ctlFormulaStates); + } + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- mc time = %10g\n", + (double)(finalTime - initialTime) / 1000.0); + fprintf(vis_stdout, + "-- %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, + Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); + } + mdd_free(modelInitialStates); + mdd_free(fairStates); + Ctlp_FormulaFree(ctlFormula); + + if ((McOptionsReadReduceFsm(options)) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* + ** We need to free the reducedFsm only if it was created under "-r" + ** option and was non-NIL. + */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + modelCareStates = NIL(mdd_t); + modelCareStatesArray = NIL(array_t); + } else if (modelCareStatesArray) { + modelCareStatesArray = NIL(array_t); + } + } + }/* for all formulae */ + + if (verbosity > McVerbosityNone_c) { + finalTime = util_cpu_time(); + fprintf(vis_stdout, "-- total mc time = %10g\n", + (double)(finalTime - totalInitialTime) / 1000.0); + fprintf(vis_stdout, + "-- total %d image computations and %d preimage computations\n", + Img_GetNumberOfImageComputation(Img_Forward_c), + Img_GetNumberOfImageComputation(Img_Backward_c)); + /* Print tfm options if we have a global fsm. */ + if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) { + imageInfo = Fsm_FsmReadImageInfo(modelFsm); + if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || + Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { + Img_TfmPrintStatistics(imageInfo, Img_Both_c); + } + } + } + + /* Print results of coverage computation */ + McPrintCoverageSummary(modelFsm, dcLevel, + options, modelCareStatesArray, + modelCareStates, totalcoveredstates, + signalTypeList, signalList, statesCoveredList, + performCoverageHoskote, performCoverageImproved); + mdd_array_free(newCoveredStatesList); + mdd_array_free(statesToRemoveList); + array_free(signalTypeList); + array_free(signalList); + mdd_array_free(statesCoveredList); + if (totalcoveredstates != NIL(mdd_t)) + mdd_free(totalcoveredstates); + + if (modelCareStates) { + mdd_array_free(modelCareStatesArray); + } + + if(hintsArray) + Ctlp_FormulaArrayFree(hintsArray); + + if ((McOptionsReadReduceFsm(options) == FALSE) && + (reducedFsm != NIL(Fsm_Fsm_t))) { + /* If "-r" was not specified and we did some reduction at top + level, we need to free it */ + Fsm_FsmFree(reducedFsm); + reducedFsm = NIL(Fsm_Fsm_t); + modelFsm = NIL(Fsm_Fsm_t); + } + + if(systemVarBddIdTable) + st_free_table(systemVarBddIdTable); + array_free(ctlNormalFormulaArray); + (void) fprintf(vis_stdout, "\n"); + + Ctlp_FormulaArrayFree(ctlArray); + McOptionsFree(options); + alarm(0); + return 0; + +} + + +/**Function******************************************************************** + + Synopsis [Parse command line options for mc.] + + SideEffects [] + +******************************************************************************/ +static McOptions_t * +ParseMcOptions( + int argc, + char **argv) +{ + unsigned int i; + int c; + char *guideFileName = NIL(char); + char *variablesForSystem = NIL(char); + FILE *guideFile = NIL(FILE); + FILE *systemFile = NIL(FILE); + boolean doCoverageHoskote = FALSE; + boolean doCoverageImproved = FALSE; + boolean useMore = FALSE; + boolean reduceFsm = FALSE; + boolean printInputs = FALSE; + boolean useFormulaTree = FALSE; + boolean vd = FALSE; + boolean beer = FALSE; + boolean FAFWFlag = FALSE; + boolean GFAFWFlag = FALSE; + FILE *inputFp=NIL(FILE); + FILE *debugOut=NIL(FILE); + char *debugOutName=NIL(char); + Mc_DcLevel dcLevel = McDcLevelRch_c; + McDbgLevel dbgLevel = McDbgLevelNone_c; + Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c; + Mc_FwdBwdAnalysis fwdBwd = McFwd_c; + McOptions_t *options = McOptionsAlloc(); + int timeOutPeriod = 0; + Mc_FwdBwdAnalysis traversalDirection = McBwd_c; + Fsm_ArdcOptions_t *ardcOptions; + Mc_GSHScheduleType schedule = McGSH_EL_c; + + /* + * Parse command line options. + */ + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "bcirmg:hv:d:D:VBf:t:CIFR:S:GWw:")) != EOF) { + switch(c) { + case 'g': + guideFileName = util_strsav(util_optarg); + break; + case 'h': + goto usage; + case 'v': + for (i = 0; i < strlen(util_optarg); i++) { + if (!isdigit((int)util_optarg[i])) { + goto usage; + } + } + verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg); + break; + case 'd': + for (i = 0; i < strlen(util_optarg); i++) { + if (!isdigit((int)util_optarg[i])) { + goto usage; + } + } + dbgLevel = (McDbgLevel) atoi(util_optarg); + break; + case 'D': + for (i = 0; i < strlen(util_optarg); i++) { + if (!isdigit((int)util_optarg[i])) { + goto usage; + } + } + dcLevel = (Mc_DcLevel) atoi(util_optarg); + break; + case 'b': + fwdBwd = McBwd_c; + break; + case 'V': /*Vacuity detection option*/ + vd = TRUE; + break; + case 'B': /*Vacuity detection Beer et al method option*/ + vd = TRUE; + beer = TRUE; + break; + case 'f': + debugOutName = util_strsav(util_optarg); + break; + case 'm': + useMore = TRUE; + break; + case 'r' : + reduceFsm = TRUE; + break; + case 'c': + useFormulaTree = TRUE; + break; + case 't' : + timeOutPeriod = atoi(util_optarg); + break; + case 'i' : + printInputs = TRUE; + break; + case 'F' : + traversalDirection = McFwd_c; + break; + case 'S' : + schedule = McStringConvertToScheduleType(util_optarg); + break; + case 'w': + variablesForSystem = util_strsav(util_optarg); + case 'W': + FAFWFlag = 1; + break; + case 'G': + GFAFWFlag = 1; + break; + case 'C' : + doCoverageHoskote = TRUE; + break; + case 'I' : + doCoverageImproved = TRUE; + break; + default: + goto usage; + } + } + + /* + * Open the ctl file. + */ + if (argc - util_optind == 0) { + (void) fprintf(vis_stderr, "** mc error: file containing ctl formulas not provided\n"); + goto usage; + } + else if (argc - util_optind > 1) { + (void) fprintf(vis_stderr, "** mc error: too many arguments\n"); + goto usage; + } + + McOptionsSetFwdBwd(options, fwdBwd); + McOptionsSetUseMore(options, useMore); + McOptionsSetReduceFsm(options, reduceFsm); + McOptionsSetVacuityDetect(options, vd); + McOptionsSetBeerMethod(options, beer); + McOptionsSetUseFormulaTree(options, useFormulaTree); + McOptionsSetPrintInputs(options, printInputs); + McOptionsSetTimeOutPeriod(options, timeOutPeriod); + McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag); + McOptionsSetCoverageHoskote(options, doCoverageHoskote); + McOptionsSetCoverageImproved(options, doCoverageImproved); + + if((FAFWFlag > 0 || GFAFWFlag > 0) && dbgLevel == 0) { + fprintf(vis_stderr, "** mc warning : -w and -W options are ignored without -d option\n"); + } + + if((FAFWFlag > 0 || GFAFWFlag > 0) && printInputs == 0) { + fprintf(vis_stderr, "** mc warning : -i is recommended with -w or -W option\n"); + } + if(FAFWFlag) { + if (bdd_get_package_name() != CUDD) { + fprintf(vis_stderr, "** mc warning : -w and -W option is only available with CUDD\n"); + FAFWFlag = 0; + FREE(variablesForSystem); + variablesForSystem = NIL(char); + } + } + + + if (schedule == McGSH_Unassigned_c) { + (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg); + goto usage; + } else { + McOptionsSetSchedule(options, schedule); + } + inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + if (inputFp == NIL(FILE)) { + McOptionsFree(options); + if (guideFileName != NIL(char)) FREE(guideFileName); + return NIL(McOptions_t); + } + McOptionsSetCtlFile(options, inputFp); + + if (debugOutName != NIL(char)) { + debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0); + FREE(debugOutName); + if (debugOut == NIL(FILE)) { + McOptionsFree(options); + if (guideFileName != NIL(char)) FREE(guideFileName); + return NIL(McOptions_t); + } + } + McOptionsSetDebugFile(options, debugOut); + + + if (guideFileName != NIL(char)) { + guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0); + if (guideFile == NIL(FILE)) { + fprintf(vis_stderr, "** mc error: cannot open guided search file %s.\n", + guideFileName); + FREE(guideFileName); + guideFileName = NIL(char); + McOptionsFree(options); + return NIL(McOptions_t); + } + FREE(guideFileName); + guideFileName = NIL(char); + } + McOptionsSetGuideFile(options, guideFile); + + if (variablesForSystem != NIL(char)) { + systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0); + if (systemFile == NIL(FILE)) { + fprintf(vis_stderr, "** mc error: cannot open system variables file for FAFW %s.\n", + variablesForSystem); + FREE(variablesForSystem); + variablesForSystem = NIL(char); + McOptionsFree(options); + return NIL(McOptions_t); + } + FREE(variablesForSystem); + variablesForSystem = NIL(char); + } + McOptionsSetVariablesForSystem(options, systemFile); + + if ((verbosityLevel != McVerbosityNone_c) && + (verbosityLevel != McVerbosityLittle_c) && + (verbosityLevel != McVerbositySome_c) && + (verbosityLevel != McVerbosityMax_c)) { + goto usage; + } + else { + McOptionsSetVerbosityLevel(options, verbosityLevel); + } + + if ((dbgLevel != McDbgLevelNone_c) && + (dbgLevel != McDbgLevelMin_c) && + (dbgLevel != McDbgLevelMinVerbose_c) && + (dbgLevel != McDbgLevelMax_c) && + (dbgLevel != McDbgLevelInteractive_c)) { + goto usage; + } + else { + McOptionsSetDbgLevel(options, dbgLevel); + } + + if ((dcLevel != McDcLevelNone_c) && + (dcLevel != McDcLevelRch_c ) && + (dcLevel != McDcLevelRchFrontier_c ) && + (dcLevel != McDcLevelArdc_c )) { + goto usage; + } + else { + McOptionsSetDcLevel(options, dcLevel); + } + + McOptionsSetTraversalDirection(options, traversalDirection); + if (dcLevel == McDcLevelArdc_c) { + ardcOptions = Fsm_ArdcAllocOptionsStruct(); + Fsm_ArdcGetDefaultOptions(ardcOptions); + } else + ardcOptions = NIL(Fsm_ArdcOptions_t); + McOptionsSetArdcOptions(options, ardcOptions); + + return options; + + usage: + (void) fprintf(vis_stderr, "usage: model_check [-b][-c][-d dbg_level][-f dbg_file][-g ][-h][-i][-m][-r][-V][-B][-t period][-C][-I][-P][-v verbosity_level][-D dc_level][-F][-S ] \n"); + (void) fprintf(vis_stderr, " -b \tUse backward analysis in debugging\n"); + (void) fprintf(vis_stderr, " -c \tNo sharing of CTL parse tree. This option does not matter for vacuity detection.\n"); + (void) fprintf(vis_stderr, " -d \n"); + (void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n"); + (void) fprintf(vis_stderr, " debug_level = 1 => automatic minimal debugging\n"); + (void) fprintf(vis_stderr, " debug_level = 2 => automatic minimal debugging with extra verbosity\n"); + (void) fprintf(vis_stderr, " debug_level = 3 => automatic maximal debugging\n"); + (void) fprintf(vis_stderr, " debug_level = 4 => interactive debugging\n"); + (void) fprintf(vis_stderr, " -f \n"); + (void) fprintf(vis_stderr, " write error trace to dbg_out\n"); + (void) fprintf(vis_stderr, " -g \tSpecify file for guided search.\n"); + (void) fprintf(vis_stderr, " -h \tPrints this usage message.\n"); + (void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n"); + (void) fprintf(vis_stderr, " -m \tPipe debug output through more.\n"); + (void) fprintf(vis_stderr, " -r reduce FSM with respect to formula being verified\n"); + (void) fprintf(vis_stderr, " -t time out period\n"); + (void) fprintf(vis_stderr, " -v \n"); + (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); + (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); + (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); + (void) fprintf(vis_stderr, " -w \tSpecify variables controlled by system.\n"); + (void) fprintf(vis_stderr, " -B vacuity detection for w-ACTL formulae using method of Beer et al \n"); + (void) fprintf(vis_stderr, " -C Compute coverage of all observable signals using Hoskote et.al's implementation\n"); + (void) fprintf(vis_stderr, " -D \n"); + (void) fprintf(vis_stderr, " dc_level = 0 => no use of don't cares\n"); + (void) fprintf(vis_stderr, " dc_level = 1 => use unreached states as don't cares (Default)\n"); + (void) fprintf(vis_stderr, " dc_level = 2 => use unreached states as don't cares\n"); + + (void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n"); + (void) fprintf(vis_stderr, " dc_level = 3 => use over-approximate unreached states as don't cares\n"); + (void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n"); + (void) fprintf(vis_stderr, " -F \tUse forward model checking.\n"); + (void) fprintf(vis_stderr, " -G \tUse general fate and free will algorithm.\n"); + (void) fprintf(vis_stderr, " -I Compute coverage of all observable signals using improved coverage implementation\n"); + (void) fprintf(vis_stderr, " -S \n"); + (void) fprintf(vis_stderr, " schedule is one of {EL,EL1,EL2,budget,random,off}\n"); + (void) fprintf(vis_stderr, " -V thorough vacuity detection\n"); + (void) fprintf(vis_stderr, " -W \tUse fate and free will algorithm when all the variables are controlled by system.\n"); + (void) fprintf(vis_stderr, " The input file containing CTL formula to be checked.\n"); + + if (guideFileName != NIL(char)) FREE(guideFileName); + McOptionsFree(options); + + return NIL(McOptions_t); +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandPrintModels (Hrc_Manager_t **hmgr, + int argc, char **argv)' function in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static int print_modelsMine(Hrc_Manager_t **hmgr, int argc, char **argv) +{ + + (void) fprintf(vis_stderr, "*** 'print_models' begins. *** \n"); + + st_generator *gen; + char *name; + Hrc_Model_t *model; + Hrc_Node_t *node; + int c; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c){ + case 'h': + goto usage; + default: + goto usage; + } + } + if(argc != 1) { + goto usage; + } + + node = Hrc_ManagerReadCurrentNode(*hmgr); + if (node == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"No file has been read in.\n"); + return 1; + } + + Hrc_ManagerForEachModel(*hmgr, gen, name, model) { + PrintNodeStats(Hrc_ModelReadMasterNode(model), FALSE); + (void) fprintf(vis_stdout, "subckts = %d\n", + st_count(Hrc_ModelReadSubcktTable(model))); + } + return 0; + +usage: + (void) fprintf(vis_stderr, "usage: print_models [-h]\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + return 1; + +} + +/**Function******************************************************************** + + Synopsis [This function prints the statistics of a node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +PrintNodeStats( + Hrc_Node_t *node, + boolean isHnode) +{ + (void) fprintf(vis_stdout, "Model name = %s", Hrc_NodeReadModelName(node)); + if(isHnode) { + (void) fprintf(vis_stdout, ", Instance name = %s\n", + Hrc_NodeReadInstanceName(node)); + } + else { + (void) fprintf(vis_stdout, "\n"); + } + (void) fprintf(vis_stdout, "inputs = %d,", Hrc_NodeReadNumFormalInputs(node)); + (void) fprintf(vis_stdout, " outputs = %d,", Hrc_NodeReadNumFormalOutputs(node)); + (void) fprintf(vis_stdout, " variables = %d,", Hrc_NodeReadNumVariables(node)); + (void) fprintf(vis_stdout, " tables = %d,", Hrc_NodeReadNumTables(node)); + (void) fprintf(vis_stdout, " latches = %d", Hrc_NodeReadNumLatches(node)); + if(isHnode) { + (void) fprintf(vis_stdout, ", children = %d\n", Hrc_NodeReadNumChildren(node)); + } + else { + (void) fprintf(vis_stdout, "\n"); + } +} + +/**Function******************************************************************** + + Synopsis [returns child or parent node (it is actually the current node)] + + Description [Refer to 'static int CommandCd (Hrc_Manager_t **hmgr, + int argc, char **argv)' function in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static Hrc_Node_t *cdMine(Hrc_Manager_t **hmgr, int argc, char **argv) +{ + + (void) fprintf(vis_stderr, "*** 'cd' begins. *** \n"); + + Hrc_Node_t *currentNode, *parent, *child; + int c; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c){ + case 'h': + goto usage; + default: + goto usage; + } + } + + if (argc != 2){ + goto usage; + } + + currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + if (currentNode == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stdout,"No file has been read in.\n"); + return NIL(Hrc_Node_t); + } + /* go to the parent node */ + if (strcmp(*(++argv),"..") == 0){ + if ((parent = Hrc_NodeReadParentNode(currentNode)) == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"You are at the root node. Can't cd to a parent.\n"); + return currentNode; + } + Hrc_ManagerSetCurrentNode(*hmgr,parent); + return parent; + } + + if ((child = Hrc_NodeFindChildByName(currentNode,*argv)) == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"No child node whose name is %s exists in the current node.\n",*argv); + return currentNode; + } + Hrc_ManagerSetCurrentNode(*hmgr,child); + return child; + +usage: + (void)fprintf(vis_stderr,"usage: cd [-h] child_name or cd ..\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + return NIL(Hrc_Node_t); +} + + +/**Function******************************************************************** + + Synopsis [returns current node] + + Description [Refer to 'static int CommandLs (Hrc_Manager_t **hmgr, + int argc, char **argv)' function in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static Hrc_Node_t *lsMine(Hrc_Manager_t **hmgr, int argc, char **argv){ + + (void) fprintf(vis_stderr, "*** 'ls' begins. *** \n"); + + int recursiveFlag = 0; + int c; + Hrc_Node_t *currentNode; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "hR")) != EOF) { + switch(c){ + case 'h': + goto usage; + case 'R': + recursiveFlag = 1; + break; + default: + goto usage; + } + } + /* if there are some arguments for ls */ + if (argc != util_optind){ + goto usage; + } + + currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + if (currentNode == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stdout,"No file has been read in.\n"); + return NIL(Hrc_Node_t); + } + NodeListChildren(currentNode, recursiveFlag, 0); + return currentNode; + +usage: + (void)fprintf(vis_stderr,"usage: ls [-h] [-R]\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + (void) fprintf(vis_stderr, " -R \t\tprint recursive tree\n"); + + return NIL(Hrc_Node_t); + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandPwd (Hrc_Manager_t **hmgr, + int argc, char **argv)' function in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static char *pwdMine(Hrc_Manager_t **hmgr, int argc, char **argv){ + + (void) fprintf(vis_stderr, "*** 'pwd' begins. *** \n"); + + Hrc_Node_t *currentNode; + Hrc_Node_t *rootNode; + char *separator, *hierarchicalName; + int c; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c){ + case 'h': + goto usage; + default: + goto usage; + } + } + if (argc != 1){ + goto usage; + } + + currentNode = Hrc_ManagerReadCurrentNode(*hmgr); + if (currentNode == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stdout,"No file has been read in.\n"); + return NIL(char); + } + rootNode = Hrc_ManagerReadRootNode(*hmgr); + separator = (char *) ((rootNode == currentNode) ? "" : "."); + hierarchicalName = Hrc_NodeFindHierarchicalName(currentNode, FALSE); + (void)fprintf(vis_stdout,"%s%s%s\n", Hrc_NodeReadInstanceName(rootNode), + separator, hierarchicalName); + (void) sprintf(currentPath, "%s%s%s", Hrc_NodeReadInstanceName(rootNode), separator, hierarchicalName); + FREE(hierarchicalName); + return currentPath; + +usage: + (void)fprintf(vis_stderr,"usage: pwd [-h]\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + return NIL(char); + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [Refer to 'static int CommandPrintLatches (Hrc_Manager_t **hmgr, + int argc, char **argv)' function in hrcCmd.c] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int print_latchesMine(Hrc_Manager_t **hmgr, int argc, char **argv){ + + (void) fprintf(vis_stderr, "*** 'print_latches' begins. *** \n"); + + int c, i; + Hrc_Node_t *node; + st_generator *gen; + char *latchName; + Hrc_Latch_t *latch; + array_t *tmpArray; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c){ + case 'h': + goto usage; + default: + goto usage; + } + } + /* if there are some arguments left */ + if (argc != util_optind){ + goto usage; + } + node = Hrc_ManagerReadCurrentNode(*hmgr); + if (node == NIL(Hrc_Node_t)){ + (void)fprintf(vis_stderr,"No file has been read in.\n"); + return 1; + } + + if (Hrc_NodeReadNumLatches(node) == 0){ + fprintf(vis_stdout,"No latches\n"); + } + else { + tmpArray = array_alloc(char *,0); + Hrc_NodeForEachLatch(node,gen,latchName,latch){ + array_insert_last(char *,tmpArray,latchName); + } + array_sort(tmpArray,_HrcStringCmp); + for (i=0; i < array_n(tmpArray); i++){ + fprintf(vis_stdout,"%s ",array_fetch(char *,tmpArray,i)); + } + fprintf(vis_stdout,"\n"); + array_free(tmpArray); + } + return 0; + +usage: + (void) fprintf(vis_stderr,"usage: print_latches [-h]\n"); + (void) fprintf(vis_stderr, " -h \t\tprint the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [Converts a string to an order type.] + + Description [Converts a string to an order type. If string does not refer to + one of the allowed order types, then returns Ord_Unassigned_c.] + + SideEffects [] + +******************************************************************************/ +static Ord_OrderType +StringConvertToOrderType( + char *string) +{ + if (strcmp("all", string) == 0) { + return Ord_All_c; + } + else if (strcmp("input_and_latch", string) == 0) { + return Ord_InputAndLatch_c; + } + else if (strcmp("next_state_node", string) == 0) { + return Ord_NextStateNode_c; + } + else if (strcmp("partial", string) == 0) { + return Ord_Partial_c; + } + else { + return Ord_Unassigned_c; + } +} + + +/**Function******************************************************************** + + Synopsis [The core routine for the command ls.] + + Description [The core routine for the command ls. If the second argument + is set to 1, it calls the ls routine recursively all the way down to leaves.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +NodeListChildren( + Hrc_Node_t *hnode, + boolean recursiveFlag, + int depth) +{ + st_generator *gen; + char *childName; + Hrc_Node_t *child; + int newDepth, i; + array_t *tmpArray; + + newDepth = depth + 1; + tmpArray = array_alloc(char *,0); + Hrc_NodeForEachChild(hnode,gen,childName,child){ + array_insert_last(char *,tmpArray,childName); + } + array_sort(tmpArray,_HrcStringCmp); + for (i=0; i < array_n(tmpArray); i++){ + PrintSpace(depth); + childName = array_fetch(char *,tmpArray,i); + (void)fprintf(vis_stdout,"%s\n",childName); + if (recursiveFlag == 1){ + NodeListChildren(Hrc_NodeFindChildByName(hnode,childName),recursiveFlag,newDepth); + } + } + array_free(tmpArray); +} + +/**Function******************************************************************** + + Synopsis [The core routine for the command ls. Returns array_t] + + Description [The core routine for the command ls. If the second argument + is set to 1, it calls the ls routine recursively all the way down to leaves.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static array_t *NodeListChildrenMine(Hrc_Node_t *hnode, boolean recursiveFlag, int depth){ + + st_generator *gen; + char *childName; + Hrc_Node_t *child; + int newDepth, i; + array_t *tmpArray; + + newDepth = depth + 1; + tmpArray = array_alloc(char *,0); + Hrc_NodeForEachChild(hnode,gen,childName,child){ + array_insert_last(char *,tmpArray,childName); + } + array_sort(tmpArray,_HrcStringCmp); + for (i=0; i < array_n(tmpArray); i++){ + PrintSpace(depth); + childName = array_fetch(char *,tmpArray,i); + (void)fprintf(vis_stdout,"%s\n",childName); + if (recursiveFlag == 1){ + NodeListChildren(Hrc_NodeFindChildByName(hnode,childName),recursiveFlag,newDepth); + } + } +// array_free(tmpArray); + return tmpArray; +} + +/**Function******************************************************************** + + Synopsis [Prints out spaces.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +PrintSpace(int depth) +{ + int i; + for (i=0; i < depth; i++){ + (void)fprintf(vis_stdout," "); + } +} + + +/**Function******************************************************************** + + Synopsis [Verifies that suppliedNodeList has the correct nodes.] + + Description [Returns TRUE if the set of nodes in suppliedNodeList matches + the set of nodes in network specified by orderType; else returns FALSE and + writes a message to error_string. OrderType should be one of the following: + 1) Ord_All_c: should match the set of all nodes in network; 2) + Ord_InputAndLatch_c: should match the set of inputs (primary + pseudo), + latches, and next state nodes; 3) Ord_NextStateNode_c: should match the set + of next state nodes; number should be the number of latches; 4) + Ord_Partial_c: returns TRUE automatically.] + + SideEffects [] + +******************************************************************************/ +static boolean +NetworkCheckSuppliedNodeList( + Ntk_Network_t * network, + lsList suppliedNodeList, + Ord_OrderType orderType) +{ + lsGen gen; + st_generator *stGen; + Ntk_Node_t *node; + st_table *requiredNodes; + st_table *suppliedNodes; + char *dummy; + boolean returnFlag = TRUE; + + assert(orderType != Ord_Unassigned_c); + + if (orderType == Ord_Partial_c) { + return TRUE; + } + + /* At this point, orderType must be one of the these. */ + assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c) + || (orderType == Ord_NextStateNode_c)); + + + /* + * Build up the table of required nodes. Next state nodes are included by + * all 3 order types. + */ + requiredNodes = st_init_table(st_ptrcmp, st_ptrhash); + Ntk_NetworkForEachNode(network, gen, node) { + if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) { + st_insert(requiredNodes, (char *) node, NIL(char)); + } + else if ((orderType == Ord_InputAndLatch_c) + && Ntk_NodeTestIsCombInput(node)) { + st_insert(requiredNodes, (char *) node, NIL(char)); + } + /* else, this node is not included by orderType */ + } + + /* + * Convert suppliedNodeList to the table of supplied nodes. + */ + suppliedNodes = st_init_table(st_ptrcmp, st_ptrhash); + lsForEachItem(suppliedNodeList, gen, node) { + int status = st_insert(suppliedNodes, (char *) node, NIL(char)); + if (status) { + error_append("node "); + error_append(Ntk_NodeReadName(node)); + error_append(" appears more than once in ordering file\n"); + returnFlag = FALSE; + } + } + + /* + * Check that suppliedNodes is contained in requiredNodes. + */ + st_foreach_item(suppliedNodes, stGen, &node, &dummy) { + if (!st_is_member(requiredNodes, node)) { + error_append("node "); + error_append(Ntk_NodeReadName(node)); + error_append(" supplied but not required\n"); + returnFlag = FALSE; + } + } + + /* + * Check that suppliedNodes is contained in requiredNodes. + */ + st_foreach_item(requiredNodes, stGen, &node, &dummy) { + if (!st_is_member(suppliedNodes, node)) { + error_append("node "); + error_append(Ntk_NodeReadName(node)); + error_append(" required but not supplied\n"); + returnFlag = FALSE; + } + } + + st_free_table(requiredNodes); + st_free_table(suppliedNodes); + return returnFlag; +} + +/**Function******************************************************************** + + Synopsis [Returns a list of names corresponding to the names in a file.] + + Description [Parses a file and builds a name list corresponding to the names + found in the first "column" of each line of the file. Any line starting + with the comment character '#' or white space is ignored. No checks are + made to see if the names are well-formed in any respect. If a problem is + found while parsing the file (e.g. name length exceeded), then a message is + written to error_string, the partial name list is freed, and the function + returns FALSE; otherwise, it returns TRUE, and a pointer to a list is + returned.] + + Comment [The parser consists of 3 states. See the documentation + accompanying the #defines defining the state names. This code was adapted + from Ord_FileReadNodeList.] + + SideEffects [] + +******************************************************************************/ +static boolean +FileReadNameList( + FILE * fp, + lsList * nameList /* of char *, for return */, + int verbose) +{ + int c; + int state; + int curPosition = 0; + char *name; + char string[MAX_NAME_LENGTH]; + boolean returnFlag = TRUE; + + *nameList = lsCreate(); + + state = STATE_TEST; + while ((c = fgetc(fp)) != EOF) { + + switch (state) { + case STATE_TEST: + /* At start of a new line. */ + if (c == '#') { + /* Line starting with comment character; wait for newline */ + state = STATE_WAIT; + } + else if ((c == ' ') || (c == '\t')) { + /* Line starting with white space; wait for newline */ + state = STATE_WAIT; + } + else if (c == '\n') { + /* Line starting with newline; go to next line */ + state = STATE_TEST; + } + else { + /* Assume starting a name. */ + curPosition = 0; + string[curPosition++] = c; + state = STATE_IN; + } + break; + case STATE_WAIT: + /* + * Waiting for the newline character. + */ + state = (c == '\n') ? STATE_TEST : STATE_WAIT; + break; + case STATE_IN: + /* + * Parsing a name. If white space reached, then terminate the + * name and process it. Else, continue parsing. + */ + if ((c == ' ') || (c == '\n') || (c == '\t')) { + string[curPosition] = '\0'; + name = util_strsav(string); + if (verbose > 1) { + (void) fprintf(vis_stdout, "Reading name: %s\n", name); + } + (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH); + + state = (c == '\n') ? STATE_TEST : STATE_WAIT; + } + else { + string[curPosition++] = c; + if (curPosition >= MAX_NAME_LENGTH) { + error_append("maximum name length exceeded"); + returnFlag = FALSE; + } + state = STATE_IN; /* redundant, but be explicit */ + } + break; + default: + fail("unrecognized state"); + } + } + + /* + * Handle case where EOF terminates a name. + */ + if (state == STATE_IN) { + string[curPosition] = '\0'; + name = util_strsav(string); + if (verbose > 1) { + (void) fprintf(vis_stdout, "Reading name: %s\n", name); + } + (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH); + + } + + if (returnFlag) { + return TRUE; + } + else { + (void) lsDestroy(*nameList, (void (*) (lsGeneric)) NULL); + return FALSE; + } +} + +/**Function******************************************************************** + + Synopsis [Initilizes all the global variables used in the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoGlobalVariablesInitialize(void) +{ + globalLineNumber = 1; + globalModel = NIL(Hrc_Model_t); + globalHnode = NIL(Hrc_Node_t); + globalFirstModel = NIL(Hrc_Model_t); /* set once */ + globalRootModel = NIL(Hrc_Model_t); /* set once */ + globalRootInstanceName = NIL(char); /* set once */ + globalMvNameArray = NIL(array_t); + globalSymValueArray = NIL(array_t); + globalTableInputArray = NIL(array_t); + globalTableOutputArray = NIL(array_t); + globalTableDefaultArray = NIL(array_t); + globalTableSymCubeArray = NIL(array_t); + globalFormalNameArray = NIL(array_t); + globalActualNameArray = NIL(array_t); + + globalSubcktArray = NIL(array_t); + globalResetArray = NIL(array_t); + + globalNewModelArray = array_alloc(Hrc_Model_t *,0); + + globalCurrentStackDepth = 0; + + /* a hash table from a model name to an array of resets/subcircuits in the model */ + globalParserResetInfo = st_init_table(st_ptrcmp,st_ptrhash); + globalParserSubcktInfo = st_init_table(st_ptrcmp,st_ptrhash); +} + +/**Function******************************************************************** + + Synopsis [Frees all the global data structures used in the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoGlobalVariablesFree(void) +{ + array_free(globalNewModelArray); + _IoGlobalResetInfoFree(); + _IoGlobalSubcktInfoFree(); +} + + +/**Function******************************************************************** + + Synopsis [Frees the subckt information only used by the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoGlobalSubcktInfoFree(void) +{ + st_generator *gen; + char *key, *val; + + st_foreach_item(globalParserSubcktInfo,gen,&key,&val){ + if ((array_t *)val != NIL(array_t)){ + _IoSubcktArrayFree((array_t *)val); + } + } + st_free_table(globalParserSubcktInfo); +} + + +/**Function******************************************************************** + + Synopsis [Frees an array of the subckt data structure only used by the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoSubcktArrayFree(array_t *array) +{ + int i; + + for (i=0; i < array_n(array); i++){ + _IoSubcktFree(array_fetch(IoSubckt_t *,array,i)); + } + array_free(array); +} + +/**Function******************************************************************** + + Synopsis [Frees the subckt data structure used by the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoSubcktFree(IoSubckt_t *subckt) +{ + FREE(subckt->modelName); + FREE(subckt->instanceName); + IoStringArrayFree(subckt->formalNameArray); + IoStringArrayFree(subckt->actualNameArray); + FREE(subckt); +} + + +/**Function******************************************************************** + + Synopsis [Frees the reset data structure used only by the parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +_IoGlobalResetInfoFree(void) +{ + st_generator *gen; + char *key, *val; + int i; + Tbl_Table_t *resetTable; + + st_foreach_item(globalParserResetInfo,gen,&key,&val){ + if ((array_t *)val != NIL(array_t)){ + for (i=0; i < array_n((array_t *)val); i++){ + resetTable = array_fetch(Tbl_Table_t *,(array_t *)val,i); + if (resetTable != NIL(Tbl_Table_t)){ + Tbl_TableFree(resetTable); + } + } + array_free((array_t *)val); + } + } + st_free_table(globalParserResetInfo); +} + + +/**Function******************************************************************** + + Synopsis [Checks if two hnodes are compatible with respect to their input + or output interface depending on the last boolean flag.] + + Description [Checks if two hnodes are compatible with respect to their input + or output interface depending on the last boolean flag. 0 for input and 1 + for output.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static boolean +_IoNodeTestCompatibilityAux( + Hrc_Manager_t *hmgr, + Hrc_Node_t *hnode1, + Hrc_Node_t *hnode2, + boolean mode) +{ + int i, n; + array_t *formalVars1, *formalVars2; + Var_Variable_t *var1, *var2; + + if (mode == 0){ + formalVars1 = Hrc_NodeReadFormalInputs(hnode1); + formalVars2 = Hrc_NodeReadFormalInputs(hnode2); + } + else { + formalVars1 = Hrc_NodeReadFormalOutputs(hnode1); + formalVars2 = Hrc_NodeReadFormalOutputs(hnode2); + } + if ((n = array_n(formalVars1)) != array_n(formalVars2)){ + error_append("Two hnodes have different number of formal "); + if (mode == 0){ + error_append("inputs.\n"); + } + else { + error_append("outputs.\n"); + } + return 0; + } + for (i=0; i < n; i++){ + var1 = array_fetch(Var_Variable_t *,formalVars1,i); + var2 = array_fetch(Var_Variable_t *,formalVars2,i); + if (strcmp(Var_VariableReadName(var1),Var_VariableReadName(var2)) != 0){ + error_append("Two hnodes have different ports, "); + error_append(Var_VariableReadName(var1)); + error_append(" and "); + error_append(Var_VariableReadName(var2)); + error_append("\n"); + return 0; + } + if (Var_VariablesTestHaveSameDomain(var1,var2) == 0){ + error_append("Two hnodes have ports defined over different domains, "); + error_append(Var_VariableReadName(var1)); + error_append(" and "); + error_append(Var_VariableReadName(var2)); + error_append("\n"); + return 0; + } + } + return 1; +} + + +/**Function******************************************************************** + + Synopsis [Canonicalizes all the tables in a given manager using + Tbl_TableCanonicalize().] + + SideEffects [The original tables will be overwritten.] + + SeeAlso [] + +******************************************************************************/ +static void +_IoManagerCanonicalize( + Hrc_Manager_t *hmgr) +{ + int i; + Hrc_Model_t *model; + Hrc_Node_t *node; + Tbl_Table_t *table; + st_generator *gen, *gen2; + char *modelName, *latchName; + Hrc_Latch_t *latch; + + Hrc_ManagerForEachModel(hmgr,gen,modelName,model){ + node = Hrc_ModelReadMasterNode(model); + Hrc_NodeForEachNameTable(node,i,table){ + Tbl_TableCanonicalize(table); + } + Hrc_NodeForEachLatch(node,gen2,latchName,latch){ + Tbl_TableCanonicalize(Hrc_LatchReadResetTable(latch)); + } + } +} + + +/**Function******************************************************************** + + Synopsis [Handle function for timeout.] + + Description [This function is called when the time out occurs. + Since alarm is set with an elapsed time, this function checks if the + CPU time corresponds to the timeout of the command. If not, it + reprograms the alarm to fire again later.] + + SideEffects [] + +******************************************************************************/ +static void +TimeOutHandle(void) +{ + int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000); + + if (seconds < mcTimeOut) { + unsigned slack = (unsigned) (mcTimeOut - seconds); + (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle); + (void) alarm(slack); + } else { + longjmp(timeOutEnv, 1); + } +} /* TimeOutHandle */ + + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int +nodenameCompare( + const void * node1, + const void * node2) +{ +Ntk_Node_t *v1, *v2; +char *name1, *name2; + + v1 = *(Ntk_Node_t **)(node1); + v2 = *(Ntk_Node_t **)(node2); + name1 = Ntk_NodeReadName(v1); + name2 = Ntk_NodeReadName(v2); + + return (strcmp(name1, name2)); +} + + +/**Function******************************************************************** + + Synopsis [This function is used for string comparison in array_sort.] + + Description [This function is used for string comparison in array_sort.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int +_HrcStringCmp( + const void * s1, + const void * s2) +{ + return(strcmp(*(char **)s1, *(char **)s2)); +} + + +/**Function******************************************************************** + + Synopsis [Prints whether model checking passed or failed] + + Description [Prints whether model checking passed or failed, and if + requested, a debug trace.] + + SideEffects [] + +******************************************************************************/ +static boolean +McPrintPassFailMine( + mdd_manager *mddMgr, + Fsm_Fsm_t *modelFsm, + Mc_FwdBwdAnalysis traversalDirection, + Ctlp_Formula_t *ctlFormula, + mdd_t *ctlFormulaStates, + mdd_t *modelInitialStates, + array_t *modelCareStatesArray, + McOptions_t *options, + Mc_VerbosityLevel verbosity) +{ + (void) fprintf(vis_stdout, "![McPrintPassFailMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![McPrintPassFailMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + if (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) { + fprintf(vis_stdout, "# MC: formula passed --- "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + fprintf(vis_stdout, "\n"); + return TRUE; + } + else { + fprintf(vis_stdout, "# MC: formula failed --- "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + fprintf(vis_stdout, "\n"); + if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { + McFsmDebugFormulaMine(options, ctlFormula,modelFsm, modelCareStatesArray); + } + return FALSE; + } +} + + +/**Function******************************************************************** + + Synopsis [Debug CTL formula in existential normal form] + + Description [Debug CTL formula in existential normal form. The extent to + which debug information is generated is a function of options settings. + + The debugger works with ctlFormula, but uses the pointers back to + the original formula that it was converted from, to give the user + more sensible feedback. To do this, it relies on a specific + translation: only EF, AU, AF, AG, and AX are converted. Hence, the + only times that the converted bit is set, we have a conversion of + one of these formulas, and the operator is either EU, or negation. + in the latter case, we can conclude from the child of the negation + what formula we converted from: EX means AX, EG means AF, EU means AG, + and OR means AU. + ] + + SideEffects [Affects vis_stdpipe] + + SeeAlso [Ctlp_FormulaConvertToExistentialForm] + +******************************************************************************/ +static int +McFsmDebugFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray) +{ + (void) fprintf(vis_stdout, "![McFsmDebugFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![McFsmDebugFormulaMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + mdd_t *modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm); + mdd_t *goodStates = Ctlp_FormulaObtainLatestApprox(ctlFormula); + mdd_t *badStates = mdd_and(modelInitialStates, goodStates, 1, 0); + mdd_t *witnessSuccState; + FILE *debugFile = McOptionsReadDebugFile(options); + FILE *oldStdOut; + FILE *oldStdErr; + extern FILE *vis_stdpipe; + char *nrOfTracesString; + int nrOfTraces; /* nr of debug traces that we output */ + int i; /* counts debug traces */ + array_t *completeCExArray; + array_t *initCExArray; + initCExArray = array_alloc(mdd_t *, 0); + + mdd_free(modelInitialStates); + + oldStdOut = vis_stdout; + oldStdErr = vis_stderr; + + nrOfTracesString = Cmd_FlagReadByName("nr_counterexamples"); + if(nrOfTracesString == NIL(char)) + nrOfTraces = 1; + else + nrOfTraces = atoi(nrOfTracesString); + + (void) fprintf(vis_stderr, "[McFsmDebugFormulaMine] Number of debug traces = %d \n", nrOfTraces); + + if (debugFile) { + vis_stdpipe = debugFile; + vis_stdout = vis_stdpipe; + (void)fprintf(vis_stdpipe, "# MC: formula failed --- "); + Ctlp_FormulaPrint(vis_stdpipe,Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void)fprintf(vis_stdpipe, "\n"); + } else if (McOptionsReadUseMore(options)){ + vis_stdpipe = popen("more", "w"); + vis_stdout = vis_stdpipe; + vis_stderr = vis_stdpipe; + } + else + vis_stdpipe = vis_stdout; + + for(i = 0; i < nrOfTraces; i++){ + (void)fprintf(vis_stdout, "# MC: Calling debugger for trace %d\n", + i+1); + witnessSuccState = McComputeACloseState(badStates, goodStates, modelFsm); + + completeCExArray = McFsmStateDebugFormulaMine(options, ctlFormula, witnessSuccState, modelFsm, + careSetArray, initCExArray); + (void) fprintf(vis_stdout, "\n![McFsmDebugFormulaMine] -> nb completeCExArray : %d \n", array_n(completeCExArray)); +// (void) fprintf(vis_stdout, "\n![McFsmDebugFormulaMine] -> nb initCExArray : %d \n", array_n(initCExArray)); + + (void) fprintf(vis_stdout, "\n![McFsmDebugFormulaMine] START xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx \n"); + boolean printInputs = McOptionsReadPrintInputs( options ); + Mc_PrintPathMine( completeCExArray, modelFsm, printInputs ); + (void) fprintf(vis_stdout, "\n![McFsmDebugFormulaMine] END xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx \n"); + + (void)fprintf(vis_stdout, "\n"); + + mdd_free(witnessSuccState); + } + mdd_free(badStates); + mdd_free(goodStates); + + if (vis_stdout != oldStdOut && vis_stdout != debugFile) + (void)pclose(vis_stdpipe); + + vis_stdout = oldStdOut; + vis_stderr = oldStdErr; + + return 1; +} + + +/**Function******************************************************************** + + Synopsis [Debug CTL formula in existential normal form at state aState] + + Description [Debug CTL formula in existential normal form at state + aState. Formula is assumed to have been CONVERTED to existential normal + form.] + + SideEffects [] + +******************************************************************************/ +static array_t * +McFsmStateDebugFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray, + array_t *prevCExArray) +{ + (void) fprintf(vis_stdout, "![McFsmStateDebugFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] MC CTL Formula : "); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 0 --> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + + + Ctlp_Formula_t *originalFormula; + array_t *cExampleArray; +// array_t *preCExArray; + array_t *fullCExArray; + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + + //prevCExArray = array_alloc(mdd_t *, 0); +// fullCExArray = prevCExArray; + if ( ctlFormula == NIL(Ctlp_Formula_t) ) { + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] * END * \n"); + fullCExArray = prevCExArray; + return fullCExArray; + } + if ( Ctlp_FormulaTestIsConverted( ctlFormula ) ) { + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> FsmStateDebugConvertedFormulaMine \n"); + cExampleArray = FsmStateDebugConvertedFormulaMine(options, ctlFormula, aState, modelFsm, + careSetArray, &prevCExArray); + + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 1 --> nb cExampleArray : %d ", array_n(cExampleArray )); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 1 --> nb prevCExArray : %d ", array_n(prevCExArray)); + +// boolean printInputs = McOptionsReadPrintInputs( options ); +// Mc_PrintPathMine( cExampleArray, modelFsm, printInputs ); + + if (array_n(prevCExArray)==0 ) { + fullCExArray = cExampleArray; + } + else { + fullCExArray = McCreateMergedPath(cExampleArray, prevCExArray); + } + + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 1 --> nb fullCExArray : %d ", array_n(fullCExArray )); + prevCExArray = fullCExArray; + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 1 --> nb prevCExArray End : %d ", array_n(prevCExArray)); + +/* (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] START OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO00000000O\n"); + boolean printInputs = McOptionsReadPrintInputs( options ); + Mc_PrintPathMine( fullCExArray, modelFsm, printInputs ); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] END 0OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO00000000O\n"); +*/ + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] * END * \n"); + return fullCExArray; + } + + originalFormula = Ctlp_FormulaReadOriginalFormula( ctlFormula ); + + switch ( Ctlp_FormulaReadType( ctlFormula ) ) { + + case Ctlp_ID_c : + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugIDMine \n"); + DebugIDMine( options, ctlFormula, aState, modelFsm ); + fullCExArray = prevCExArray; + break; + + case Ctlp_TRUE_c: + case Ctlp_FALSE_c: + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugTrueFalseMine \n"); + DebugTrueFalseMine( ctlFormula, aState, modelFsm ); + fullCExArray = prevCExArray; + break; + + case Ctlp_EQ_c: + case Ctlp_XOR_c: + case Ctlp_THEN_c: + case Ctlp_NOT_c: + case Ctlp_AND_c: + case Ctlp_OR_c: + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugBooleanMine \n"); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 2 --> nb prevCExArray : %d \n", array_n(prevCExArray)); + cExampleArray = DebugBooleanMine(options, ctlFormula, aState, modelFsm, careSetArray, &prevCExArray); + + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 2 --> nb cExampleArray : %d ", array_n(cExampleArray )); + + +/* if (array_n(prevCExArray)==0 ) { + fullCExArray = cExampleArray; + } + else { + fullCExArray = McCreateMergedPath(cExampleArray, prevCExArray); + } +*/ + + fullCExArray = cExampleArray; + prevCExArray = fullCExArray; + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 2 --> nb prevCExArray after DB : %d ", array_n(prevCExArray)); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 2 --> nb fullCExArray : %d ", array_n(fullCExArray )); + + break; + + case Ctlp_EX_c: + case Ctlp_EU_c: + case Ctlp_EG_c: + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> Ctlp_EG_c\n"); + if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) { + mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula); + mdd_t *closeState; + Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm); + array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> McStateFailsFormulaMine \n"); + + McStateFailsFormulaMine(aState, originalFormula, debugLevel, modelFsm); + if (mdd_is_tautology(passStates, 0)) { + fprintf(vis_stdout, + "--No state satisfies the formula\n"); + mdd_free(passStates); + + fullCExArray = prevCExArray; + break; + } + fprintf(vis_stdout, + "--A simple counter example does not exist since it\n"); + fprintf(vis_stdout, + " requires generating all paths from the state\n"); + fprintf(vis_stdout, + "--A state at minimum distance satisfying the formula is\n"); + closeState = McComputeACloseState(passStates, aState, modelFsm); + mdd_free(passStates); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> Mc_MintermPrintMine \n"); + Mc_MintermPrintMine(closeState, PSVars, modelNetwork); + mdd_free(closeState); + + fullCExArray = prevCExArray; + + break; + } + else { + McPath_t *witnessPath = NIL(McPath_t); + if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EX_c ) { + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugEXMine \n"); + witnessPath = DebugEXMine(ctlFormula, aState, modelFsm, careSetArray); + } + else if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) { + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugEUMine \n"); + witnessPath = DebugEUMine(ctlFormula, aState, modelFsm, careSetArray); + } + else { + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> DebugEGMine \n"); + witnessPath = DebugEGMine(ctlFormula, aState, modelFsm, careSetArray, + options); + } + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] >> FsmPathDebugFormulaMine \n"); + cExampleArray = FsmPathDebugFormulaMine(options, ctlFormula, modelFsm, witnessPath, + careSetArray, &prevCExArray); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 3 --> nb cExampleArray : %d ", array_n(cExampleArray )); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 3 --> nb prevCExArray : %d ", array_n(prevCExArray)); + +/* if (array_n(prevCExArray)==0 ) { + fullCExArray = cExampleArray; + } + else { + fullCExArray = McCreateMergedPath(cExampleArray, prevCExArray); + } +*/ + fullCExArray = prevCExArray; + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] 3 --> nb fullCExArray : %d ", array_n(fullCExArray )); + +// McPathFree( witnessPath ); //NOTE: INITIALLY FREED + } + break; + + case Ctlp_Cmp_c: + case Ctlp_Init_c: + case Ctlp_FwdU_c: + case Ctlp_FwdG_c: + case Ctlp_EY_c: + case Ctlp_EH_c: + fullCExArray = prevCExArray; + break; + + default: { + fail("Bad switch in debugging normal formula\n"); + fullCExArray = prevCExArray; + } + } +// *prevCExArray = fullCExArray; + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] LAST --> nb prevCExArray End: %d ", array_n(prevCExArray)); +/* (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] START OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO00000000O\n"); + boolean printInputs = McOptionsReadPrintInputs( options ); + Mc_PrintPathMine( prevCExArray, modelFsm, printInputs ); + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] END 0OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO00000000O\n"); +*/ + (void) fprintf(vis_stdout, "\n![McFsmStateDebugFormulaMine] * END * \n"); + return fullCExArray; + +} + +/**Function******************************************************************** + + Synopsis [Debug a converted formula] + + Comment [There are five kinds of formula that are converted: EF, AU, AF, AG, + AX. The Ctlp_Formula_t structure has a pointer back to the original formula + (where one exists). For the non-trivial cases (AU, AF, AG, AX) if the + formula is false, we create a counter example, i.e. a fair path which fails + the property. The AG, AX, AF cases are simple; the AU case is tricky because + this can be failed on two ways.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmStateDebugConvertedFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmStateDebugConvertedFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + + McPath_t *witnessPath; + McPath_t *counterExamplePath; + + array_t *cExArray; + + Ctlp_Formula_t *originalFormula =Ctlp_FormulaReadOriginalFormula(ctlFormula); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + + if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> Ctlp_EU_c \n"); + if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) { + mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula); + mdd_t *closeState; + Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm); + array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> McStateFailsFormulaMine \n"); + McStateFailsFormulaMine( aState, originalFormula, debugLevel, modelFsm ); + if (mdd_is_tautology(passStates, 0)) { + fprintf(vis_stdout, + "--No state satisfies the formula\n"); + } else { + fprintf(vis_stdout, + "\n--A simple counter example does not exist since it\n"); + fprintf(vis_stdout, + " requires generating all paths from the state\n"); + fprintf(vis_stdout, + "--A state at minimum distance satisfying the formula is\n"); + closeState = McComputeACloseState(passStates, aState, modelFsm); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> Mc_MintermPrintMine \n"); + Mc_MintermPrintMine(closeState, PSVars, modelNetwork); + mdd_free(closeState); + } + mdd_free(passStates); + } + else { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> DebugEUMine \n"); + witnessPath = DebugEUMine(ctlFormula, aState, modelFsm, careSetArray); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> FsmPathDebugEFFormulaMine\n"); + cExArray = FsmPathDebugEFFormulaMine(options, ctlFormula, modelFsm, witnessPath, + careSetArray, preCExArray); +// McPathFree( witnessPath ); + } + cExArray = *preCExArray; + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] ** END ** \n"); + return cExArray; + //return cExArray; // EF Formula not yet treated + } + + /* + * The original formula must be an AX,AF,AG, or AU formula + */ + if ( McStateSatisfiesFormula( ctlFormula, aState ) ) { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> McStatePassesFormulaMine\n"); + McStatePassesFormulaMine( aState, originalFormula, debugLevel, modelFsm ); + fprintf(vis_stdout, + "--A simple witness does not exist since it requires\n"); + fprintf(vis_stdout, " generating all paths from the state\n"); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] ** END ** \n"); + cExArray = *preCExArray; //Added to avoid seg fault + return cExArray; // maybe aState gotta checkout later!! + } + + switch ( Ctlp_FormulaReadType( lFormula ) ) { + case Ctlp_EX_c: { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> DebugEXMine\n"); + counterExamplePath = DebugEXMine(lFormula, aState, modelFsm, careSetArray); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> FsmPathDebugAXFormulaMine\n"); + cExArray = FsmPathDebugAXFormulaMine(options, ctlFormula, modelFsm, counterExamplePath, careSetArray, preCExArray); +// McPathFree( counterExamplePath ); //NOTE: INITIALLY FREED + break; + } + + case Ctlp_EG_c: { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> DebugEGMine\n"); + counterExamplePath = DebugEGMine(lFormula, aState, modelFsm, careSetArray, + options); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> FsmPathDebugAFFormulaMine\n"); + cExArray = FsmPathDebugAFFormulaMine(options, ctlFormula, modelFsm, counterExamplePath, + careSetArray, preCExArray); +// McPathFree( counterExamplePath ); //NOTE: INITIALLY FREED + break; + } + + case Ctlp_EU_c: { + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> DebugEUMine\n"); + counterExamplePath = DebugEUMine(lFormula, aState, modelFsm, careSetArray); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> FsmPathDebugAGFormulaMine\n"); + cExArray = FsmPathDebugAGFormulaMine(options, ctlFormula, modelFsm, counterExamplePath, + careSetArray, preCExArray); +// McPathFree( counterExamplePath ); //NOTE: INITIALLY FREED + break; + } + + case Ctlp_OR_c: { + /* + * need special functions bcoz of two possibilities + */ + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] >> FsmPathDebugAUFormulaMine\n"); + cExArray = FsmPathDebugAUFormulaMine(options, aState, ctlFormula, modelFsm, + careSetArray, preCExArray); + + break; + } + + default: fail("Bad formula type in handling converted operator\n"); + } + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] LAST ---> nb preCExArray : %d", array_n(*preCExArray)); + (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] LAST ---> nb cExArray : %d", array_n(cExArray )); + +// boolean printInputs = McOptionsReadPrintInputs( options ); +// (void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] printInputs = %s \n", (printInputs==TRUE)? "TRUE":"FALSE"); +// Mc_PrintPathMine(cExArray, modelFsm, printInputs ); +(void) fprintf(vis_stdout, "\n![FsmStateDebugConvertedFormulaMine] ** END ** \n"); + return cExArray; +} + + +/**Function******************************************************************** + + Synopsis [Debug a formula of the form EX, EG, EU, EF.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *witnessPath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + + array_t *witnessArray; + switch ( Ctlp_FormulaReadType( ctlFormula ) ) { + case Ctlp_EX_c: { + witnessArray = FsmPathDebugEXFormulaMine(options, ctlFormula, modelFsm, witnessPath, + careSetArray, preCExArray); + break; + } + + case Ctlp_EU_c: { + witnessArray = FsmPathDebugEUFormulaMine(options, ctlFormula, modelFsm, witnessPath, + careSetArray, preCExArray); + break; + } + + case Ctlp_EG_c: { + witnessArray = FsmPathDebugEGFormulaMine(options, ctlFormula, modelFsm, witnessPath, + careSetArray, preCExArray); + break; + } + default: { + fail("bad switch in converting converted formula\n"); + } + } + + (void) fprintf(vis_stdout, "\n![FsmPathDebugFormulaMine] ---> witnessArray : %d *END*\n", array_n(witnessArray)); + + return witnessArray; +} + + +/**Function******************************************************************** + + Synopsis [Debug an Atomic Formula] + + Description [Debug an Atomic Formula. As per the semantics of fair CTL, a + state satisfies an Atomic Formula just in case the given wire computes the + appropriate Boolean function on that state as input. The state has to be + fair; however we do NOT justify the fairness by printing a path to a fair + cycle. THe user can achieve this effect by adding ANDing in a formula EG + TRUE.] + + SideEffects [] + +******************************************************************************/ +static void +DebugIDMine( + McOptions_t *options, + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm) +{ + + (void) fprintf(vis_stdout, "![DebugIDMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![DebugIDMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, aFormula); + fprintf(vis_stdout, "\n"); + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + + if ( McStateSatisfiesFormula( aFormula, aState ) ) { + McStatePassesFormulaMine( aState, originalFormula, debugLevel, modelFsm ); + } + else { + McStateFailsFormulaMine( aState, originalFormula, debugLevel, modelFsm ); + } +} + +/**Function******************************************************************** + + Synopsis [Debug a TRUE/FALSE formula] + + SideEffects [] + +******************************************************************************/ +static void +DebugTrueFalseMine( + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm) +{ + (void) fprintf(vis_stdout, "![DebugTrueFalseMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![[DebugTrueFalseMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, aFormula); + + fprintf(vis_stdout, "\n"); + fprintf(vis_stdout, "--Nothing to debug for %s\n", + ((Ctlp_FormulaReadType(aFormula) == Ctlp_TRUE_c) ? "TRUE\n" : "FALSE\n")); +} + +/**Function******************************************************************** + + Synopsis [Debug a Boolean formula] + + Desciption [Debug a Boolean formula. For Boolean formula built out of binary + connective, we may debug only one branch, if say the formula is an AND and + the left branch is fails.] + + SideEffects [] + +******************************************************************************/ +static array_t * +DebugBooleanMine( + McOptions_t *options, + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![DebugBooleanMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![DebugBooleanMine] MC CTL Formula : "); + (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 0 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); + Ctlp_FormulaPrint(vis_stdout, aFormula); + fprintf(vis_stdout, "\n"); + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( aFormula ); + Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( aFormula ); + McDbgLevel debugLevel = McOptionsReadDbgLevel(options); + + if (McStateSatisfiesFormula(aFormula, aState)) { + McStatePassesFormulaMine(aState, originalFormula, debugLevel, modelFsm); + } else { + McStateFailsFormulaMine(aState, originalFormula, debugLevel, modelFsm); + } + + /* We always debug the first (left) child. */ + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + cExArray = McFsmStateDebugFormulaMine(options, lFormula, aState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 1 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 1 ---> nb cExArray : %d \n", array_n(cExArray)); + /* What we do for the second child depends on the type of the formula. + * For Ctlp_AND_c, Ctlp_OR_c, Ctlp_THEN_c the right child may not be + * needed. With early termination, the right child may not have the + * information required to produce a counterexample; hence, its debugging + * is not optional. (We may get incorrect answers.) + */ + if (Ctlp_FormulaReadType(aFormula) == Ctlp_AND_c) { + /* If aFormula fails and aState does not satisfy lFormula + * 1. The information about aState at the right child is not + * necessarilty correct. (aState was a don't care state.) + * 2. A counterexample to lFormula is a counterexample to + * aFormula. + * So, if aFormula fails, we should debug the right child only if + * aState satisfies lFormula. + * If, on the other hand, aFormula passes, then aState must satisfy + * lFormula, and we need to witness both lFormula and rFormula. + */ + if (McStateSatisfiesFormula(lFormula, aState)) { + cExArray = McFsmStateDebugFormulaMine(options, rFormula, aState, modelFsm, + careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 2 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 2 ---> nb cExArray : %d \n", array_n(cExArray)); + } + } else if (Ctlp_FormulaReadType(aFormula) == Ctlp_OR_c) { + /* if aFormula passes, we should debug the right child only if + * aState does not satisfy lFormula. + * If, on the other hand, aFormula fails, then aState may not satisfy + * lFormula, and we need to produce counterexamples for both lFormula + * and rFormula. + */ + if (!McStateSatisfiesFormula(lFormula, aState)) { + cExArray = McFsmStateDebugFormulaMine(options, rFormula, aState, modelFsm, + careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 3 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 3 ---> nb cExArray : %d \n", array_n(cExArray)); + } + } else if (Ctlp_FormulaReadType(aFormula) == Ctlp_THEN_c) { + /* This case is like the OR, with the polarity of the left + * left child reversed. + */ + if (McStateSatisfiesFormula(lFormula, aState)) { + cExArray = McFsmStateDebugFormulaMine(options, rFormula, aState, modelFsm, + careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 4 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 4 ---> nb cExArray : %d \n", array_n(cExArray)); + } + } else if (Ctlp_FormulaReadType(aFormula) != Ctlp_NOT_c) { + /* For Ctlp_EQ_c and Ctlp_XOR_c both children must be debugged. */ + cExArray = McFsmStateDebugFormulaMine(options, rFormula, aState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 5 ---> nb prevCExArray : %d \n", array_n(*preCExArray)); +// (void) fprintf(vis_stdout, "\n![DebugBooleanMine] 5 ---> nb cExArray : %d \n", array_n(cExArray)); + } + (void) fprintf(vis_stdout, "\n![DebugBooleanMine] LAST ---> nb prevCExArray : %d ", array_n(*preCExArray)); + (void) fprintf(vis_stdout, "\n![DebugBooleanMine] LAST ---> nb cExArray : %d *END*\n", array_n(cExArray)); + return cExArray; +} + + +/**Function******************************************************************** + + Synopsis [Debug a formula of type EX.] + + Description [Debug a formula of type EX at specified state. It is assumed + that aState satisfies the EX formula.] + + SideEffects [] + +******************************************************************************/ +static McPath_t * +DebugEXMine( + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray) +{ + (void) fprintf(vis_stdout, "![DebugEXMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![DebugEXMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, aFormula); + fprintf(vis_stdout, "\n"); + + mdd_t *aDupState = mdd_dup( aState ); + mdd_t *aStateSuccs; + mdd_t *statesSatisfyingLeftFormula; + mdd_t *targetStates; + mdd_t *witnessSuccState; + Ctlp_Formula_t *lFormula; + McPath_t *witnessPath = McPathAlloc(); + array_t *stemArray = array_alloc( mdd_t *, 0 ); + Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); + + /* + * By using careSet here, can end up with unreachable successors + */ + aStateSuccs = Img_ImageInfoComputeImageWithDomainVars(imageInfo, + aState, aState, careSetArray); + + lFormula = Ctlp_FormulaReadLeftChild( aFormula ); + statesSatisfyingLeftFormula = Ctlp_FormulaObtainLatestApprox( lFormula ); + + targetStates = mdd_and( aStateSuccs, statesSatisfyingLeftFormula, 1, 1 ); + mdd_free( aStateSuccs ); mdd_free( statesSatisfyingLeftFormula ); + + witnessSuccState = Mc_ComputeACloseState( targetStates, aState, modelFsm ); + mdd_free( targetStates ); + + array_insert_last( mdd_t *, stemArray, aDupState ); + array_insert_last( mdd_t *, stemArray, witnessSuccState ); + + McPathSetStemArray( witnessPath, stemArray ); + + return witnessPath; +} + +/**Function******************************************************************** + + Synopsis [Debug a formula of type EU.] + + Description [Debug a formula of type EU at specified state. It is assumed that + state fails formula.] + + SideEffects [] + +******************************************************************************/ +static McPath_t * +DebugEUMine( + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray) +{ + (void) fprintf(vis_stdout, "![DebugEUMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![DebugEUMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, aFormula); + fprintf(vis_stdout, "\n"); + + McPath_t *witnessPath = McPathAlloc(); + array_t *OnionRings = (array_t *) Ctlp_FormulaReadDebugData( aFormula ); + array_t *pathToCore = Mc_BuildPathToCore(aState, OnionRings, + modelFsm, + McGreaterOrEqualZero_c ); + + McPathSetStemArray( witnessPath, pathToCore ); + + return witnessPath; +} + +/**Function******************************************************************** + + Synopsis [Debug a formula of type EG.] + + Description [Debug a formula of type EG at specified state. It is assumed + that state fails formula. Refer to Clarke et al DAC 1995 for details of the + algorithm.] + + SideEffects [] + +******************************************************************************/ +static McPath_t * +DebugEGMine( + Ctlp_Formula_t *aFormula, + mdd_t *aState, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray, + McOptions_t *options) +{ + (void) fprintf(vis_stdout, "![DebugEGMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(aFormula)); + (void) fprintf(vis_stdout, "\n![DebugEGMine] MC CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, aFormula); + fprintf(vis_stdout, "\n"); + + array_t *arrayOfOnionRings = (array_t *) Ctlp_FormulaReadDebugData(aFormula); + mdd_t *invariantMdd = Ctlp_FormulaObtainLatestApprox( aFormula ); + McPath_t *fairPath = McBuildFairPath(aState, invariantMdd, arrayOfOnionRings, + modelFsm, careSetArray, + McOptionsReadVerbosityLevel(options), + McOptionsReadDcLevel(options), + McOptionsReadFwdBwd(options)); + mdd_free( invariantMdd ); + + return fairPath; +} + + +/**Function******************************************************************** + + Synopsis [Debug a path for EX type formula.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugEXFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *witnessPath, + array_t *careSetArray, + array_t **preCExArray) +{ + + (void) fprintf(vis_stdout, "![FsmPathDebugEXFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugEXFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEXFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *witnessArray = McPathReadStemArray( witnessPath ); + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + Ctlp_Formula_t *lChild = Ctlp_FormulaReadLeftChild( ctlFormula ); + char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula ); + boolean printInputs = McOptionsReadPrintInputs( options ); + mdd_t *secondlastState; + if(array_n(witnessArray)<2) + { + fprintf(vis_stdout,"witnessArray has less than two elements, return\n"); + if (array_n(witnessArray) > 0) return witnessArray; + else return NIL(array_t); + } + secondlastState= array_fetch( mdd_t *, witnessArray, (array_n(witnessArray)-1) ); + + (void) fprintf(vis_stderr, "-[FsmPathDebugEXFormulaMine] array_n(witnessArrayEX) = %d\n",array_n(witnessArray)); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%spasses EX formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName, + ctlFormulaText ); + + FREE(firstStateName); + FREE(ctlFormulaText); + + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + switch ( McOptionsReadDbgLevel( options ) ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: + case McDbgLevelMax_c: + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); +// cExArray = McFsmStateDebugFormulaMine(options, lChild, secondlastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lChild, secondlastState, modelFsm, careSetArray, *preCExArray); + break; + case McDbgLevelInteractive_c: + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + if (McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n")) +// cExArray = McFsmStateDebugFormulaMine(options, lChild, secondlastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lChild, secondlastState, modelFsm, careSetArray, *preCExArray); + break; + default: + fail("Reached bad switch in FsmPathDebugEXFormulaMine\n"); + } +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEXFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + return witnessArray; +} + + +/**Function******************************************************************** + + Synopsis [Debug a path for EU type formula.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugEUFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *witnessPath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugEUFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugEUFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEUFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula ); + char *lFormulaText = Ctlp_FormulaConvertToString( lFormula ); + char *rFormulaText = Ctlp_FormulaConvertToString( rFormula ); + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *witnessArray = McPathReadStemArray( witnessPath ); + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray )); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%spasses EU formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName, + ctlFormulaText ); + + if ( array_n(witnessArray ) == 1 ) { + (void) fprintf(vis_stderr, "-[FsmPathDebugEUFormulaMine] *VERIFICATION REQUIRED!* CEx n_state = %d \n", array_n(witnessArray)); + Mc_PrintPath(witnessArray, modelFsm, printInputs); // added + } + + (void) fprintf(vis_stderr, "-[FsmPathDebugEUFormulaMine] array_n(witnessArrayEU) = %d\n",array_n(witnessArray)); + + FREE(firstStateName); + FREE(ctlFormulaText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: + if ( array_n(witnessArray ) == 1 ) { + if( debugLevel != McDbgLevelMin_c ) + fprintf(vis_stdout, "since %s is true at this state", rFormulaText); +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else { + if( debugLevel != McDbgLevelMin_c ) + fprintf(vis_stdout, "--Path on which %s is true till %s is true\n", + lFormulaText, rFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath(witnessArray, modelFsm, printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + break; + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: + if ( array_n(witnessArray ) == 1 ) { + fprintf(vis_stdout, "since %s is true at this state", rFormulaText); +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else { + int i; + fprintf(vis_stdout, "--Path on which %s is true till %s is true\n", + lFormulaText, rFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath(witnessArray,modelFsm,printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); + for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) { + mdd_t *aState = array_fetch( mdd_t *, witnessArray, i ); + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "Continue debugging EU formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, lFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lFormula, aState, modelFsm, careSetArray, *preCExArray); + } + } +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + break; + default: + fail("Should not be here - bad switch in debugging EU formula\n"); + } + + FREE(lFormulaText); + FREE(rFormulaText); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEUFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + return witnessArray; +} + +/**Function******************************************************************** + + Synopsis [Debug a path for EG type formula.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugEGFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *witnessPath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugEGFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugEGFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEGFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + mdd_t *firstState; + char *firstStateName; + array_t *witnessArray; + array_t *witness; + char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula ); + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *stemArray = McPathReadStemArray( witnessPath ); + array_t *cycleArray = McPathReadCycleArray( witnessPath ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + char *lFormulaText = Ctlp_FormulaConvertToString( lFormula ); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + witnessArray = McCreateMergedPath( stemArray, cycleArray ); + firstState = array_fetch( mdd_t *, witnessArray, 0 ); + firstStateName = Mc_MintermToString(firstState, PSVars,Fsm_FsmReadNetwork(modelFsm)); + + + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(stemArrayEG) = %d\n",array_n(stemArray)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(cycleArrayEG) = %d\n",array_n(cycleArray)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(witnessArrayEG) = %d\n",array_n(witnessArray)); + + + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%spasses EG formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName, + ctlFormulaText ); + + FREE(firstStateName); + FREE(ctlFormulaText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: { + McPath_t *normalPath = McPathNormalize( witnessPath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(stemNormEG) = %d\n",array_n(stem)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(cycleNormEG) = %d\n",array_n(cycle)); + witness = McCreateMergedPath( stem, cycle ); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(witnessNormEG) = %d\n",array_n(witness)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + Mc_PrintPath( witness, modelFsm, printInputs ); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + + if(debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n", + lFormulaText); + + FREE( lFormulaText ); + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, "\n"); + fprintf(vis_stdout, " --Counter example ends\n\n"); + McPathFree( normalPath ); + break; + } + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: { + McPath_t *normalPath = McPathNormalize( witnessPath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + int i; + + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(stemNormEG) = %d\n",array_n(stem)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(cycleNormEG) = %d\n",array_n(cycle)); + witness = McCreateMergedPath( stem, cycle ); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] array_n(witnessNormEG) = %d\n",array_n(witness)); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + Mc_PrintPath( witness, modelFsm, printInputs ); + (void) fprintf(vis_stderr, "-[FsmPathDebugEGFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + + fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n", + lFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) { + mdd_t *aState = array_fetch( mdd_t *, witnessArray, i ); + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "--Continue debugging EG formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, lFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lFormula, aState, modelFsm, careSetArray, *preCExArray); + } + } + break; + } + default: + fail("Bad switch in FsmPathDebugEGFormulaMine\n"); + witness = NIL(array_t); + } + + McNormalizeBddPointer(witnessArray); + mdd_array_free( witnessArray ); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEGFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + return witness; +} + +/**Function******************************************************************** + + Synopsis [Debug a EF formula] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugEFFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *witnessPath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugEFFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugEFFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEFFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); + char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula ); + + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *witnessArray = McPathReadStemArray( witnessPath ); + + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray ); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + + Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula ); + Ctlp_Formula_t *rOriginalFormula = Ctlp_FormulaReadOriginalFormula(rFormula); + char *rOriginalFormulaText = Ctlp_FormulaConvertToString( rOriginalFormula ); + char *rFormulaText = Ctlp_FormulaConvertToString( rFormula ); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%spasses EF formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName, + originalFormulaText ); + +// Added in case if there's no counter example => CTL fails at initial state +// (void) fprintf(vis_stderr, "-[FsmPathDebugAGFormulaMine] 1) CEx n_state = %d \n", array_n(witnessArray)); + if ( array_n(witnessArray ) == 1 ) { + (void) fprintf(vis_stderr, "-[FsmPathDebugEFFormulaMine] *VERIFICATION REQUIRED!* CEx n_state = %d \n", array_n(witnessArray)); + Mc_PrintPath(witnessArray, modelFsm, printInputs); // added + } + (void) fprintf(vis_stderr, "-[FsmPathDebugEFFormulaMine] array_n(witnessArrayEF) = %d\n",array_n(witnessArray)); + + FREE(firstStateName); + FREE(originalFormulaText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: + if ( array_n(witnessArray ) == 1 ) { + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, "since %s is true at this state\n", + rOriginalFormulaText); + + FREE( rOriginalFormulaText ); +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else { + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, + "--Witness is a path to a state where %s is finally true\n", + rOriginalFormulaText); + (void) fprintf( vis_stdout, "\n--Fair path stem:\n"); + FREE( rOriginalFormulaText ); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + } + break; + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: + if ( array_n(witnessArray ) == 1 ) { +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else + { + fprintf(vis_stdout, + "--Witness is a path to a state where %s is finally true\n", + rOriginalFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "--Continue debugging EF formula? (1-yes,0-no)\n"))) + { +// cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, rFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + } + break; + default: + fail("bad switch in debugging EF\n"); + } +// (void) fprintf(vis_stdout, "\n![FsmPathDebugEFFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + FREE(rFormulaText); + return witnessArray; +} + + +/**Function******************************************************************** + + Synopsis [Debug a AX formula] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugAXFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *counterExamplePath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugAXFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAXFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAXFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); + char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula ); + Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula ); + + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *witnessArray = McPathReadStemArray( counterExamplePath ); + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + mdd_t *lastState = array_fetch( mdd_t *, witnessArray, 1 ); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + boolean printInputs = McOptionsReadPrintInputs( options ); + + (void) fprintf(vis_stderr, "-[FsmPathDebugAXFormulaMine] array_n(witnessArrayAX) = %d\n",array_n(witnessArray)); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%sfails AX formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName, + originalFormulaText ); + + FREE(firstStateName); + FREE(originalFormulaText); + + switch ( McOptionsReadDbgLevel( options ) ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: + case McDbgLevelMax_c: + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + fprintf(vis_stdout, "\n"); +// cExArray = McFsmStateDebugFormulaMine(options, lllFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lllFormula, lastState, modelFsm, careSetArray, *preCExArray); + break; + case McDbgLevelInteractive_c: + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + if ( McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n") ) { +// cExArray = McFsmStateDebugFormulaMine(options, lllFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lllFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + break; + default: + fail("Bad switch in FsmPathDebugAXFormulaMine\n"); + } + +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAXFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + return witnessArray; +} + +/**Function******************************************************************** + + Synopsis [Debug a AF formula] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugAFFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *counterExamplePath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugAFFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAFFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAFFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); + char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula ); + Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula ); + Ctlp_Formula_t *lllOriginalFormula = Ctlp_FormulaReadOriginalFormula( + lllFormula); + char *lllOriginalFormulaText = Ctlp_FormulaConvertToString( + lllOriginalFormula); + + mdd_t *firstState; + array_t *witnessArray; + array_t *witness; + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *stemArray = McPathReadStemArray( counterExamplePath ); + array_t *cycleArray = McPathReadCycleArray( counterExamplePath ); + char *firstStateName; + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + witnessArray = McCreateMergedPath( stemArray, cycleArray ); + firstState = array_fetch( mdd_t *, witnessArray, 0 ); + firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(stemArrayEG) = %d\n",array_n(stemArray)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(cycleArrayEG) = %d\n",array_n(cycleArray)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(witnessArrayEG) = %d\n",array_n(witnessArray)); + + + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%sfails AF formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName, + originalFormulaText ); + FREE(firstStateName); + FREE(originalFormulaText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c: { + McPath_t *normalPath = McPathNormalize( counterExamplePath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(stemNormEG) = %d\n",array_n(stem)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(cycleNormEG) = %d\n",array_n(cycle)); + witness = McCreateMergedPath( stem, cycle ); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(witnessNormEG) = %d\n",array_n(witness)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + Mc_PrintPath( witness, modelFsm, printInputs ); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, "--A fair path on which %s is always false:\n", + lllOriginalFormulaText ); + + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, "\n"); + fprintf(vis_stdout, " --Counter example ends\n\n"); + McPathFree( normalPath ); + break; + } + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: { + int i; + McPath_t *normalPath = McPathNormalize( counterExamplePath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(stemNormEG) = %d\n",array_n(stem)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(cycleNormEG) = %d\n",array_n(cycle)); + witness = McCreateMergedPath( stem, cycle ); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] array_n(witnessNormEG) = %d\n",array_n(witness)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + Mc_PrintPath( witness, modelFsm, printInputs ); + (void) fprintf(vis_stderr, "-[FsmPathDebugAFFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + + + fprintf(vis_stdout, "--A fair path on which %s is always false:\n", + lllOriginalFormulaText ); + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, "\n"); + fprintf(vis_stdout, " --Counter example ends\n\n"); + McPathFree( normalPath ); + for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) { + mdd_t *aState = array_fetch( mdd_t *, witnessArray, i ); + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "--Continue debugging AF formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, lllFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lllFormula, aState, modelFsm, careSetArray, *preCExArray); + } + } + + break; + } + default: { + fail("Bad case in switch for debugging AF formula\n"); + witness = NIL(array_t); + } + } + +// array_free(prevCExArray); + McNormalizeBddPointer(witnessArray); + mdd_array_free( witnessArray ); + FREE(lllOriginalFormulaText); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAFFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); + return witness; +} + +/**Function******************************************************************** + + Synopsis [Debug an AG formula.] + + Description [Debugs an AG formula. What it really wants is a formula of the + form !EF! phi, that was converted from the formula AG phi, with all the + converted pointers set as required: the top ! points to the original AG + formula, and top node of phi points to the original phi.] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugAGFormulaMine( + McOptions_t *options, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + McPath_t *counterExamplePath, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugAGFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAGFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAGFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); + char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula ); + Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula ); + Ctlp_Formula_t *lrlOriginalFormula = Ctlp_FormulaReadOriginalFormula( + lrlFormula); + char *lrlOriginalFormulaText = Ctlp_FormulaConvertToString( + lrlOriginalFormula); + + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *witnessArray = McPathReadStemArray( counterExamplePath ); + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray )); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + +// CEXStruct CEXPath [array_n( aPath )]; +// *Mc_MintermToStringMine( mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork, CEXStruct *CEXPath, int seqNumber, boolean inOutIndicator, BmcCnfClauses_t *cnfClauses); + (void) fprintf(vis_stderr, "-[FsmPathDebugAGFormulaMine] array_n(witnessArrayAG) = %d\n",array_n(witnessArray)); + + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + assert( Ctlp_FormulaReadType(ctlFormula) == Ctlp_NOT_c ); + assert( Ctlp_FormulaTestIsConverted(ctlFormula) ); + assert( Ctlp_FormulaReadType(originalFormula) == Ctlp_AG_c ); + assert( originalFormulaText != NIL(char) ); + assert( Ctlp_FormulaReadType(lFormula) == Ctlp_EU_c ); + assert( Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(lFormula)) == + Ctlp_TRUE_c ); + assert( Ctlp_FormulaReadType(lrFormula) == Ctlp_NOT_c ); + assert( lrlOriginalFormula != NIL(Ctlp_Formula_t) ); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%sfails AG formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName, + originalFormulaText ); + +// Added in case if there's no counter example => CTL fails at initial state +// (void) fprintf(vis_stderr, "-[FsmPathDebugAGFormulaMine] 1) CEx n_state = %d \n", array_n(witnessArray)); + if ( array_n(witnessArray ) == 1 ) { +// (void) fprintf(vis_stderr, "-[FsmPathDebugAGFormulaMine] 2) CEx n_state = %d \n", array_n(witnessArray)); + Mc_PrintPath(witnessArray, modelFsm, printInputs); // added + } + FREE(firstStateName); + FREE(originalFormulaText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c:{ + if ( array_n(witnessArray ) == 1 ) { + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, "since %s is false at this state\n", + lrlOriginalFormulaText ); +// cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else { + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, + "--Counter example is a path to a state where %s is false\n", + lrlOriginalFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath(witnessArray, modelFsm, printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); +// cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + break; + } + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: { + if ( array_n(witnessArray ) == 1 ) { + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, "since %s is false at this state\n", + lrlOriginalFormulaText ); +// cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + else { + fprintf(vis_stdout, + "--Counter example is a path to a state where %s is false\n", + lrlOriginalFormulaText); + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath( witnessArray, modelFsm, printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "--Continue debugging AG formula? (1-yes,0-no)\n"))) + { +// cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lrlFormula, lastState, modelFsm, careSetArray, *preCExArray); + } + } + break; + } + default: { + fail("bad switch in debugging AG\n"); + } + } +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAGFormulaMine] ---> nb prevCExArray : %d *END*\n", array_n(prevCExArray)); +// array_free(prevCExArray); + FREE(lrlOriginalFormulaText); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAGFormulaMine] *** Mc_PrintPathMine STARTS ----------------------\n"); +// Mc_PrintPathMine(witnessArray, modelFsm, printInputs); +// (void) fprintf(vis_stdout, "![FsmPathDebugAGFormulaMine] Mc_PrintPathMine ENDS *** -------------------------\n"); + return witnessArray; +} + +/**Function******************************************************************** + + Synopsis [Debug a AU formula] + + SideEffects [] + +******************************************************************************/ +static array_t * +FsmPathDebugAUFormulaMine( + McOptions_t *options, + mdd_t *aState, + Ctlp_Formula_t *ctlFormula, + Fsm_Fsm_t *modelFsm, + array_t *careSetArray, + array_t **preCExArray) +{ + (void) fprintf(vis_stdout, "![FsmPathDebugAUFormulaMine] Original CTL Formula : "); + Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] MC CTL Formula : "); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] 0 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + Ctlp_FormulaPrint(vis_stdout, ctlFormula); + fprintf(vis_stdout, "\n"); + array_t *cExArray; +// array_t *prevCExArray; +// prevCExArray = array_alloc(mdd_t *, 0); //Note: added just to respect arg requirements but not used + + Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); + char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula ); + Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula ); + Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula ); + Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula ); + Ctlp_Formula_t *lrllFormula = Ctlp_FormulaReadLeftChild( lrlFormula ); + Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula ); + Ctlp_Formula_t *llrFormula = Ctlp_FormulaReadRightChild( llFormula ); + Ctlp_Formula_t *llrlFormula = Ctlp_FormulaReadLeftChild( llrFormula ); + Ctlp_Formula_t *llrllFormula = Ctlp_FormulaReadLeftChild( llrlFormula ); + Ctlp_Formula_t *fFormula = llrllFormula; + Ctlp_Formula_t *gFormula = lrllFormula; + Ctlp_Formula_t *fOriginalFormula = Ctlp_FormulaReadOriginalFormula(fFormula); + Ctlp_Formula_t *gOriginalFormula = Ctlp_FormulaReadOriginalFormula(gFormula); + char *fText = Ctlp_FormulaConvertToString( fOriginalFormula ); + char *gText = Ctlp_FormulaConvertToString( gOriginalFormula ); + + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + char *firstStateName = Mc_MintermToString(aState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + McDbgLevel debugLevel = McOptionsReadDbgLevel( options ); + boolean printInputs = McOptionsReadPrintInputs( options ); + + if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c) + fprintf(vis_stdout, "--State\n%sfails AU formula\n\n", + firstStateName); + else + fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName, + originalFormulaText ); + FREE(firstStateName); + FREE(originalFormulaText); + + /* orginal formula is A(fUg) => converted is !((E[!g U (!f*!g)]) + (EG!g)) */ + + if ( McStateSatisfiesFormula( llFormula, aState ) ) { + /* + * the case E[!g U (!f*!g)] is true + */ + McPath_t *counterExamplePath = DebugEUMine(llFormula, aState, modelFsm, + careSetArray); + + array_t *stemArray = McPathReadStemArray( counterExamplePath ); + array_t *witnessArray = stemArray; + mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 ); + mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray ); + char *firstStateName = Mc_MintermToString(firstState, PSVars, + Fsm_FsmReadNetwork(modelFsm)); + +// Added in case if there's no counter example => CTL fails at initial state +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] 1) CEx n_state = %d \n", array_n(witnessArray)); + if ( array_n(witnessArray ) == 1 ) { + (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] *VERIFICATION REQUIRED!* CEx n_state = %d \n", array_n(witnessArray)); + Mc_PrintPath(witnessArray, modelFsm, printInputs); // added + } + (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(witnessArrayEU) = %d\n",array_n(witnessArray)); + + switch ( debugLevel ) { + case McDbgLevelMinVerbose_c: + fprintf(vis_stdout, + "--Counter example is a fair path where %s is false until %s is also false\n", + gText, fText); + case McDbgLevelMin_c: + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath(witnessArray, modelFsm, printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); +// cExArray = McFsmStateDebugFormulaMine(options, llrFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, llrFormula, lastState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] 1 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + break; + + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: { + if ( array_n(witnessArray ) == 1 ) { + fprintf(vis_stdout, + "--At state %s\nformula %s is false and\nformula %s is also false\n", + firstStateName, fText, gText); + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "Continue debugging AU formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, fFormula, aState, modelFsm, careSetArray, prevCExArray); +// cExArray = McFsmStateDebugFormulaMine(options, gFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, fFormula, aState, modelFsm, careSetArray, *preCExArray); + cExArray = McFsmStateDebugFormulaMine(options, gFormula, aState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] 2 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + } + } + else { + int i; + fprintf(vis_stdout, " --Counter example begins\n"); + Mc_PrintPath(witnessArray,modelFsm,printInputs); + fprintf(vis_stdout, " --Counter example ends\n\n"); + for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) { + mdd_t *aState = array_fetch( mdd_t *, witnessArray, i ); + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "Continue debugging AU formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, gFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, llrFormula, lastState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] 3 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + } + } + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "Continue debugging AU formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, fFormula, lastState, modelFsm, careSetArray, prevCExArray); +// cExArray = McFsmStateDebugFormulaMine(options, gFormula, lastState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, fFormula, lastState, modelFsm, careSetArray, *preCExArray); + cExArray = McFsmStateDebugFormulaMine(options, gFormula, lastState, modelFsm, careSetArray, *preCExArray); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] 4 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + } + } + break; + } + + default: { + fail("Unknown case in debugging AU\n"); + } + }/* case */ +// McPathFree( counterExamplePath ); NOTE: INITIALLY FREED + +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + +// array_free(prevCExArray); + FREE( fText ); + FREE( gText ); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] *** Mc_PrintPathMine WA STARTS ------------------\n"); +// Mc_PrintPathMine(witnessArray, modelFsm, printInputs); +// (void) fprintf(vis_stdout, "![FsmPathDebugAUFormulaMine] Mc_PrintPathMine WA ENDS *** -------------------\n"); + + *preCExArray = cExArray; +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] LAST ---> nb cExArray : %d \n", array_n(cExArray)); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] LAST ---> nb preCExArray : %d \n", array_n(*preCExArray)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] ---> nb witnessArray : %d *END*\n", array_n(witnessArray)); + return witnessArray; + } + else { + /* + * must be the case that EG!g + */ + McPath_t *counterExamplePath = DebugEGMine(lrFormula, aState, modelFsm, + careSetArray, + options); + + assert( McStateSatisfiesFormula( lrFormula, aState ) ); + + array_t *stemArray = McPathReadStemArray( counterExamplePath ); + array_t *cycleArray = McPathReadCycleArray( counterExamplePath ); + array_t *witnessArray = McCreateMergedPath( stemArray, cycleArray ); + McPath_t *normalPath = McPathNormalize( counterExamplePath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(stemArrayEG) = %d\n",array_n(stemArray)); +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(cycleArrayEG) = %d\n",array_n(cycleArray)); +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(witnessArrayEG) = %d\n",array_n(witnessArray)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(stemNormEG) = %d\n",array_n(stem)); + (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(cycleNormEG) = %d\n",array_n(cycle)); + array_t *witness = McCreateMergedPath( stem, cycle ); + (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] array_n(witnessNormEG) = %d\n",array_n(witness)); +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); +// Mc_PrintPathMine( witness, modelFsm, printInputs ); +// (void) fprintf(vis_stderr, "-[FsmPathDebugAUFormulaMine] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n"); + + + + if( debugLevel != McDbgLevelMin_c) + fprintf(vis_stdout, + "--Counter example is a fair path where %s is always false\n", + gText); + + switch ( debugLevel ) { + case McDbgLevelMin_c: + case McDbgLevelMinVerbose_c:{ +/* McPath_t *normalPath = McPathNormalize( counterExamplePath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); +*/ + + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + McPathFree( normalPath ); + + break; + } + + case McDbgLevelMax_c: + case McDbgLevelInteractive_c: + { + int i; +/* array_t *stemArray = McPathReadStemArray( counterExamplePath ); + array_t *cycleArray = McPathReadCycleArray( counterExamplePath ); + array_t *witnessArray = McCreateMergedPath( stemArray, cycleArray ); + McPath_t *normalPath = McPathNormalize( counterExamplePath ); + array_t *stem = McPathReadStemArray( normalPath ); + array_t *cycle = McPathReadCycleArray( normalPath ); + */ + fprintf(vis_stdout, " --Counter example begins\n"); + (void) fprintf( vis_stdout, "--Fair path stem:\n"); + Mc_PrintPath( stem, modelFsm, printInputs ); + + (void) fprintf( vis_stdout, "--Fair path cycle:\n"); + Mc_PrintPath( cycle, modelFsm, printInputs ); + fprintf(vis_stdout, " --Counter example ends\n\n"); + McPathFree( normalPath ); + for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) { + mdd_t *aState = array_fetch( mdd_t *, witnessArray, i ); + + if (debugLevel == McDbgLevelMax_c || + (debugLevel == McDbgLevelInteractive_c && + McQueryContinue( + "--Continue debugging AU formula? (1-yes,0-no)\n"))) { +// cExArray = McFsmStateDebugFormulaMine(options, lrllFormula, aState, modelFsm, careSetArray, prevCExArray); + cExArray = McFsmStateDebugFormulaMine(options, lrllFormula, aState, modelFsm, careSetArray, *preCExArray); + *preCExArray = cExArray; +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] EG 1 ---> nb preCExArray : %d \n", array_n(*preCExArray)); + } + } + break; + } + + default: { + fail("Bad switch in debugging AU formula\n"); + } + }/* case */ + +// McPathFree( counterExamplePath ); NOTE: INITIALLY FREED +// array_free(prevCExArray); + FREE( fText ); + FREE( gText ); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] ---> nb prevCExArray : %d \n", array_n(prevCExArray)); + +// *preCExArray = cExArray; // preCExArray = &cExArray; + +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] LAST ---> nb cExArray : %d \n", array_n(cExArray)); +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] LAST ---> nb preCExArray : %d \n", array_n(*preCExArray)); + (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] ---> nb witness : %d *END*\n", array_n(witness)); + +// (void) fprintf(vis_stdout, "\n![FsmPathDebugAUFormulaMine] *** Mc_PrintPathMine STARTS ------------------ \n"); +// Mc_PrintPathMine(witness, modelFsm, printInputs); +// (void) fprintf(vis_stdout, "![FsmPathDebugAUFormulaMine] Mc_PrintPathMine ENDS *** --------------------- \n"); + return witness; + } + +} + + + +/**Function******************************************************************** + + Synopsis [Utility function - prints states on path, inputs for transitions] + + SideEffects [] + +******************************************************************************/ +static int +Mc_PrintPathMine( + array_t *aPath, + Fsm_Fsm_t *modelFsm, + boolean printInput) +{ + (void) fprintf(vis_stderr, "![Mc_PrintPathMine] \n"); + int check, forced, i; + int numForced; + mdd_t *inputSet=NIL(mdd_t); + mdd_t *uInput = NIL(mdd_t); + mdd_t *vInput = NIL(mdd_t); + + array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm ); + array_t *inputVars = Fsm_FsmReadInputVars( modelFsm ); + mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); + + forced = 0; + check = 1; + numForced = 0; + + + (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] NUMBER OF STEPS IN THE COUNTER EXAMPLE PATH = %d \n", array_n( aPath )); + + CEXStruct CEXPath [array_n( aPath )]; + //CEXStruct *testCEX; + //testCEX = (CEXStruct *)malloc(sizeof(CEXStruct)*array_n( aPath )); + + // --- SAT Solver File Generation --- + BmcOption_t *options = BmcOptionAlloc(); + int steps = (array_n( aPath ) - 1); // taille du contre exemple +// SATSolverFileGen (&hmgr, CNF_FILE, steps, options); + BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t); + cnfClauses = BmcCnfClausesAlloc(); + Ntk_Network_t * ntk = Ntk_HrcManagerReadCurrentNetwork(hmgrGlobalC); + build_unroll_circuit(ntk,steps,options,cnfClauses); + (void) fprintf(vis_stderr, "*** CNF clauses for current network generated. *** \n\n"); + + (void) fprintf(vis_stderr, "*** Generating CNF clauses for Counter Example... *** \n\n"); + + for( i = -1 ; i < (array_n( aPath )-1); i++ ) { + + CEXPath[i+1].pathIndex = i+1; + CEXPath[i+1].n_outputVar = array_n( psVars ); + + (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] CEX PATH INDEX: CEXPath[%d].pathIndex = %d \n", i+1, CEXPath[i+1].pathIndex); + (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] NUMBER OF OUTPUTS: CEXPath[%d].n_outputVar = %d \n", i+1, CEXPath[i+1].n_outputVar); + + //deviceInfo = (deviceStruct *)malloc(sizeof(deviceStruct)*diagInfo.n_failures); + CEXPath[i+1].outputVar = (CEXVarStruct *)malloc(sizeof(CEXVarStruct)*CEXPath[i+1].n_outputVar); + //deviceInfo[i].dData = (dataStruct *)malloc(sizeof(dataStruct)*(deviceInfo[i].nb_d_data)); + + mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i ); + mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) ); + +// (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] aState = %ld \n", aState); +// (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] bState = %ld \n", bState); + + Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm); + + char *aStateString = aState ? Mc_MintermToString( aState, psVars, modelNetwork ) : NIL(char); + char *bStateString = Mc_MintermToStringMine( bState, psVars, modelNetwork, CEXPath, (i+1), FALSE, cnfClauses); +// (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] aState = %s \n", aStateString); +// (void) fprintf(vis_stderr, " --- [Mc_PrintPathMine] bState = %s \n", bStateString); + + + if((long)aState%2) { + aState = (mdd_t *)((long)aState -1); + forced++; + } + else forced = 0; + + if((long)bState%2) { + bState = (mdd_t *)((long)bState -1); + } + + if ( printInput == TRUE && i != -1) { + inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, aState, bState ); + vInput = Mc_ComputeACloseMinterm( inputSet, uInput, inputVars, mddMgr ); + } + if(forced) { + fprintf(vis_stdout, "---- Forced %d\n", forced); + numForced ++; + } + McPrintTransitionMine( aState, bState, uInput, vInput, psVars, inputVars, + printInput, modelFsm, CEXPath, (i+1), cnfClauses); + + + + if ( uInput != NIL(mdd_t) ) { + mdd_free(uInput); + } + uInput = vInput; + + if ( inputSet != NIL(mdd_t) ) { + mdd_free(inputSet); + } + } + + if ( vInput != NIL(mdd_t) ) { + mdd_free(uInput); + } + + if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) { + fprintf(vis_stdout, + "# MC: the number of non-trivial forced segments %d\n", + numForced); + } + + FILE *cnfFile = fopen(CNF_FILE_C1,"w"); + mAig_Manager_t * maigManager = Ntk_NetworkReadMAigManager(ntk); + BmcWriteClausesMine(maigManager, cnfFile, cnfClauses, options); + fclose(cnfFile); + + (void) fprintf(vis_stderr, "*** Generation of CNF clauses for Counter Example completed. *** \n\n"); + // --- SAT Solver --- + options->satInFile= CNF_FILE_C1; + options->verbosityLevel=BmcVerbositySome_c; + + SATSolver (steps, options); + (void) fprintf(vis_stderr, "*** SAT Solver completed. *** \n"); + + return 1; +} + + +/**Function******************************************************************** + + Synopsis [Print a transition to vis_stdout.] + + Description [Print a transition to vis_stdout. The transition is supposed to be + from aState to bState on input vInput. If uInput is not NIL, instead of + printing vInput, we only print the places where it differs from uInput. If there + is no difference anywhere, we print "-Unchanged-". Similarly, we print only the + incremental difference from aState to bState; if there is none, we print "-Unchanged-". + If aState is NIL we simply print bState and return.] + + SideEffects [] + +******************************************************************************/ +static void +McPrintTransitionMine( + mdd_t *aState, + mdd_t *bState, + mdd_t *uInput, + mdd_t *vInput, + array_t *stateSupport, + array_t *inputSupport, + boolean printInputs, + Fsm_Fsm_t *modelFsm, + CEXStruct *CEXPath, + int seqNumber, + BmcCnfClauses_t *cnfClauses) +{ + (void) fprintf(vis_stderr, "![McPrintTransitionMine] \n"); + Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm ); + char *aString = aState ? Mc_MintermToString( aState, stateSupport, modelNetwork ) : NIL(char); + char *bString = Mc_MintermToString( bState, stateSupport, modelNetwork ); + + char *tmp1String = aString; + char *tmp2String = bString; + char *ptr1; + char *ptr2; + st_table *node2MvfAigTable; + + node2MvfAigTable = + (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY); + + if ( aState == NIL(mdd_t) ) { + fprintf( vis_stdout, "--State %d:\n%s\n", seqNumber, bString ); + FREE(bString); + return; + } + + fprintf(vis_stdout, "--Goes to state %d:\n", seqNumber ); + + { + boolean unchanged=TRUE; + while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) { + ptr2 = strchr( tmp2String, '\n' ); + *ptr1 = 0; + *ptr2 = 0; + if ( (strcmp( tmp1String, tmp2String ) ) ) { + fprintf( vis_stdout, "%s\n", tmp2String ); + unchanged = FALSE; + } + tmp1String = & (ptr1[1]); + tmp2String = & (ptr2[1]); + } + if (unchanged == TRUE) { + fprintf( vis_stdout, "\n"); + } + } + + if ( array_n( inputSupport ) > 0 ) { + CEXPath[seqNumber].n_inputVar = array_n( inputSupport ); + } + else CEXPath[seqNumber].n_inputVar = 0; + + (void) fprintf(vis_stderr, " ---- [McPrintTransitionMine] NUMBER OF INPUTS: CEXPath[%d].n_inputVar = %d \n", seqNumber, CEXPath[seqNumber].n_inputVar); + CEXPath[seqNumber].inputVar = (CEXVarStruct *)malloc(sizeof(CEXVarStruct)*CEXPath[seqNumber].n_inputVar); + + if ( printInputs == TRUE ) { + +// (void) fprintf(vis_stderr, " ---- [McPrintTransitionMine] NUMBER OF INPUTS = %d \n", array_n( inputSupport )); + + + /* first test that there are inputs */ + if ( array_n( inputSupport ) > 0 ) { + fprintf(vis_stdout, "--On input:\n"); + + if ( uInput == NIL(mdd_t) ) { + char *vString = Mc_MintermToStringMine( vInput, inputSupport, modelNetwork, CEXPath, seqNumber, TRUE, cnfClauses); + fprintf(vis_stdout, "%s", vString ); + FREE(vString); + } + else { + boolean unchanged=TRUE; + char *uString = Mc_MintermToString( uInput, inputSupport, modelNetwork ); + char *vString = Mc_MintermToStringMine( vInput, inputSupport, modelNetwork, CEXPath, seqNumber, TRUE, cnfClauses); + tmp1String = uString; + tmp2String = vString; +// (void) fprintf(vis_stderr, " ---- [McPrintTransitionMine] uString = %s \n", uString); +// (void) fprintf(vis_stderr, " ---- [McPrintTransitionMine] vString = %s \n", vString); + + while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) { + ptr2 = strchr( tmp2String, '\n' ); + *ptr1 = 0; + *ptr2 = 0; + if ( (strcmp( tmp1String, tmp2String ) ) ) { + fprintf( vis_stdout, "%s\n", tmp2String ); + unchanged = FALSE; + } + tmp1String = & (ptr1[1]); + tmp2String = & (ptr2[1]); + } + if (unchanged == TRUE) { + fprintf( vis_stdout, "\n"); + } + FREE(uString); + FREE(vString); + } + } + } + + FREE( aString ); + FREE( bString ); + fprintf (vis_stdout, "\n"); +} + + +/**Function******************************************************************** + + Synopsis [Print a minterm.] + + SideEffects [] + +******************************************************************************/ +static void +Mc_MintermPrintMine( + mdd_t *aMinterm, + array_t *support, + Ntk_Network_t *aNetwork) +{ + char *tmpString = Mc_MintermToString( aMinterm, support, aNetwork ); // to be modified!! + fprintf( vis_stdout, "%s", tmpString ); + FREE(tmpString); +} + + +/**Function******************************************************************** + + Synopsis [Return a string for a minterm. Only used in 'Mc_PrintPathMine' + function] + + SideEffects [] + +******************************************************************************/ +static char * +Mc_MintermToStringMine( + mdd_t *aMinterm, + array_t *aSupport, + Ntk_Network_t *aNetwork, + CEXStruct *CEXPath, + int seqNumber, + boolean inOutIndicator, // TRUE = input Variables, FALSE = output Variables (independent printInput option) + BmcCnfClauses_t *cnfClauses) +{ + (void) fprintf(vis_stderr, "![Mc_MintermToStringMine] \n"); + int i; + char *tmp1String; + char *tmp2String; + char bodyString[McMaxStringLength_c]; + char *mintermString = NIL(char); + mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork ); + array_t *valueArray; + array_t *stringArray = array_alloc( char *, 0 ); + char *symbolicValue; + + aMinterm = GET_NORMAL_PT(aMinterm); + valueArray = McConvertMintermToValueArrayMine(aMinterm, aSupport, mddMgr); +// (void) fprintf(vis_stderr, " ---- [Mc_MintermToStringMine] CEX n outputs = %d \n", array_n( aSupport )); +// (void) fprintf(vis_stderr, " ----- [Mc_MintermToStringMine] Number of variables = %d \n", array_n( aSupport )); + +// CEXVarStruct testBB [array_n( aSupport)]; + + for ( i = 0 ; i < array_n( aSupport ); i++ ) { + + int mddId = array_fetch( int, aSupport, i ); + int value = array_fetch( int, valueArray, i ); + Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); + char *nodeName = Ntk_NodeReadName( node ); + Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node ); + +// (void) fprintf(vis_stderr, "\n ----- [Mc_MintermToStringMine] VARIABLE %d: \n", i+1 ); +// (void) fprintf(vis_stderr, " ----- [Mc_MintermToStringMine] nodeName = %s \n", nodeName); +// (void) fprintf(vis_stderr, " ----- [Mc_MintermToStringMine] mddId = %d \n", mddId); +// (void) fprintf(vis_stderr, " ----- [Mc_MintermToStringMine] value = %d \n", value); + + if ( Var_VariableTestIsSymbolic( nodeVar ) ) { + symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value ); +// (void) fprintf(vis_stderr, " ----- [Mc_MintermToStringMine] symbolic value = %s \n", symbolicValue); + sprintf( bodyString, "%s:%s", nodeName, symbolicValue ); + //testBB[i].symbolicValue = symbolicValue; + // sprintf(testBB[i].symbolicValue, "%s", symbolicValue); + } + else { + sprintf( bodyString, "%s:%d", nodeName, value ); + //testBB[i].symbolicValue = NIL(char); + symbolicValue = "NIL"; +// sprintf(testBB[i].symbolicValue, "%s", "NIL"); + } + + + if (inOutIndicator == TRUE) { + CEXPath[seqNumber].inputVar[i].varIndex = i; + CEXPath[seqNumber].inputVar[i].varId = mddId; + CEXPath[seqNumber].inputVar[i].varValue = value; + sprintf(CEXPath[seqNumber].inputVar[i].varName, "%s", nodeName); + sprintf(CEXPath[seqNumber].inputVar[i].symbolicValue, "%s", symbolicValue); + } + else{ + CEXPath[seqNumber].outputVar[i].varIndex = i; + CEXPath[seqNumber].outputVar[i].varId = mddId; + CEXPath[seqNumber].outputVar[i].varValue = value; + sprintf(CEXPath[seqNumber].outputVar[i].varName, "%s", nodeName); + sprintf(CEXPath[seqNumber].outputVar[i].symbolicValue, "%s", symbolicValue); + } + +// testBB[i].varIndex = i; +// testBB[i].varId = mddId; +// testBB[i].varValue = value; +// sprintf(testBB[i].varName, "%s", nodeName); +// testBB[i].varName = nodeName; + + + + tmp1String = util_strsav( bodyString ); + array_insert_last( char *, stringArray, tmp1String ); + } + array_free(valueArray); + + array_sort( stringArray, cmp); + + for ( i = 0 ; i < array_n( stringArray ); i++ ) { + tmp1String = array_fetch( char *, stringArray, i ); + if( i == 0 ) { + mintermString = util_strcat3(tmp1String, "", "" ); + } + else { + tmp2String = util_strcat3(mintermString, "\n", tmp1String ); + FREE(mintermString); + mintermString = tmp2String; + } + FREE(tmp1String); + } + array_free( stringArray ); + + tmp1String = util_strcat3(mintermString, "\n", ""); + FREE(mintermString); + mintermString = tmp1String; + + int j, k; + boolean indexFound; + int lookUpResult; + int n_bitValue; // number of bit - 1 = highest bit number representing the value of the variable + int *cnfIndex= malloc(sizeof(int)*SIZE_1); + int newIndex; + array_t * newClause; + char *tempCNFString; + + for ( i = 0 ; i < array_n( aSupport ); i++ ) { + + j=0; + indexFound = TRUE; + + if (inOutIndicator == TRUE) { +/* (void) fprintf(vis_stderr, "\n CEXPath[%d].inputVar[%d].varIndex = %d \n", seqNumber, i, CEXPath[seqNumber].inputVar[i].varIndex); + (void) fprintf(vis_stderr, " CEXPath[%d].inputVar[%d].varId = %d \n", seqNumber, i, CEXPath[seqNumber].inputVar[i].varId); + (void) fprintf(vis_stderr, "\n"); + (void) fprintf(vis_stderr, " CEXPath[%d].inputVar[%d].varValue = %d \n", seqNumber, i, CEXPath[seqNumber].inputVar[i].varValue); + (void) fprintf(vis_stderr, " CEXPath[%d].inputVar[%d].varName = %s \n", seqNumber, i, CEXPath[seqNumber].inputVar[i].varName); + (void) fprintf(vis_stderr, " CEXPath[%d].inputVar[%d].symbolicValue = %s \n", seqNumber, i, CEXPath[seqNumber].inputVar[i].symbolicValue); +*/ + + // insertion of cnf clauses related to the input in Counter Example at each state + do{ + tempCNFString = CNFVariableNameConstructor(CEXPath[seqNumber].inputVar[i].varName, j, seqNumber-1); // the sequence of input begins at -1 and ends at (last sequence-1) + lookUpResult = st_lookup(cnfClauses->cnfIndexTable, tempCNFString, &cnfIndex[j]); + // (void) fprintf(vis_stderr, "[SeqNumber: %d][i: %d][j: %d] tempCNFString = %s; lookUpResult = %d; cnfIndex = %d;\n", seqNumber, i, j, tempCNFString, lookUpResult, cnfIndex); + if (lookUpResult == 0) { + indexFound = FALSE; + } + else { + indexFound = TRUE; + (void) fprintf(vis_stderr, " [CNF Index Search] Variable bit name = %s => CNF Index = %d \n", tempCNFString, cnfIndex[j]); + j++; + } + }while ((indexFound == TRUE)&&(j 0){ + // Value decomposition en binary. Then affectation of the value of each bit of the variable in CNF format for each index of the variable + + int *binaryValue = malloc (sizeof(int)*(n_bitValue+1)); + binaryValue = DecBinConverter (CEXPath[seqNumber].inputVar[i].varValue, (n_bitValue+1), binaryValue); + +// (void) fprintf(vis_stderr, "---- Decimal Value = %d ==> Binary Value = ", CEXPath[seqNumber].inputVar[i].varValue); +// for (k=0; k < n_bitValue+1; k++){ +// (void) fprintf(vis_stderr, "%d ", binaryValue[n_bitValue-k]); +// } + + for (k=0; k<(n_bitValue+1); k++){ + + newClause = array_alloc(int,1); + // if varValue = 1 => cnfIndex; if varValue = 0 => -cnfIndex +// (void) fprintf(vis_stderr, "CNF Index = %d : Value = %d \n", cnfIndex[k], binaryValue[k]); +// if (binaryValue[k] == 0) array_insert(int,newClause,0,-cnfIndex[k]); +// else array_insert(int, newClause, 0, cnfIndex[k]); + +// NOTE: MSB is on lowest bit encoding +// (void) fprintf(vis_stderr, "CNF Index = %d : Value = %d \n", cnfIndex[k], binaryValue[n_bitValue-k]); + if (binaryValue[n_bitValue-k] == 0) array_insert(int,newClause,0,-cnfIndex[k]); + else array_insert(int, newClause, 0, cnfIndex[k]); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + } + free (binaryValue); + // (void) fprintf(vis_stderr, "![WARNING] Variable is coded in more than one bit. This case is not yet treated. \n", n_bitValue); + + } + else{ + if (n_bitValue == 0){ + newClause = array_alloc(int,1); + // if varValue = 1 => cnfIndex; if varValue = 0 => -cnfIndex + if (CEXPath[seqNumber].inputVar[i].varValue == 0) array_insert(int,newClause,0,-cnfIndex[0]); + else array_insert(int, newClause, 0, cnfIndex[0]); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + } + else { // n_bitValue = -1 or <0 + (void) fprintf(vis_stderr, "![WARNING] Variable CNF index not found. Verification required. \n", CEXPath[seqNumber].outputVar[i].varName, seqNumber); + } + } + } + else { + (void) fprintf(vis_stderr, "![WARNING] Too many CNF index found for %s at state %d! Verification required.. counter j exceeded security constraint (j < SIZE_1 = 100). \n" ); + } + + + } + else{ +/* (void) fprintf(vis_stderr, "\n CEXPath[%d].outputVar[%d].varIndex = %d \n", seqNumber, i, CEXPath[seqNumber].outputVar[i].varIndex); + (void) fprintf(vis_stderr, " CEXPath[%d].outputVar[%d].varId = %d \n", seqNumber, i, CEXPath[seqNumber].outputVar[i].varId); + (void) fprintf(vis_stderr, " CEXPath[%d].outputVar[%d].varValue = %d \n", seqNumber, i, CEXPath[seqNumber].outputVar[i].varValue); + (void) fprintf(vis_stderr, " CEXPath[%d].outputVar[%d].varName = %s \n", seqNumber, i, CEXPath[seqNumber].outputVar[i].varName); + (void) fprintf(vis_stderr, " CEXPath[%d].outputVar[%d].symbolicValue = %s \n", seqNumber, i, CEXPath[seqNumber].outputVar[i].symbolicValue); +*/ + +//--- CNF: insertion of cnf clauses related to Counter Example output at each state +// if (i>0){ // to exclude the states in CNF + + do{ + tempCNFString = CNFVariableNameConstructor(CEXPath[seqNumber].outputVar[i].varName, j, seqNumber); + //int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName) + //propIndex = findIndex(cnfClauses, tempCNFString); + lookUpResult = st_lookup(cnfClauses->cnfIndexTable, tempCNFString, &cnfIndex[j]); + // (void) fprintf(vis_stderr, "[SeqNumber: %d][i: %d][j: %d] tempCNFString = %s; lookUpResult = %d; cnfIndex = %d;\n", seqNumber, i, j, tempCNFString, lookUpResult, cnfIndex); + if (lookUpResult == 0) { + indexFound = FALSE; + } + else { + indexFound = TRUE; + (void) fprintf(vis_stderr, " [CNF Index Search] Variable bit name = %s => CNF Index = %d \n", tempCNFString, cnfIndex[j]); + j++; + } + }while ((indexFound == TRUE)&&(j 0){ + // Value decomposition en binary. Then affectation of the value of each bit of the variable in CNF format for each index of the variable + + int *binaryValue = malloc (sizeof(int)*(n_bitValue+1)); + binaryValue = DecBinConverter (CEXPath[seqNumber].outputVar[i].varValue, (n_bitValue+1), binaryValue); + +// (void) fprintf(vis_stderr, "####### Decimal Value = %d ==> Binary Value = ", CEXPath[seqNumber].outputVar[i].varValue); +// for (k=0; k<(n_bitValue+1); k++){ +// (void) fprintf(vis_stderr, "%d ", binaryValue[n_bitValue-k]); +// } +// (void) fprintf(vis_stderr, "\n"); + + for (k=0; k<(n_bitValue+1); k++){ +// for (k=(n_bitValue); k>=0; k--){ + newClause = array_alloc(int,1); + // if varValue = 1 => cnfIndex; if varValue = 0 => -cnfIndex +// (void) fprintf(vis_stderr, "CNF Index = %d : Value = %d \n", cnfIndex[k], binaryValue[k]); +// if (binaryValue[k] == 0) array_insert(int,newClause,0,-cnfIndex[k]); +// else array_insert(int, newClause, 0, cnfIndex[k]); +// NOTE: MSB is on lowest bit encoding +// (void) fprintf(vis_stderr, "CNF Index = %d : Value = %d \n", cnfIndex[k], binaryValue[n_bitValue-k]); + if (binaryValue[n_bitValue-k] == 0) array_insert(int,newClause,0,-cnfIndex[k]); + else array_insert(int, newClause, 0, cnfIndex[k]); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + + } + free (binaryValue); + // (void) fprintf(vis_stderr, "![WARNING] Variable is coded in more than one bit. This case is not yet treated. \n", n_bitValue); + + } + else{ + if (n_bitValue == 0){ + newClause = array_alloc(int,1); + // if varValue = 1 => cnfIndex; if varValue = 0 => -cnfIndex + if (CEXPath[seqNumber].outputVar[i].varValue == 0) array_insert(int,newClause,0,-cnfIndex[0]); + else array_insert(int, newClause, 0, cnfIndex[0]); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + } + else { // n_bitValue = -1 or <0 + (void) fprintf(vis_stderr, "![WARNING] Variable CNF index not found. Verification required. \n", CEXPath[seqNumber].outputVar[i].varName, seqNumber); + } + } + } + else { + (void) fprintf(vis_stderr, "![WARNING] Too many CNF index found for %s at state %d! Verification required.. counter j exceeded security constraint (j < SIZE_1 = 100). \n" ); + } +// } + } + } + + return mintermString; +} + + + +/**Function******************************************************************** + + Synopsis [Convert a minterm to an array of integers] + + SideEffects [] + +******************************************************************************/ +static array_t * +McConvertMintermToValueArrayMine( + mdd_t *aMinterm, + array_t *aSupport, + mdd_manager *mddMgr) +{ + (void) fprintf(vis_stderr, "![McConvertMintermToValueArrayMine] \n"); + array_t *resultValueArray; + + /* this will be performed only in v0s-g executables */ + assert( MintermCheckWellFormed( aMinterm, aSupport, mddMgr )); + + resultValueArray = array_alloc( int, 0 ); + { + int i; + for( i = 0 ; i < array_n( aSupport ); i++ ) { + int aSupportVar = array_fetch( int, aSupport, i ); + int j; + for( j = 0 ; TRUE ; j++) { + + mdd_t *faceMdd, *tmpMdd; + array_t *tmpArray = array_alloc( int, 0 ); + + array_insert_last( int, tmpArray, j ); + faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray ); + array_free( tmpArray ); + + tmpMdd = mdd_and( faceMdd, aMinterm, 1, 1 ); + mdd_free( faceMdd ); + if ( !mdd_is_tautology( tmpMdd, 0 ) ) { + mdd_free( tmpMdd ); + array_insert_last( int, resultValueArray, j ); + break; + } + mdd_free( tmpMdd ); + } + } + } + + return resultValueArray; +} + +/**Function******************************************************************** + + Synopsis [Print message saying given state passes formula.] + + SideEffects [] + +******************************************************************************/ +static void +McStatePassesFormulaMine( + mdd_t *aState, + Ctlp_Formula_t *formula, + McDbgLevel debugLevel, + Fsm_Fsm_t *modelFsm) +{ + McStatePassesOrFailsFormulaMine( aState, formula, 1, debugLevel, modelFsm ); +} + + +/**Function******************************************************************** + + Synopsis [Print message saying given state fails formula.] + + SideEffects [] + +******************************************************************************/ +static void +McStateFailsFormulaMine( + mdd_t *aState, + Ctlp_Formula_t *formula, + McDbgLevel debugLevel, + Fsm_Fsm_t *modelFsm) +{ + McStatePassesOrFailsFormulaMine( aState, formula, 0, debugLevel, modelFsm ); +} + + +/**Function******************************************************************** + + Synopsis [Utility function - prints state passes or fails formula] + + SideEffects [] + +******************************************************************************/ +static void +McStatePassesOrFailsFormulaMine ( + mdd_t *aState, + Ctlp_Formula_t *formula, + int pass, + McDbgLevel debugLevel, + Fsm_Fsm_t *modelFsm) +{ + + (void) fprintf(vis_stderr, "![McStatePassesOrFailsFormulaMine] \n"); + array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); + char *formulaText = Ctlp_FormulaConvertToString( formula ); + Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm ); + + /* Nodes created in converting formulae like AU may not have text + * attached to them. */ + if (formulaText == NIL(char)) + return; + + fprintf( vis_stdout, "--State\n"); + Mc_MintermPrintMine( aState, PSVars, modelNetwork ); + if ( pass ) + fprintf( vis_stdout, "passes "); + else + fprintf( vis_stdout, "fails "); + + if( debugLevel > McDbgLevelMin_c) + fprintf(vis_stdout, "%s.\n\n", formulaText); + else + fprintf(vis_stdout, "\n\n"); + + FREE(formulaText); +} + + +/**Function******************************************************************** + + Synopsis [Compare two strings in the from of char **] + + SideEffects [] + +******************************************************************************/ +static int +cmp( + const void * s1, + const void * s2) +{ + return(strcmp(*(char **)s1, *(char **)s2)); +} + + + +/**Function******************************************************************** + + Synopsis [Test that given mdd is a minterm.] + + SideEffects [] + +******************************************************************************/ +static boolean +MintermCheckWellFormed( + mdd_t *aMinterm, + array_t *aSupport, + mdd_manager *mddMgr) +{ + + /* first check its support */ + if (!SetCheckSupport(aMinterm, aSupport, mddMgr)) { + return FALSE; + } + + /* now check its a minterm */ + { + float cardinality = mdd_count_onset( mddMgr, aMinterm, aSupport ); + if ( cardinality != 1 ) { + fprintf( vis_stderr, "-- onset is not one\n"); + return FALSE; + } + } + return TRUE; +} + + +/**Function******************************************************************** + + Synopsis [Test that given mdd is a minterm.] + + SideEffects [] + +******************************************************************************/ +static boolean +SetCheckSupport( + mdd_t *aMinterm, + array_t *aSupport, + mdd_manager *mddMgr) +{ + if (!mdd_check_support(mddMgr, aMinterm, aSupport)) { + fprintf(vis_stderr, + "** mc error: support of minterm is not contained in claimed support\n"); + return FALSE; + } + return TRUE; +} + + +/**Function******************************************************************** + + Synopsis [CNF Clause generator - variable name contruction] + + SideEffects [] + +******************************************************************************/ +static char *CNFVariableNameConstructor(char *varName, int varEncoding, int pathIndex) +{ + char tempStr [LENGTH_1]; + char *cnfVarName; + int nChar; + + nChar = sprintf(tempStr, "%s_%d_%d", varName, varEncoding, pathIndex); // value sign has to be added later + cnfVarName = tempStr; + //(void) fprintf(vis_stderr, "[TEST] CNF Variable Name : %s [number of characters = %d] >> return : %s\n", tempStr, nChar, cnfVarName); + + return cnfVarName; +} + +/**Function******************************************************************** + + Synopsis [ + c = a <-> b = (a=0)*(b=0) + (a=1)*(b=1) .... + For a given term (a=i)*(b=i), if either is Zero, don't generate + clauses for this term. + if both are One, don't generate clauses + for c. + ] + + SideEffects [] + +******************************************************************************/ +static void +BmcGenerateClausesFromStateTostateMine( + bAig_Manager_t *manager, + bAigEdge_t *fromAigArray, + bAigEdge_t *toAigArray, + int mvfSize, + int fromState, + int toState, + BmcCnfClauses_t *cnfClauses, + int outIndex) +{ + array_t *clause, *tmpclause; + int toIndex, fromIndex, cnfIndex; + int i; + + /* used to turn off the warning messages: might be left uninitialized. + We are sure that these two variables will not be used uninitialized. + */ + toIndex =0; + fromIndex = 0; + + for(i=0; i< mvfSize; i++){ + if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){ + return; /* the clause is always true */ + } + } + clause = array_alloc(int, 0); + for(i=0; i< mvfSize; i++){ + if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){ + if (toAigArray[i] != bAig_One){ + /* to State */ + + toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i], + toState,cnfClauses); + } + if (fromAigArray[i] != bAig_One){ + /* from State */ + fromIndex = BmcGenerateCnfFormulaForAigFunction(manager, + fromAigArray[i], + fromState, + cnfClauses); + } + /* + Create new var for the output of this node. We don't create variable for this node, we only + use its index number. + */ + cnfIndex = cnfClauses->cnfGlobalIndex++; /* index of the output of the OR of T(from, to) */ + + assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex); + assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex); + assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex); + + if (toAigArray[i] == bAig_One){ + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, -fromIndex); + array_insert(int, tmpclause, 1, cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, fromIndex); + array_insert(int, tmpclause, 1, -cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + } else if (fromAigArray[i] == bAig_One){ + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, -toIndex); + array_insert(int, tmpclause, 1, cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, toIndex); + array_insert(int, tmpclause, 1, -cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + } else { + tmpclause = array_alloc(int, 3); + array_insert(int, tmpclause, 0, -toIndex); + array_insert(int, tmpclause, 1, -fromIndex); + array_insert(int, tmpclause, 2, cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, toIndex); + array_insert(int, tmpclause, 1, -cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + + tmpclause = array_alloc(int, 2); + array_insert(int, tmpclause, 0, fromIndex); + array_insert(int, tmpclause, 1, -cnfIndex); + BmcCnfInsertClause(cnfClauses, tmpclause); + array_free(tmpclause); + } + array_insert_last(int, clause, cnfIndex); + } /* if */ +// (void) fprintf(vis_stderr, "[CNF] (%d) > To : %d; From : %d; cnfIndex : %d \n", i, toIndex, fromIndex, cnfIndex); + } /* for i loop */ + if (outIndex != 0 ){ + array_insert_last(int, clause, -outIndex); + } + BmcCnfInsertClause(cnfClauses, clause); + array_free(clause); + + return; +} + + +/**Function******************************************************************** + + Synopsis [Generate CNF formula for a path from state 'from' to state 'to'] + + Description [Unfold the transition relation 'k' states (k = to-from +1), and + generate clauses for each state. + + For a multi-valued latch of 4 vlaues. Two binary variables are used + to rpresent X, x1 and x0. For this latch, there exist three multi-valued + functions. + One for the binary reoresentation of the variable. For example the + second entry of the mvf = 1, iff ~x1 and x0. + The second mfv is for the data input of the latch. If the And/Inv graph + attached to an entry of this mvf equal to 1, X equal to the binary + representation corresponding to this entry. For example, if the And/ + INV graph attached to the first entry =1, then X = ~x1 & ~x0. + To generate the CNF to the transition relation, first generate CNF to + next state varaible using mvf of the latch. Then, generate CNF for + latch data input using current state variavles. Finaly, generate CNF + for the AND of these two MVF. This for every entry of the MVF. Then + OR the results. + The third MVF is for the initial value of the latch. It is treat the + same as the latch data input except if the initial value is constant. + + The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states. + BMC_NO_INITIAL_STATES otherwise. + ] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void +BmcCnfGenerateClausesForPathMine( + Ntk_Network_t *network, + int from, + int to, + int initialState, + BmcCnfClauses_t *cnfClauses, + st_table *nodeToMvfAigTable, + st_table *CoiTable) +{ + mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); + st_generator *stGen; + + Ntk_Node_t *latch, *latchData, *latchInit; + MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig; + bAigEdge_t *initBAig, *latchBAig, *dataBAig; + + int i, k, mvfSize; + + st_foreach_item(CoiTable, stGen, &latch, NULL) { + + + latchInit = Ntk_LatchReadInitialInput(latch); + latchData = Ntk_LatchReadDataInput(latch); + + /* Get the multi-valued function for each node*/ + initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable); + if (initMvfAig == NIL(MvfAig_Function_t)){ + (void) fprintf(vis_stderr, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit)); + return; + } + dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable); + if (dataMvfAig == NIL(MvfAig_Function_t)){ + (void) fprintf(vis_stderr, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData)); + return; + } + latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); + if (latchMvfAig == NIL(MvfAig_Function_t)){ + latchMvfAig = Bmc_NodeBuildMVF(network, latch); + array_free(latchMvfAig); + latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); + } + + mvfSize = array_n(initMvfAig); + initBAig = ALLOC(bAigEdge_t, mvfSize); + dataBAig = ALLOC(bAigEdge_t, mvfSize); + latchBAig = ALLOC(bAigEdge_t, mvfSize); + + for(i=0; i< mvfSize; i++){ + dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i)); + latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i)); + initBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i)); + } + /* + if (from == 0){ + */ + if (initialState == BMC_INITIAL_STATES){ + /* Generate the CNF for the initial state of the latch */ + BmcGenerateClausesFromStateTostateMine(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0); + } + /* Generate the CNF for the transition functions */ + for (k=from; k < to; k++){ + BmcGenerateClausesFromStateTostateMine(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0); + } /* for k state loop */ + + FREE(initBAig); + FREE(dataBAig); + FREE(latchBAig); + }/* For each latch loop*/ + + return; +} + + + +/**Function******************************************************************** + + Synopsis [Write the set of clauses in diamacs format to the output file.] + + SideEffects [] + +******************************************************************************/ +static void +BmcWriteClausesMine( + mAig_Manager_t *maigManager, + FILE *cnfFile, + BmcCnfClauses_t *cnfClauses, + BmcOption_t *options) +{ + st_generator *stGen; + char *name; + int cnfIndex, i, k; + + if (options->verbosityLevel == BmcVerbosityMax_c) { + fprintf(vis_stderr, + "\n--- [CNF] Number of Variables = %d Number of Clauses = %d\n", + cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); + } + st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) { + fprintf(cnfFile, "c %s %d\n",name, cnfIndex); + } + (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1, + cnfClauses->noOfClauses); + if (cnfClauses->clauseArray != NIL(array_t)) { + for (i = 0; i < cnfClauses->nextIndex; i++) { + k = array_fetch(int, cnfClauses->clauseArray, i); + (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' '); + } + } + return; +} + + +/**Function******************************************************************** + + Synopsis [Decimal value to binary converter - Done by Me] + + SideEffects [] + +******************************************************************************/ + +static int *DecBinConverter (int decValue, int size, int *binValue){ + + int i; +// int tempVal; +// int *binValue = malloc (sizeof(int)*size); + +// tempVal = decValue; + for (i=0; i> 1; + } + + return binValue; +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [- Done by Cecile Braunstein] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void printSATAssig( array_t* result) +{ + int k; + printf("RESULT : \n"); + for(k=0; k< array_n(result); k++){ + printf("%d\n",array_fetch(int, result, k)); + } +} + +/**Function******************************************************************** + + Synopsis [] + + Description [- Done by Cecile Braunstein] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName) +{ + int index; + + st_lookup(cnfClauses->cnfIndexTable,nodeName,&index); + return index; + +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [- Done by Cecile Braunstein] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static st_table * generateAllLatches(Ntk_Network_t * ntk) +{ + st_table *CoiTable = st_init_table(st_ptrcmp, st_ptrhash); + lsGen gen ; + Ntk_Node_t *node; + + Ntk_NetworkForEachNode(ntk,gen, node){ + if (Ntk_NodeTestIsLatch(node)){ + st_insert(CoiTable, (char *) node, (char *) 0); + } + } + return CoiTable; +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [- Done by Cecile Braunstein] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static void build_unroll_circuit(Ntk_Network_t * ntk, int bound, BmcOption_t * options,BmcCnfClauses_t* cnfClauses) +{ + (void) fprintf(vis_stderr, "\n*** Generating CNF clauses for current network. *** \n"); + + st_table *CoiTable = generateAllLatches(ntk); + lsGen gen ; + Ntk_Node_t *node; + + + + Ntk_NetworkForEachNode(ntk,gen, node){ + if (Ntk_NodeTestIsLatch(node)){ + st_insert(CoiTable, (char *) node, (char *) 0); + } + } + + options->verbosityLevel = BmcVerbosityMax_c; + options->satSolver = CirCUs; + options->timeOutPeriod = 0; + options->printInputs = TRUE; + options->minK = bound; + options->maxK = bound; + options->step = bound; + options->dbgLevel = 1; + + //nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph + st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, MVFAIG_NETWORK_APPL_KEY); + assert(nodeToMvfAigTable != NIL(st_table)); + + // Create clauses database + int initState = BMC_INITIAL_STATES; + BmcCnfGenerateClausesForPathMine(ntk, 0, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable); + +} + + +/**Function******************************************************************** + + Synopsis [SAT Solver CNF File generator - Done by Cecile Braunstein] + + Description [ OBSOLETE!!! ] + + SideEffects [] + +******************************************************************************/ + +static int SATSolverFileGen (Hrc_Manager_t ** hmgr, char *fileName, int steps, BmcOption_t *options) +{ + + (void) fprintf(vis_stderr, "\n*** Generating CNF File for SAT Solver. *** \n"); + +// BmcOption_t *options = BmcOptionAlloc(); + BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t); + cnfClauses = BmcCnfClausesAlloc(); + Ntk_Network_t * ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + build_unroll_circuit(ntk,steps,options,cnfClauses); + + int propIndex; + int newIndex; + array_t * newClause; + char *tempCNFString; + + tempCNFString = CNFVariableNameConstructor("o2", 0, 0); + propIndex = findIndex(cnfClauses, tempCNFString); + newClause = array_alloc(int,1); + array_insert(int,newClause,0,-propIndex); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + + tempCNFString = CNFVariableNameConstructor("o2", 0, 1); + propIndex = findIndex(cnfClauses, tempCNFString); + newClause = array_alloc(int,1); + array_insert(int,newClause,0,-propIndex); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + + tempCNFString = CNFVariableNameConstructor("o2", 0, 2); + propIndex = findIndex(cnfClauses, tempCNFString); + newClause = array_alloc(int,1); + array_insert(int,newClause,0, -propIndex); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + + tempCNFString = CNFVariableNameConstructor("o2", 0, 3); + propIndex = findIndex(cnfClauses, tempCNFString); + newClause = array_alloc(int,1); + array_insert(int,newClause,0, propIndex); + BmcCnfInsertClause(cnfClauses, newClause); + array_free(newClause); + + + FILE *cnfFile = fopen(fileName,"w"); + mAig_Manager_t * maigManager = Ntk_NetworkReadMAigManager(ntk); + BmcWriteClausesMine(maigManager, cnfFile, cnfClauses, options); + fclose(cnfFile); + + return 0; +} + + +/**Function******************************************************************** + + Synopsis [- Done by Cecile Braunstein] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +static array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore, satArray_t *clauseIndexInCore) +{ + + satOption_t *satOption; + array_t *result = NIL(array_t); + int maxSize; + + satOption = sat_InitOption(); + satOption->verbose = options->verbosityLevel; + //satOption->unsatCoreFileName = "Ucore.txt"; + satOption->clauseDeletionHeuristic = 0; + satOption->coreGeneration = unsatcore; + satOption->minimizeConflictClause = 1; + + cm->comment = ALLOC(char, 2); + cm->comment[0] = ' '; + cm->comment[1] = '\0'; + cm->stdOut = stdout; + cm->stdErr = stderr; + + cm->option = satOption; + cm->each = sat_InitStatistics(); + + cm->unitLits = sat_ArrayAlloc(16); + cm->pureLits = sat_ArrayAlloc(16); + + maxSize = 10000 << (bAigNodeSize-4); + cm->nodesArray = ALLOC(bAigEdge_t, maxSize); + cm->maxNodesArraySize = maxSize; + cm->nodesArraySize = bAigNodeSize; + + sat_AllocLiteralsDB(cm); + + sat_ReadCNF(cm, options->satInFile); + sat_Main(cm); + if(cm->status == SAT_UNSAT) { + if (options->verbosityLevel != BmcVerbosityNone_c){ + (void) fprintf(vis_stderr, "# UNSAT\n"); + } + if(unsatcore) + { + clauseIndexInCore = cm->clauseIndexInCore; + } + fflush(cm->stdOut); + + }else if(cm->status == SAT_SAT) { + if (options->verbosityLevel != BmcVerbosityNone_c){ + (void) fprintf(vis_stderr, "# SAT\n"); + } + fflush(cm->stdOut); + result = array_alloc(int, 0); + { + int i, size, value; + + size = cm->initNumVariables * bAigNodeSize; + for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) { + value = SATvalue(i); + if(value == 1) { + array_insert_last(int, result, SATnodeID(i)); + } + else if(value == 0) { + array_insert_last(int, result, -(SATnodeID(i))); + } + } + } + } + return result; +} + + +/**Function******************************************************************** + + Synopsis [SAT Solver - Done by Cecile Braunstein] + + SideEffects [] + +******************************************************************************/ + +static int SATSolver (int steps, BmcOption_t *options) +{ + + (void) fprintf(vis_stderr, "*** SAT Solver begins. *** \n"); + + // Read another design and build new clauses + satManager_t *cm; + cm = sat_InitManager(0); + array_t * result = NIL(array_t); + satArray_t * coreArray= sat_ArrayAlloc(1024); + result = checkSATCircus(cm,options,steps,coreArray); + + return 0; +} + + + +