/**CFile*********************************************************************** FileName [debug.c] PackageName [debug] Synopsis [Debug package initialization, ending, and the command debug] Author [Cecile B.] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "debugInt.h" #include "imgInt.h" #include "partInt.h" static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12 braun Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv); static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv); static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv); static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int argc, char ** argv); static int CommandComposeWithCex(Hrc_Manager_t ** hmgr,int argc, char ** argv); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the test package.] SideEffects [] SeeAlso [Debug_End] ******************************************************************************/ void Debug_Init(void) { /* * Add a command to the global command table. By using the leading * underscore, the command will be listed under "help -a" but not "help". */ Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0); Cmd_CommandAdd("_transition", CommandTransition, 1); Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0); Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1); Cmd_CommandAdd("_cexbdd", CommandBuildCexBdd, 0); Cmd_CommandAdd("print_network_cnf", CommandGenerateNetworkCNF, 0); Cmd_CommandAdd("_compose", CommandComposeWithCex, 1); } /**Function******************************************************************** Synopsis [Ends the test package.] SideEffects [] SeeAlso [Debug_Init] ******************************************************************************/ void Debug_End(void) { /* * For example, free any global memory (if any) which the test package is * responsible for. */ } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv) { Ntk_Network_t * ntk; int c,verbose = 0; array_t * excludes = NIL(array_t); Dbg_Abnormal_t * abnormal; ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); char * subs; if (ntk == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** abn error: No network\n"); return 1; } while ((c = util_getopt(argc, argv, "vhs:")) != EOF) { switch(c) { case 'h': goto usage; case 'v': verbose = 1; break; case 's': subs = util_strsav(util_optarg); excludes = array_alloc(char*,0); array_insert_last(char*,excludes,subs); break; default : goto usage; } } abnormal = Dbg_DebugAbnormalAlloc(ntk); abnormal->verbose = verbose; printf("SUBS %s \n",subs); Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes); printf("\t # Abnormal predicate created %d\n", array_n(abnormal->abnormal)); return 0; usage : (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n"); (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); (void) fprintf(vis_stderr, " -v \t verbosity\n"); (void) fprintf(vis_stderr, " -s \texclude the abnormal predicate\ for this subssytem\n"); return 1; } /**Function******************************************************************** Synopsis [Implements the _sat_debug command.] CommandName [_sat_debug] CommandSynopsis [locate faulty candidates] CommandArguments [\[-h\] \[-v\]] CommandDescription [This command compute the fault candidates of a given properties.

Command options:

-h
Print the command usage.
-v
Verbose mode. ] SideEffects [] ******************************************************************************/ static int CommandSatDebug( Hrc_Manager_t ** hmgr, int argc, char ** argv){ int c,i; int verbose = 0; /* default value */ BmcOption_t * options = BmcOptionAlloc(); Ntk_Network_t * network; bAig_Manager_t * manager; array_t * formulaArray; array_t * LTLformulaArray; array_t * faultNodes = array_alloc(Ntk_Node_t*,0); /* * Parse command line options. */ if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { return 1; } if (verbose) { (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n"); } /* * Read the network */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** _sat_debug error: No network\n"); BmcOptionFree(options); return 1; } manager = Ntk_NetworkReadMAigManager(network); if (manager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n"); BmcOptionFree(options); return 1; } Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); if(abn == NIL(Dbg_Abnormal_t)){ (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n"); return 1; } if(verbose) printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn))); formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); if (formulaArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** bmc error: error in parsing CTL* Fromula from file\n"); BmcOptionFree(options); return 1; } if (array_n(formulaArray) == 0) { (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); BmcOptionFree(options); Ctlsp_FormulaArrayFree(formulaArray); return 1; } LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); Ctlsp_FormulaArrayFree(formulaArray); if (LTLformulaArray == NIL(array_t)){ (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); BmcOptionFree(options); return 1; } Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0); /* Compute the cone of influence here : a list of state variables (latches) TODO refine to COI of the property */ st_table *CoiTable = generateAllLatches(network); /* Generate clauses for each time frame. This is the old way of generating clauses in BMC. */ if(verbose) { (void) fprintf(vis_stdout, "------ COI ----\n"); printLatch(CoiTable); (void) fprintf(vis_stdout, "--------------------------\n"); } BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); //Generate ltl CNF // BmcGenerateCnfForLtl Génére la formule borné et retourne un index // après il faut ajouter l'objectif de l'index avec boucle ou pas ... // cf. BmcLtlVerifyGeneralLtl Ctlsp_FormulaPrint(vis_stdout, ltlFormula); fprintf(vis_stdout, "\n"); int k = options->maxK; int l; // return the clause number int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); printf("LTL %d \n",noLoopIndex); array_t *objClause = NIL(array_t); objClause = array_alloc(int, 0); array_insert_last(int, objClause, noLoopIndex); BmcCnfInsertClause(cnfClauses, objClause); array_free(objClause); //Add Abnormal st_table * nodeToMvfAigTable = NIL(st_table); nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); assert(nodeToMvfAigTable != NIL(st_table)); Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses); //loop abnormal int aIndex; Ntk_Node_t * abnNode; Dbg_ForEachAbnormal(abn,aIndex,abnNode){ char * nodeName = Ntk_NodeReadName(abnNode); //set abnormal for each step array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex); int cnfIndex; int step; bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex); array_t * cnfVal = array_alloc(int,0); arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses); array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex); array_insert_last(int,cnfVal,abnIndex); FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); BmcWriteClauses(manager, cnfFile, cnfClauses, options); fclose(cnfFile); printf("AINDEX %d\n",aIndex); if(aIndex == 0) { FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0); BmcWriteClauses(manager, cnfFile, cnfClauses, options); fclose(cnfFile); } }//end for each step //SAT procedure //assig assig input from cex //TODO build cex correctly int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel); // Build set of FaultCandidates if (res == SAT_SAT) { char * realNodeName = util_strsav(nodeName); realNodeName[strlen(nodeName)-3] = '\0'; printf("Real = %s\n", realNodeName); Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); array_insert_last(Ntk_Node_t*,faultNodes,realNode); } arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ int abnIndex = array_fetch(int,cnfVal,step); array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); } } if(verbose) (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ latches \n",cnfClauses->noOfClauses,st_count(CoiTable)); (void) fprintf(vis_stdout,"Number of Fault candidates %d\n", array_n(faultNodes)); (void) fprintf(vis_stdout,"gates : \n"); printNodeArray(faultNodes); Ctlsp_FormulaArrayFree(LTLformulaArray); BmcCnfClausesFree(cnfClauses); BmcOptionFree(options); array_free(faultNodes); return 0; } /**Function******************************************************************** Synopsis [Implements the generate_network_cnf.] CommandName [generate_network_cnf] CommandSynopsis [generate a CNF view of the network] CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ] CommandDescription [This command generate a CNF of the network in DMACS form. The network may be unroll within k steps.

Command options:

-h
Print the command usage.
-v
Verbose mode.
-k
number of steps (default 1). ] SideEffects [] ******************************************************************************/ static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv) { BmcOption_t *options = BmcOptionAlloc(); int c; unsigned int i; Ntk_Network_t * network; bAig_Manager_t * manager; char * outName = NIL(char); FILE *cnfFile; if (!options){ return 1; } options->dbgOut = 0; /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) { switch(c) { case 'h': goto usage; case 'k': options->maxK = atoi(util_optarg); break; case 'v': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg); break; default: goto usage; } } if (argc - util_optind != 0) { outName = util_strsav(argv[util_optind]); /* create SAT Solver input file */ options->cnfFileName= outName; options->satInFile = options->cnfFileName; cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); } /* * Read the network */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n"); BmcOptionFree(options); return 1; } manager = Ntk_NetworkReadMAigManager(network); if (manager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n"); BmcOptionFree(options); return 1; } /* Compute the cone of influence here : a list of state variables (latches) */ st_table *CoiTable = generateAllLatches(network); if(options->verbosityLevel) { (void) fprintf(vis_stdout, "------ COI ----\n"); printLatch(CoiTable); (void) fprintf(vis_stdout, "--------------------------\n"); } BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); if(outName != NIL(char)) { BmcWriteClauses(manager, cnfFile, cnfClauses, options); fclose(cnfFile); } else BmcWriteClauses(manager, vis_stdout, cnfClauses, options); if(options->verbosityLevel) { (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK); (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses, st_count(CoiTable)); } BmcOptionFree(options); return 0; usage: (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] \n"); (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\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, " The output file containing CNF of the network.\n"); BmcOptionFree(options); return 1; } /**Function******************************************************************** Synopsis [Implements the _Debug_test command.] CommandName [_Debug_test] CommandSynopsis [template for implementing commands] CommandArguments [\[-h\] \[-v\]] CommandDescription [This command does nothing useful. It merely serves as a template for the implementation of new commands.

