[27] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [debug.c] |
---|
| 4 | |
---|
| 5 | PackageName [debug] |
---|
| 6 | |
---|
[30] | 7 | Synopsis [Debug package initialization, ending, and the command debug] |
---|
[27] | 8 | |
---|
[35] | 9 | Author [Cecile B.] |
---|
[27] | 10 | |
---|
| 11 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
| 12 | All rights reserved. |
---|
| 13 | |
---|
| 14 | Permission is hereby granted, without written agreement and without license |
---|
| 15 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 16 | documentation for any purpose, provided that the above copyright notice and |
---|
| 17 | the following two paragraphs appear in all copies of this software. |
---|
| 18 | |
---|
| 19 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
| 20 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
| 21 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
| 22 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
| 23 | |
---|
| 24 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
| 25 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
| 26 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
| 27 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
| 28 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
| 29 | |
---|
| 30 | ******************************************************************************/ |
---|
| 31 | |
---|
| 32 | #include "debugInt.h" |
---|
[30] | 33 | #include "imgInt.h" |
---|
| 34 | #include "partInt.h" |
---|
[27] | 35 | static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12 braun Exp $"; |
---|
| 36 | |
---|
| 37 | /*---------------------------------------------------------------------------*/ |
---|
| 38 | /* Constant declarations */ |
---|
| 39 | /*---------------------------------------------------------------------------*/ |
---|
| 40 | |
---|
| 41 | /*---------------------------------------------------------------------------*/ |
---|
| 42 | /* Structure declarations */ |
---|
| 43 | /*---------------------------------------------------------------------------*/ |
---|
| 44 | |
---|
| 45 | /*---------------------------------------------------------------------------*/ |
---|
| 46 | /* Type declarations */ |
---|
| 47 | /*---------------------------------------------------------------------------*/ |
---|
| 48 | |
---|
| 49 | /*---------------------------------------------------------------------------*/ |
---|
| 50 | /* Variable declarations */ |
---|
| 51 | /*---------------------------------------------------------------------------*/ |
---|
| 52 | |
---|
| 53 | /*---------------------------------------------------------------------------*/ |
---|
| 54 | /* Macro declarations */ |
---|
| 55 | /*---------------------------------------------------------------------------*/ |
---|
| 56 | |
---|
| 57 | /**AutomaticStart*************************************************************/ |
---|
| 58 | |
---|
| 59 | /*---------------------------------------------------------------------------*/ |
---|
| 60 | /* Static function prototypes */ |
---|
| 61 | /*---------------------------------------------------------------------------*/ |
---|
| 62 | |
---|
[35] | 63 | static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
[27] | 64 | static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
[30] | 65 | static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
[35] | 66 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
[27] | 67 | |
---|
| 68 | |
---|
| 69 | /**AutomaticEnd***************************************************************/ |
---|
| 70 | |
---|
| 71 | |
---|
| 72 | /*---------------------------------------------------------------------------*/ |
---|
| 73 | /* Definition of exported functions */ |
---|
| 74 | /*---------------------------------------------------------------------------*/ |
---|
| 75 | |
---|
| 76 | /**Function******************************************************************** |
---|
| 77 | |
---|
| 78 | Synopsis [Initializes the test package.] |
---|
| 79 | |
---|
| 80 | SideEffects [] |
---|
| 81 | |
---|
| 82 | SeeAlso [Debug_End] |
---|
| 83 | |
---|
| 84 | ******************************************************************************/ |
---|
| 85 | void |
---|
| 86 | Debug_Init(void) |
---|
| 87 | { |
---|
| 88 | /* |
---|
| 89 | * Add a command to the global command table. By using the leading |
---|
| 90 | * underscore, the command will be listed under "help -a" but not "help". |
---|
| 91 | */ |
---|
[35] | 92 | Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0); |
---|
| 93 | Cmd_CommandAdd("_transition", CommandTransition, 1); |
---|
| 94 | Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0); |
---|
| 95 | Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1); |
---|
[27] | 96 | |
---|
| 97 | } |
---|
| 98 | |
---|
| 99 | |
---|
| 100 | /**Function******************************************************************** |
---|
| 101 | |
---|
| 102 | Synopsis [Ends the test package.] |
---|
| 103 | |
---|
| 104 | SideEffects [] |
---|
| 105 | |
---|
| 106 | SeeAlso [Debug_Init] |
---|
| 107 | |
---|
| 108 | ******************************************************************************/ |
---|
| 109 | void |
---|
| 110 | Debug_End(void) |
---|
| 111 | { |
---|
| 112 | /* |
---|
| 113 | * For example, free any global memory (if any) which the test package is |
---|
| 114 | * responsible for. |
---|
| 115 | */ |
---|
| 116 | } |
---|
| 117 | |
---|
| 118 | |
---|
| 119 | /*---------------------------------------------------------------------------*/ |
---|
| 120 | /* Definition of internal functions */ |
---|
| 121 | /*---------------------------------------------------------------------------*/ |
---|
| 122 | |
---|
| 123 | |
---|
| 124 | /*---------------------------------------------------------------------------*/ |
---|
| 125 | /* Definition of static functions */ |
---|
| 126 | /*---------------------------------------------------------------------------*/ |
---|
| 127 | |
---|
[35] | 128 | |
---|
[36] | 129 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv) |
---|
[35] | 130 | { |
---|
| 131 | Ntk_Network_t * ntk; |
---|
[36] | 132 | int c,verbose; |
---|
| 133 | Dbg_Abnormal_t * abnormal; |
---|
[35] | 134 | ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 135 | if (ntk == NIL(Ntk_Network_t)) { |
---|
| 136 | (void) fprintf(vis_stdout, "** abn error: No network\n"); |
---|
| 137 | return 1; |
---|
| 138 | } |
---|
[36] | 139 | while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) { |
---|
| 140 | switch(c) { |
---|
| 141 | case 'v': |
---|
| 142 | verbose = 1; |
---|
| 143 | break; |
---|
[35] | 144 | } |
---|
[36] | 145 | } |
---|
| 146 | abnormal = Dbg_DebugAbnormalAlloc(ntk); |
---|
| 147 | abnormal->verbose = verbose; |
---|
| 148 | Dbg_AddAbnormalPredicatetoNetwork(abnormal); |
---|
[35] | 149 | } |
---|
[27] | 150 | /**Function******************************************************************** |
---|
| 151 | |
---|
[35] | 152 | Synopsis [Implements the _sat_debug command.] |
---|
| 153 | |
---|
| 154 | CommandName [_sat_debug] |
---|
| 155 | |
---|
| 156 | CommandSynopsis [locate faulty candidates] |
---|
| 157 | |
---|
| 158 | CommandArguments [\[-h\] \[-v\]] |
---|
| 159 | |
---|
| 160 | CommandDescription [This command compute the fault candidates of a given |
---|
| 161 | properties.<p> |
---|
| 162 | |
---|
| 163 | Command options:<p> |
---|
| 164 | |
---|
| 165 | <dl> |
---|
| 166 | <dt> -h |
---|
| 167 | <dd> Print the command usage. |
---|
| 168 | </dl> |
---|
| 169 | |
---|
| 170 | <dt> -v |
---|
| 171 | <dd> Verbose mode. |
---|
| 172 | </dl> |
---|
| 173 | ] |
---|
| 174 | |
---|
| 175 | SideEffects [] |
---|
| 176 | |
---|
| 177 | ******************************************************************************/ |
---|
[38] | 178 | static int |
---|
| 179 | checkIndex( |
---|
| 180 | int index, |
---|
| 181 | BmcCnfClauses_t *cnfClauses) |
---|
| 182 | { |
---|
| 183 | int rtnValue = -1; /* it is not TRUE or FALSE*/ |
---|
[35] | 184 | |
---|
[38] | 185 | if (index == 0){ /* TRUE or FALSE*/ |
---|
| 186 | if (cnfClauses->emptyClause){ /* last added clause was empty = FALSE*/ |
---|
| 187 | rtnValue = 0; /* FALSE */ |
---|
| 188 | } else { |
---|
| 189 | /* |
---|
| 190 | if (cnfClauses->noOfClauses == 0) |
---|
| 191 | rtnValue = 1; |
---|
| 192 | } |
---|
| 193 | */ |
---|
| 194 | rtnValue = 1; /* TRUE */ |
---|
| 195 | } |
---|
| 196 | } |
---|
| 197 | return rtnValue; |
---|
| 198 | } |
---|
[35] | 199 | |
---|
[38] | 200 | |
---|
[35] | 201 | static int |
---|
| 202 | CommandSatDebug( |
---|
| 203 | Hrc_Manager_t ** hmgr, |
---|
| 204 | int argc, |
---|
| 205 | char ** argv){ |
---|
| 206 | int c,i; |
---|
| 207 | int verbose = 0; /* default value */ |
---|
| 208 | BmcOption_t *options = BmcOptionAlloc(); |
---|
| 209 | Ntk_Network_t * network; |
---|
| 210 | bAig_Manager_t *manager; |
---|
[38] | 211 | array_t *formulaArray; |
---|
| 212 | array_t *LTLformulaArray; |
---|
| 213 | char *ltlFileName = NIL(char); |
---|
[35] | 214 | |
---|
| 215 | /* |
---|
| 216 | * Parse command line options. |
---|
| 217 | */ |
---|
| 218 | util_getopt_reset(); |
---|
[38] | 219 | while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) { |
---|
[35] | 220 | switch(c) { |
---|
| 221 | case 'v': |
---|
| 222 | verbose = 1; |
---|
| 223 | options->verbosityLevel = verbose; |
---|
| 224 | break; |
---|
| 225 | case 'h': |
---|
| 226 | goto usage; |
---|
| 227 | case 'm': |
---|
| 228 | for (i = 0; i < strlen(util_optarg); i++) { |
---|
| 229 | if (!isdigit((int)util_optarg[i])) { |
---|
| 230 | goto usage; |
---|
| 231 | } |
---|
| 232 | } |
---|
| 233 | options->minK = atoi(util_optarg); |
---|
| 234 | break; |
---|
| 235 | case 'k': |
---|
| 236 | for (i = 0; i < strlen(util_optarg); i++) { |
---|
| 237 | if (!isdigit((int)util_optarg[i])) { |
---|
| 238 | goto usage; |
---|
| 239 | } |
---|
| 240 | } |
---|
| 241 | options->maxK = atoi(util_optarg); |
---|
| 242 | break; |
---|
| 243 | case 'o': |
---|
| 244 | options->cnfFileName = util_strsav(util_optarg); |
---|
[38] | 245 | break; |
---|
| 246 | case 'p': |
---|
| 247 | ltlFileName = util_strsav(util_optarg); |
---|
| 248 | break; |
---|
[35] | 249 | |
---|
| 250 | default: |
---|
| 251 | goto usage; |
---|
| 252 | } |
---|
| 253 | } |
---|
[38] | 254 | printf("MAX K %d", options->maxK); |
---|
[35] | 255 | if (options->minK > options->maxK){ |
---|
| 256 | (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n"); |
---|
| 257 | goto usage; |
---|
| 258 | } |
---|
| 259 | |
---|
| 260 | if (verbose) { |
---|
| 261 | (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n"); |
---|
| 262 | } |
---|
| 263 | /* create SAT Solver input file */ |
---|
| 264 | if (options->cnfFileName == NIL(char)) { |
---|
| 265 | options->satInFile = BmcCreateTmpFile(); |
---|
| 266 | } |
---|
| 267 | else { |
---|
| 268 | options->satInFile = options->cnfFileName; |
---|
| 269 | } |
---|
| 270 | |
---|
| 271 | /* create SAT Solver output file */ |
---|
| 272 | options->satOutFile = BmcCreateTmpFile(); |
---|
| 273 | if (options->satOutFile == NIL(char)){ |
---|
| 274 | BmcOptionFree(options); |
---|
| 275 | (void) fprintf(vis_stdout, "The _sat_debug problem.\n"); |
---|
| 276 | return 1; |
---|
| 277 | } |
---|
| 278 | |
---|
| 279 | options->verbosityLevel = 1; |
---|
| 280 | //options->satSolver |
---|
| 281 | //options->clauses |
---|
| 282 | |
---|
| 283 | /* |
---|
| 284 | * Read the network |
---|
| 285 | */ |
---|
| 286 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 287 | if (network == NIL(Ntk_Network_t)) { |
---|
| 288 | (void) fprintf(vis_stdout, "** bmc error: No network\n"); |
---|
| 289 | BmcOptionFree(options); |
---|
| 290 | return 1; |
---|
| 291 | } |
---|
| 292 | manager = Ntk_NetworkReadMAigManager(network); |
---|
| 293 | if (manager == NIL(mAig_Manager_t)) { |
---|
| 294 | (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n"); |
---|
| 295 | BmcOptionFree(options); |
---|
| 296 | return 1; |
---|
| 297 | } |
---|
[40] | 298 | |
---|
[35] | 299 | /* |
---|
| 300 | We need the bdd when building the transition relation of the automaton |
---|
| 301 | */ |
---|
| 302 | if(options->inductiveStep !=0){ |
---|
| 303 | Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t); |
---|
| 304 | |
---|
| 305 | designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 306 | if (designFsm == NIL(Fsm_Fsm_t)) { |
---|
| 307 | (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n"); |
---|
| 308 | return 1; |
---|
| 309 | } |
---|
| 310 | } |
---|
[40] | 311 | Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); |
---|
| 312 | printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn))); |
---|
[38] | 313 | /* |
---|
| 314 | * Read the formula |
---|
| 315 | */ |
---|
| 316 | /* Read LTL Formulae */ |
---|
| 317 | if (!ltlFileName) |
---|
| 318 | goto usage; |
---|
| 319 | |
---|
| 320 | options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0); |
---|
| 321 | if (options->ltlFile == NIL(FILE)) { |
---|
| 322 | (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName); |
---|
| 323 | FREE(ltlFileName); |
---|
| 324 | BmcOptionFree(options); |
---|
| 325 | } |
---|
| 326 | FREE(ltlFileName); |
---|
| 327 | |
---|
| 328 | formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); |
---|
| 329 | if (formulaArray == NIL(array_t)) { |
---|
| 330 | (void) fprintf(vis_stderr, |
---|
| 331 | "** bmc error: error in parsing CTL* Fromula from file\n"); |
---|
| 332 | BmcOptionFree(options); |
---|
| 333 | return 1; |
---|
| 334 | } |
---|
| 335 | if (array_n(formulaArray) == 0) { |
---|
| 336 | (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); |
---|
| 337 | BmcOptionFree(options); |
---|
| 338 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
| 339 | return 1; |
---|
| 340 | } |
---|
| 341 | LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); |
---|
| 342 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
| 343 | if (LTLformulaArray == NIL(array_t)){ |
---|
| 344 | (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); |
---|
| 345 | BmcOptionFree(options); |
---|
| 346 | return 1; |
---|
| 347 | } |
---|
| 348 | Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0); |
---|
| 349 | |
---|
| 350 | |
---|
| 351 | |
---|
[35] | 352 | /* |
---|
| 353 | Compute the cone of influence |
---|
[38] | 354 | here : a list of state variables (latches) |
---|
[35] | 355 | */ |
---|
| 356 | st_table *CoiTable = generateAllLatches(network); |
---|
| 357 | /* |
---|
| 358 | Generate clauses for each time frame. This is the old way of generating |
---|
| 359 | clauses in BMC. |
---|
| 360 | */ |
---|
| 361 | st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */ |
---|
| 362 | BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t); |
---|
| 363 | FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
| 364 | /* |
---|
| 365 | nodeToMvfAigTable maps each node to its multi-function And/Inv graph |
---|
| 366 | */ |
---|
| 367 | nodeToMvfAigTable = |
---|
| 368 | (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); |
---|
| 369 | assert(nodeToMvfAigTable != NIL(st_table)); |
---|
| 370 | |
---|
| 371 | if(verbose) |
---|
| 372 | { |
---|
| 373 | (void) fprintf(vis_stdout, "------ node to mvfaig ----\n"); |
---|
| 374 | printLatch(nodeToMvfAigTable); |
---|
| 375 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
| 376 | printLatch(CoiTable); |
---|
| 377 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
| 378 | } |
---|
| 379 | /* |
---|
| 380 | Create a clause database |
---|
| 381 | */ |
---|
| 382 | cnfClauses = BmcCnfClausesAlloc(); |
---|
| 383 | /* |
---|
| 384 | Generate clauses for an initialized path of length k |
---|
| 385 | */ |
---|
[38] | 386 | Ctlsp_FormulaPrint(vis_stdout, ltlFormula); |
---|
| 387 | fprintf(vis_stdout, "\n"); |
---|
[35] | 388 | BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES, |
---|
| 389 | cnfClauses, nodeToMvfAigTable, CoiTable); |
---|
[38] | 390 | |
---|
| 391 | //Generate ltl CNF |
---|
| 392 | // BmcGenerateCnfForLtl Génére la formule borné et retourne un index |
---|
| 393 | // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ... |
---|
| 394 | // cf. BmcLtlVerifyGeneralLtl |
---|
| 395 | int k = options->maxK; |
---|
| 396 | int l; |
---|
| 397 | // return the clause number |
---|
[40] | 398 | int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); |
---|
[38] | 399 | |
---|
| 400 | int leftValue = checkIndex(noLoopIndex, cnfClauses); |
---|
| 401 | printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); |
---|
[40] | 402 | array_t *objClause = NIL(array_t); |
---|
| 403 | objClause = array_alloc(int, 0); |
---|
| 404 | array_insert_last(int, objClause, noLoopIndex); |
---|
| 405 | BmcCnfInsertClause(cnfClauses, objClause); |
---|
| 406 | array_free(objClause); |
---|
[38] | 407 | |
---|
[40] | 408 | |
---|
| 409 | //TODO Add abnormal formula |
---|
[38] | 410 | |
---|
| 411 | |
---|
| 412 | |
---|
| 413 | |
---|
| 414 | |
---|
[35] | 415 | if(verbose) |
---|
| 416 | (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ |
---|
| 417 | latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable)); |
---|
| 418 | |
---|
[38] | 419 | Ctlsp_FormulaArrayFree(LTLformulaArray); |
---|
[35] | 420 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
| 421 | fclose(cnfFile); |
---|
| 422 | BmcCnfClausesFree(cnfClauses); |
---|
| 423 | BmcOptionFree(options); |
---|
| 424 | return 0; |
---|
| 425 | usage: |
---|
| 426 | (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \ |
---|
[38] | 427 | minimum length] [-o cnf_file] [-p ltl_file]\n"); |
---|
[35] | 428 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
| 429 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
| 430 | (void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n"); |
---|
| 431 | (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n"); |
---|
[38] | 432 | (void) fprintf(vis_stderr, " -o <cnf_file> contains CNF of the debug instance\n"); |
---|
| 433 | (void) fprintf(vis_stderr, " -p <ltl_file> contains the ltl formula\n"); |
---|
[35] | 434 | return 1; /* error exit */ |
---|
| 435 | |
---|
| 436 | } |
---|
| 437 | /**Function******************************************************************** |
---|
| 438 | |
---|
[27] | 439 | Synopsis [Implements the _Debug_test command.] |
---|
| 440 | |
---|
| 441 | CommandName [_Debug_test] |
---|
| 442 | |
---|
| 443 | CommandSynopsis [template for implementing commands] |
---|
| 444 | |
---|
| 445 | CommandArguments [\[-h\] \[-v\]] |
---|
| 446 | |
---|
| 447 | CommandDescription [This command does nothing useful. It merely serves as a |
---|
| 448 | template for the implementation of new commands.<p> |
---|
| 449 | |
---|
| 450 | Command options:<p> |
---|
| 451 | |
---|
| 452 | <dl> |
---|
| 453 | <dt> -h |
---|
| 454 | <dd> Print the command usage. |
---|
| 455 | </dl> |
---|
| 456 | |
---|
| 457 | <dt> -v |
---|
| 458 | <dd> Verbose mode. |
---|
| 459 | </dl> |
---|
| 460 | ] |
---|
| 461 | |
---|
| 462 | SideEffects [] |
---|
| 463 | |
---|
| 464 | ******************************************************************************/ |
---|
| 465 | static int |
---|
| 466 | CommandDebug( |
---|
| 467 | Hrc_Manager_t ** hmgr, |
---|
| 468 | int argc, |
---|
| 469 | char ** argv) |
---|
| 470 | { |
---|
| 471 | int c; |
---|
| 472 | int verbose = 0; /* default value */ |
---|
| 473 | |
---|
| 474 | /* |
---|
| 475 | * Parse command line options. |
---|
| 476 | */ |
---|
| 477 | util_getopt_reset(); |
---|
| 478 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
| 479 | switch(c) { |
---|
| 480 | case 'v': |
---|
| 481 | verbose = 1; |
---|
| 482 | break; |
---|
| 483 | case 'h': |
---|
| 484 | goto usage; |
---|
| 485 | default: |
---|
| 486 | goto usage; |
---|
| 487 | } |
---|
| 488 | } |
---|
| 489 | |
---|
| 490 | if (verbose) { |
---|
| 491 | (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n"); |
---|
| 492 | } |
---|
| 493 | |
---|
| 494 | Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 495 | mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); |
---|
| 496 | printf("** DEBUG MODE **\n"); |
---|
| 497 | Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr); |
---|
| 498 | printf("model : %s\n", Hrc_NodeReadModelName(n)); |
---|
| 499 | |
---|
| 500 | mdd_t * safe = getSafe(fsm); |
---|
| 501 | mdd_t * forbid = getForbidden(fsm); |
---|
| 502 | mdd_t * reach = getReach(fsm); |
---|
| 503 | |
---|
| 504 | if(safe == NIL(mdd_t)) |
---|
| 505 | { |
---|
| 506 | printf("call command set_safe before\n"); |
---|
| 507 | return 1; |
---|
| 508 | } |
---|
| 509 | if(forbid == NIL(mdd_t)) |
---|
| 510 | { |
---|
| 511 | printf("call command set_forbidden before\n"); |
---|
| 512 | return 1; |
---|
| 513 | } |
---|
| 514 | |
---|
| 515 | FILE* oFile; |
---|
| 516 | oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0); |
---|
| 517 | // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile); |
---|
| 518 | // mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile); |
---|
| 519 | |
---|
| 520 | mdd_t * EFState = mdd_and(reach,safe,1,1); |
---|
| 521 | // mdd_t * errorState = mdd_and(reach,forbid,1,1); |
---|
| 522 | |
---|
| 523 | mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); |
---|
| 524 | array_t *careStatesArray = array_alloc(mdd_t *, 0); |
---|
| 525 | array_insert(mdd_t *, careStatesArray, 0,mddOne); |
---|
| 526 | |
---|
| 527 | mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 528 | EFState, |
---|
| 529 | fsm->fairnessInfo.states, |
---|
| 530 | careStatesArray, |
---|
| 531 | 0, |
---|
| 532 | McDcLevelNone_c); |
---|
| 533 | |
---|
| 534 | mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 535 | mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile); |
---|
| 536 | |
---|
| 537 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 538 | EXEFState, |
---|
| 539 | fsm->fairnessInfo.states, |
---|
| 540 | careStatesArray, |
---|
| 541 | 0, |
---|
| 542 | McDcLevelNone_c); |
---|
| 543 | mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 544 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 545 | mdd_t * andState = mdd_xor(EXEFState2,EXEFState); |
---|
| 546 | mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile); |
---|
| 547 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 548 | andState, |
---|
| 549 | fsm->fairnessInfo.states, |
---|
| 550 | careStatesArray, |
---|
| 551 | 0, |
---|
| 552 | McDcLevelNone_c); |
---|
| 553 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 554 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 555 | andState = mdd_xor(EXEFState2,andState); |
---|
| 556 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
| 557 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 558 | andState, |
---|
| 559 | fsm->fairnessInfo.states, |
---|
| 560 | careStatesArray, |
---|
| 561 | 0, |
---|
| 562 | McDcLevelNone_c); |
---|
| 563 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 564 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 565 | andState = mdd_xor(EXEFState2,andState); |
---|
| 566 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
| 567 | |
---|
| 568 | |
---|
| 569 | |
---|
| 570 | //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile); |
---|
| 571 | //mdd_GetState_Values(mddManager , EFState, stdout); |
---|
| 572 | fclose(oFile); |
---|
| 573 | |
---|
| 574 | |
---|
| 575 | |
---|
| 576 | |
---|
| 577 | |
---|
| 578 | return 0; /* normal exit */ |
---|
| 579 | |
---|
| 580 | usage: |
---|
| 581 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
| 582 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
| 583 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
| 584 | return 1; /* error exit */ |
---|
| 585 | } |
---|
| 586 | |
---|
[30] | 587 | /******************************************/ |
---|
| 588 | /* function that build a bdd for the */ |
---|
| 589 | /* simple example : */ |
---|
| 590 | /* (state = 0) -> !(state = 1) */ |
---|
| 591 | /******************************************/ |
---|
| 592 | mdd_t * buildDummyBdd(mdd_manager *mddManager) |
---|
[27] | 593 | { |
---|
[30] | 594 | /** state0 = 0 **/ |
---|
| 595 | mdd_t * s0 = mdd_eq_c(mddManager,0, 0); |
---|
| 596 | mdd_t * s1 = mdd_eq_c(mddManager,2, 0); |
---|
| 597 | mdd_t * state0 = mdd_one(mddManager); |
---|
| 598 | state0 = mdd_and(s0,s1,1,1); |
---|
| 599 | /** state1 = 1 **/ |
---|
| 600 | mdd_t * ns0 = mdd_eq_c(mddManager,1, 1); |
---|
| 601 | mdd_t * ns1 = mdd_eq_c(mddManager,3, 0); |
---|
| 602 | mdd_t * state1 = mdd_one(mddManager); |
---|
| 603 | state1 = mdd_and(ns0,ns1,1,1); |
---|
| 604 | /** state = 0) -> !(state = 1) **/ |
---|
| 605 | mdd_t * rel = mdd_one(mddManager); |
---|
| 606 | rel = mdd_or(state0,state1,0,0); |
---|
| 607 | |
---|
| 608 | return rel; |
---|
| 609 | } |
---|
[27] | 610 | |
---|
| 611 | |
---|
| 612 | /**Function******************************************************************** |
---|
| 613 | |
---|
[30] | 614 | Synopsis [Implements the transtion command.] |
---|
[27] | 615 | |
---|
[30] | 616 | CommandName [_transition] |
---|
[27] | 617 | |
---|
[30] | 618 | CommandSynopsis [compute new transition relation] |
---|
[27] | 619 | |
---|
[30] | 620 | CommandArguments [\[-h\] \[-v\]] |
---|
| 621 | |
---|
| 622 | CommandDescription [This command create a new transition relation that is a |
---|
| 623 | and of the Bdd of the old one and an other bdd. |
---|
| 624 | <p> |
---|
[27] | 625 | |
---|
[30] | 626 | Command options:<p> |
---|
[27] | 627 | |
---|
[30] | 628 | <dl> |
---|
| 629 | <dt> -h |
---|
| 630 | <dd> Print the command usage. |
---|
| 631 | </dl> |
---|
[27] | 632 | |
---|
[30] | 633 | <dt> -v |
---|
| 634 | <dd> Verbose mode. |
---|
| 635 | </dl> |
---|
| 636 | ] |
---|
[27] | 637 | |
---|
[30] | 638 | SideEffects [Change the fsm] |
---|
[27] | 639 | |
---|
| 640 | ******************************************************************************/ |
---|
| 641 | |
---|
| 642 | static int |
---|
[30] | 643 | CommandTransition (Hrc_Manager_t ** hmgr, |
---|
[27] | 644 | int argc, char ** argv){ |
---|
[30] | 645 | int c; |
---|
| 646 | int verbose = 0; /* default value */ |
---|
[27] | 647 | |
---|
[30] | 648 | /* |
---|
| 649 | * Parse command line options. |
---|
| 650 | */ |
---|
| 651 | util_getopt_reset(); |
---|
| 652 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
| 653 | switch(c) { |
---|
| 654 | case 'v': |
---|
| 655 | verbose = 1; |
---|
| 656 | break; |
---|
| 657 | case 'h': |
---|
| 658 | goto usage; |
---|
| 659 | default: |
---|
| 660 | goto usage; |
---|
[27] | 661 | } |
---|
[30] | 662 | } |
---|
[27] | 663 | |
---|
[30] | 664 | if (verbose) { |
---|
| 665 | (void) fprintf(vis_stdout, "The _transition is under construction.\n"); |
---|
| 666 | } |
---|
[27] | 667 | |
---|
[30] | 668 | Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); |
---|
| 669 | Ntk_Network_t *network = NIL(Ntk_Network_t); |
---|
| 670 | mdd_manager *mddManager; |
---|
| 671 | mdd_t *rel = NIL(mdd_t); |
---|
| 672 | graph_t *partition; |
---|
| 673 | int i; |
---|
| 674 | /******************/ |
---|
| 675 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 676 | if(network == NIL(Ntk_Network_t)) |
---|
| 677 | return 1; |
---|
| 678 | fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 679 | if(fsm == NIL(Fsm_Fsm_t)) |
---|
| 680 | return 1; |
---|
| 681 | mddManager = Fsm_FsmReadMddManager(fsm); |
---|
[27] | 682 | |
---|
| 683 | |
---|
| 684 | |
---|
[30] | 685 | /********** Build cex ***********/ |
---|
| 686 | /* Here add the function */ |
---|
| 687 | /* that build the Bdd to and */ |
---|
| 688 | /* with the transtion relation */ |
---|
| 689 | /***********************************/ |
---|
| 690 | rel = buildDummyBdd(mddManager); |
---|
| 691 | if(rel == NIL(mdd_t)) |
---|
| 692 | { |
---|
| 693 | fprintf(vis_stdout,"Problem when building the new relation bdd"); |
---|
| 694 | return 1; |
---|
[27] | 695 | } |
---|
[37] | 696 | if (verbose) |
---|
| 697 | mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); |
---|
[27] | 698 | |
---|
[37] | 699 | |
---|
[30] | 700 | /** Get image_info **/ |
---|
| 701 | Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); |
---|
| 702 | partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); |
---|
| 703 | /**** The complete transtion relation ****/ |
---|
| 704 | // array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0); |
---|
| 705 | /*****************************************/ |
---|
| 706 | /*** For each latch rebuild the transition function ***/ |
---|
| 707 | /*** mvf table is composed of mdd for each possible ***/ |
---|
| 708 | /*** value of the latch ***/ |
---|
| 709 | ImgFunctionData_t * functionData = &(imageInfo->functionData); |
---|
| 710 | array_t *roots = functionData->roots; |
---|
| 711 | array_t *rangeVarMddIdArray = functionData->rangeVars; |
---|
| 712 | char * nodeName; |
---|
| 713 | arrayForEachItem(char *, roots, i, nodeName) { |
---|
| 714 | /* The new relation */ |
---|
| 715 | vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName); |
---|
| 716 | Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); |
---|
| 717 | int mddId = array_fetch(int, rangeVarMddIdArray, i); |
---|
| 718 | mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId); |
---|
| 719 | mdd_t * n_relation = mdd_and(relation,rel,1,1); |
---|
| 720 | /* Build for each possible value */ |
---|
| 721 | int nbValue = Mvf_FunctionReadNumComponents(mvf) ; |
---|
| 722 | int v ; |
---|
| 723 | Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue); |
---|
| 724 | for(v = 0; v<nbValue;v++) |
---|
| 725 | { |
---|
| 726 | mdd_t * n_s1 = mdd_eq_c(mddManager,mddId, v); |
---|
| 727 | mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1); |
---|
| 728 | mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1); |
---|
| 729 | Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1); |
---|
[27] | 730 | |
---|
[30] | 731 | } |
---|
| 732 | /* Replace the function for the latch */ |
---|
| 733 | Part_VertexSetFunction(vertex, newMvf); |
---|
| 734 | // printf("vertex %s changed % d\n",PartVertexReadName(vertex)); |
---|
[27] | 735 | } |
---|
| 736 | |
---|
[37] | 737 | /** Change the fsm and the network with a new partition and the new fsm **/ |
---|
| 738 | Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, |
---|
| 739 | (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, |
---|
| 740 | (void *) partition); |
---|
| 741 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t)); |
---|
[30] | 742 | mdd_t * init = Fsm_FsmComputeInitialStates(fsm); |
---|
[37] | 743 | mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, |
---|
[30] | 744 | 0,0, 0, |
---|
| 745 | 0, 0, Fsm_Rch_Default_c, |
---|
| 746 | 0,1, NIL(array_t), |
---|
| 747 | (verbose > 0), NIL(array_t)); |
---|
[37] | 748 | fsm->reachabilityInfo.initialStates = init; |
---|
| 749 | fsm->reachabilityInfo.reachableStates = reach; |
---|
[30] | 750 | if(verbose) |
---|
| 751 | Fsm_FsmReachabilityPrintResults(fsm,3, 0); |
---|
[27] | 752 | |
---|
[37] | 753 | Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, |
---|
| 754 | (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, |
---|
| 755 | (void *) fsm); |
---|
[27] | 756 | |
---|
[30] | 757 | return 0; /* normal exit */ |
---|
[27] | 758 | |
---|
[30] | 759 | usage: |
---|
| 760 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
| 761 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
| 762 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
| 763 | return 1; /* error exit */ |
---|
[27] | 764 | |
---|
| 765 | } |
---|
| 766 | |
---|
| 767 | |
---|