#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 "concrete_model/concret_main.mv" #define FAIRNESS_FILE_C1 "concrete_model/machine_concret.fair" #define CTL_FILE_C1 "concrete_model/machine_concret.ctl" #define CNF_FILE_C1 "concrete_model/SATcnf_c1.cnf" #define DEBUG_FILE_C1 "concrete_model/debug_trace_crt" #define BLIF_MV_FILE_A1 "abstract_model/main_abstract.mv" #define FAIRNESS_FILE_A1 "abstract_model/main_abstract.fair" #define CTL_FILE_A1 "abstract_model/machine_concret.ctl" #define CNF_FILE_A1 "abstract_model/SATcnf_a1.cnf" #define DEBUG_FILE_A1 "abstract_model/debug_trace_abs" /*****************************************************/ /* #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; }