Command options:

-h
Print the command usage.
-v
Verbose mode. ] SideEffects [] ******************************************************************************/ static int CommandDebug( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c; int verbose = 0; /* default value */ /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "vh")) != EOF) { switch(c) { case 'v': verbose = 1; break; case 'h': goto usage; default: goto usage; } } if (verbose) { (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n"); } Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); printf("** DEBUG MODE **\n"); Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr); printf("model : %s\n", Hrc_NodeReadModelName(n)); mdd_t * safe = getSafe(fsm); mdd_t * forbid = getForbidden(fsm); mdd_t * reach = getReach(fsm); if(safe == NIL(mdd_t)) { printf("call command set_safe before\n"); return 1; } if(forbid == NIL(mdd_t)) { printf("call command set_forbidden before\n"); return 1; } FILE* oFile; oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0); // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile); // mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile); mdd_t * EFState = mdd_and(reach,safe,1,1); // mdd_t * errorState = mdd_and(reach,forbid,1,1); mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, careStatesArray, 0,mddOne); mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, EFState, fsm->fairnessInfo.states, careStatesArray, 0, McDcLevelNone_c); mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1); mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile); tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, EXEFState, fsm->fairnessInfo.states, careStatesArray, 0, McDcLevelNone_c); mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); mdd_t * andState = mdd_xor(EXEFState2,EXEFState); mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile); tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, andState, fsm->fairnessInfo.states, careStatesArray, 0, McDcLevelNone_c); EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); andState = mdd_xor(EXEFState2,andState); mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, andState, fsm->fairnessInfo.states, careStatesArray, 0, McDcLevelNone_c); EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); andState = mdd_xor(EXEFState2,andState); mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile); //mdd_GetState_Values(mddManager , EFState, stdout); fclose(oFile); return 0; /* normal exit */ usage: (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); (void) fprintf(vis_stderr, " -v\t\tverbose\n"); return 1; /* error exit */ } /******************************************/ /* function that build a bdd for the */ /* simple example : */ /* (state = 0) -> !(state = 1) */ /******************************************/ mdd_t * buildDummyBdd(mdd_manager *mddManager) { /** state0 = 0 **/ mdd_t * s0 = mdd_eq_c(mddManager,0, 0); mdd_t * s1 = mdd_eq_c(mddManager,2, 0); mdd_t * state0 = mdd_one(mddManager); state0 = mdd_and(s0,s1,1,1); /** state1 = 1 **/ mdd_t * ns0 = mdd_eq_c(mddManager,1, 1); mdd_t * ns1 = mdd_eq_c(mddManager,3, 0); mdd_t * state1 = mdd_one(mddManager); state1 = mdd_and(ns0,ns1,1,1); /** state = 0) -> !(state = 1) **/ mdd_t * rel = mdd_one(mddManager); rel = mdd_or(state0,state1,0,0); return rel; } mdd_t * buildDummy2(mdd_manager * mddManager) { mdd_t * rel = NIL(mdd_t); mdd_t * state0 = mdd_one(mddManager); mdd_t * state2 = mdd_one(mddManager); mdd_t * state3 = mdd_one(mddManager); // state0 = s0 mdd_t * s0 = mdd_eq_c(mddManager,0, 0); mdd_t * s1 = mdd_eq_c(mddManager,2, 0); state0 = mdd_and(s0,s1,1,1); // state2 = s2 s0 = mdd_eq_c(mddManager,0, 0); s1 = mdd_eq_c(mddManager,2, 1); state2 = mdd_and(s0,s1,1,1); // state3 = s3 s0 = mdd_eq_c(mddManager,0, 1); s1 = mdd_eq_c(mddManager,2, 1); state3 = mdd_and(s0,s1,1,1); // Build transition relation array_t * mvarVal = array_alloc(int,0); array_insert_last(int, mvarVal,2); array_t * val = array_alloc(int,0); array_t * mvarName = array_alloc(char*,0); array_insert_last(char*, mvarName,"S1"); int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t)); array_insert(char*, mvarName,0,"I"); int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t)); array_insert_last(int, val,1); mdd_t * e1 = mdd_literal(mddManager, e1Id,val); mdd_t * e0 = mdd_literal(mddManager, e0Id,val); mdd_t * tmp2 = mdd_and(e1,e0,0,0); mdd_t * ne2_1 = mdd_or(e1,tmp2,1,1); mdd_t * ne2_0 = mdd_and(e1,e0,0,1); array_insert(char*, mvarName,0,"Next_SI"); int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t)); Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2); Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1); Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0); mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id); //bdd_print(relation); mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout); //bdd_ite return rel; } /**Function******************************************************************** Synopsis [Implements the transtion command.] CommandName [_transition] CommandSynopsis [compute new transition relation] CommandArguments [\[-h\] \[-v\]] CommandDescription [This command create a new transition relation that is a and of the Bdd of the old one and another bdd.

Command options:

-h
Print the command usage.
-v
Verbose mode. ] SideEffects [Change the fsm] ******************************************************************************/ static int CommandTransition (Hrc_Manager_t ** hmgr, int argc, char ** argv){ int c; int verbose = 0; /* default value */ /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "vh")) != EOF) { switch(c) { case 'v': verbose = 1; break; case 'h': goto usage; default: goto usage; } } if (verbose) { (void) fprintf(vis_stdout, "The _transition is under construction.\n"); } Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); Ntk_Network_t *network = NIL(Ntk_Network_t); mdd_manager *mddManager; mdd_t *rel = NIL(mdd_t); graph_t *partition; int i; /******************/ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if(network == NIL(Ntk_Network_t)) return 1; fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); if(fsm == NIL(Fsm_Fsm_t)) return 1; mddManager = Fsm_FsmReadMddManager(fsm); /********** Build cex ***********/ /* Here add the function */ /* that build the Bdd to and */ /* with the transtion relation */ /***********************************/ rel = buildDummyBdd(mddManager); if(rel == NIL(mdd_t)) { fprintf(vis_stdout,"Problem when building the new relation bdd\n"); return 1; } if (verbose) mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); /** Get image_info **/ Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); /**** The complete transtion relation ****/ // array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0); /*****************************************/ /*** For each latch rebuild the transition function ***/ /*** mvf table is composed of mdd for each possible ***/ /*** value of the latch ***/ ImgFunctionData_t * functionData = &(imageInfo->functionData); array_t *roots = functionData->roots; array_t *rangeVarMddIdArray = functionData->rangeVars; char * nodeName; arrayForEachItem(char *, roots, i, nodeName) { /* The new relation */ vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName); Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); int mddId = array_fetch(int, rangeVarMddIdArray, i); mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId); if(verbose){ int x; mdd_t * comp; Mvf_FunctionForEachComponent( mvf, x, comp){ printf("%s,%d mdd %d ",nodeName,x,mddId); mdd_FunctionPrintMain (mddManager ,comp,"MVF",vis_stdout); } } mdd_t * n_relation = mdd_and(relation,rel,1,1); /* Build for each possible value */ int nbValue = Mvf_FunctionReadNumComponents(mvf) ; int v ; Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue); for(v = 0; v 0), NIL(array_t)); fsm->reachabilityInfo.initialStates = init; fsm->reachabilityInfo.reachableStates = reach; if(verbose) Fsm_FsmReachabilityPrintResults(fsm,3, 0); Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, (void *) fsm); return 0; /* normal exit */ usage: (void) fprintf(vis_stderr, "usage: _transition [-h] [-v]\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); (void) fprintf(vis_stderr, " -v\t\tverbose\n"); return 1; /* error exit */ } static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr, int argc, char ** argv){ int c; int verbose = 0; /* default value */ /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "vh")) != EOF) { switch(c) { case 'v': verbose = 1; break; case 'h': goto usage; default: goto usage; } } if (verbose) { (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n"); } Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); Ntk_Network_t *network = NIL(Ntk_Network_t); mdd_manager *mddManager; Hrc_Manager_t *hmgrCex = NIL(Hrc_Manager_t); Fsm_Fsm_t *fsmCex = NIL(Fsm_Fsm_t); Ntk_Network_t *networkCex = NIL(Ntk_Network_t); mdd_t *rel = NIL(mdd_t); int i; /******************/ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if(network == NIL(Ntk_Network_t)) return 1; fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); if(fsm == NIL(Fsm_Fsm_t)) return 1; mddManager = Fsm_FsmReadMddManager(fsm); mdd_t * initOrig = Fsm_FsmComputeInitialStates(fsm); mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout); /********** Build cex ***********/ /* Here add the function */ /* that build the Bdd to and */ /* with the transtion relation */ /***********************************/ //rel = buildDummyBdd(mddManager); graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2"); Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2); mdd_t * s0 = mdd_eq_c(mddManager,20, 0); mdd_t * s1 = mdd_eq_c(mddManager,22, 0); mdd_t * state0 = mdd_one(mddManager); mdd_t * state1 = mdd_one(mddManager); state0 = mdd_and(s0,s1,1,1); mdd_t * state12 = mdd_and(s0,s1,0,1); state1 = mdd_not(state0); array_insert(mdd_t *, newMvf, 1, state0); array_insert(mdd_t *, newMvf, 0, state1); mdd_t * ns1 = mdd_eq_c(mddManager,17, 1); Mvf_Function_t * newNS = Mvf_FunctionAlloc( mddManager,2); Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1)); Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0)); mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout); vertex_t * vert; vert = Part_PartitionFindVertexByName(part,"cex.s2"); Part_VertexSetFunction(vert, newNS); vert = Part_PartitionFindVertexByName(part,"cex.s3"); mdd_t * ns1S3 = mdd_eq_c(mddManager,14, 1); Mvf_Function_t * newS3 = Mvf_FunctionAlloc( mddManager,2); Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1)); Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0)); Part_VertexSetFunction(vert, newS3); // Initial state mdd_t * ns1Init = mdd_eq_c(mddManager,3, 1); Mvf_Function_t * newNSInit = Mvf_FunctionAlloc(mddManager,2); Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1)); Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0)); mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout); Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"), newNSInit); /** Change the fsm and the network with a new partition and the new fsm **/ Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, (void *) part); fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part); mdd_t * init = Fsm_FsmComputeInitialStates(fsm); //mdd_t * n_init = Mvf_MddComposeWithFunction(init, 17 , newMvf); mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,1, NIL(array_t), (verbose > 0), NIL(array_t)); fsm->reachabilityInfo.initialStates = init; fsm->reachabilityInfo.reachableStates = reach; Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, (void *) fsm); Img_ImageInfoUpdateVariables(fsm->imageInfo, fsm->partition, fsm->fsmData.presentStateVars, fsm->fsmData.inputVars, fsm->fsmData.presentStateCube, fsm->fsmData.inputCube); Fsm_FsmReachabilityPrintResults(fsm,3, 0); // // mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout); return 0; /* normal exit */ usage: (void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); (void) fprintf(vis_stderr, " -v\t\tverbose\n"); return 1; /* error exit */ } static int CommandComposeWithCex(Hrc_Manager_t ** hmgr,int argc, char ** argv) { char * cexName; char * cexModelName; char * rootName; char * newName; FILE * cexFile; Hrc_Node_t * rootNode; Hrc_Node_t * cexNode; Hrc_Model_t * rootModel; Hrc_Model_t * cexModel; Hrc_Model_t * newModel; Hrc_Manager_t * hmgrCex; // Ntk_Network_t * networkCex; array_t *cexActualInputArray, *cexActualOutputArray; array_t *actualInputArray, *actualOutputArray; rootNode = Hrc_ManagerReadRootNode(*hmgr); if(rootNode == NIL(Hrc_Node_t)){ printf("Please build the network first\n"); return 1; } rootName = Hrc_NodeReadModelName(rootNode); rootModel = Hrc_ManagerFindModelByName(*hmgr,rootName); if (argc - util_optind > 0) { cexName = util_strsav(argv[util_optind]); cexFile = Cmd_FileOpen(cexName, "r", NIL(char *), 0); if(cexFile == NULL) (void) fprintf(vis_stderr, "%s not Found\n",cexName); } else goto usage; // Read_blif_mv hmgrCex = Io_BlifMvRead(cexFile,hmgrCex,0,0,0); if(hmgrCex == NIL(Hrc_Manager_t)){ fprintf(vis_stderr, "cannot open the hierrachy %\n",cexName); return 1; } st_table * modelTable = Hrc_ManagerReadModelTable(hmgrCex); if( st_count(modelTable) != 1){ fprintf(vis_stderr, "cannot open more than one cex model\n"); return 1; } st_generator * gen; Hrc_ManagerForEachModel( hmgrCex,gen,cexModelName,cexModel){} fprintf(vis_stderr, "Compose %s with %s\n",rootName, cexModelName); cexNode = Hrc_ManagerReadRootNode(hmgrCex); actualInputArray = array_dup(Hrc_NodeReadFormalInputs(rootNode)); actualOutputArray = array_dup(Hrc_NodeReadFormalOutputs(rootNode)); Hrc_ModelAddSubckt(rootModel,cexModel,cexModelName,actualInputArray, actualOutputArray); /* modelName = Hrc_NodeReadModelName(rootNode); newRootName = ALLOC(char, strlen(cexName)+ strlen(modelName) + 2); sprintf(newRootName,"%s_%s",modelName,cexName); Hrc_Model_t * newRootModel = Hrc_ModelAlloc(*hmgr,rootName); */ fclose(cexFile); return 0; /* normal exit */ usage: (void) fprintf(vis_stderr, "usage: _compose \n"); return 1; /* error exit */ /* // Read_blif_mv FILE *fpC; fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1); boolean isCanonicalC = 0; boolean isIncrementalC = 0; boolean isVerboseC = 0; hmgrCex = Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC); //flatten_hier lsList varNameList = (lsList) NULL; Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex); networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList); Ntk_NetworkSetMddManager(networkCex, mddManager); //static_order static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;; static Ord_RootMethod rootMethod = Ord_RootsByDefault_c; static Ord_OrderType suppliedOrderType = Ord_Unassigned_c; static Ord_OrderType generatedOrderType = Ord_InputAndLatch_c; static boolean nsAfterSupport = FALSE; lsList suppliedNodeList = (lsList) NULL; Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport, generatedOrderType, suppliedOrderType, suppliedNodeList, isVerboseC); //build_partition_mdd char * modelName = Hrc_NodeReadModelName(currentNode); static Part_PartitionMethod method = Part_Default_c; graph_t *partition; lsList nodeList = lsCreate(); boolean inTermsOfLeaves = FALSE; partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0, (lsList)0, NIL(mdd_t), method, nodeList, inTermsOfLeaves, isVerboseC, 0); // PartPartitionPrint(vis_stdout, partition); printf(" Cex loaded \n"); fsmCex = Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition); array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex); array_t * nextIdsCex = Fsm_FsmReadNextStateVars(fsmCex); printf("Next Names\n"); printStringArray(nextNamesCex); printf("Next Ids\n"); printIntArray(nextIdsCex); mddManager = Fsm_FsmReadMddManager(fsm); mdd_manager * mddManagerCex = Fsm_FsmReadMddManager(fsmCex); array_t *mvar_list, *bvar_list; mvar_list = mdd_ret_mvar_list(mddManager); bvar_list = mdd_ret_bvar_list(mddManager); printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list)); printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex); //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex); // mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout); graph_t * part = Fsm_FsmReadPartition(fsm); printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition)); */ }