source: vis_dev/vis-2.3/src/debug/debug.c@ 40

Last change on this file since 40 was 40, checked in by cecile, 15 years ago

abnormal structure in network
File size: 22.8 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [debug.c]
4
5 PackageName [debug]
6
7 Synopsis [Debug package initialization, ending, and the command debug]
8
9 Author [Cecile B.]
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"
33#include "imgInt.h"
34#include "partInt.h"
35static 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
63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
65static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv);
66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv);
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******************************************************************************/
85void
86Debug_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 */
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);
96
97}
98
99
100/**Function********************************************************************
101
102 Synopsis [Ends the test package.]
103
104 SideEffects []
105
106 SeeAlso [Debug_Init]
107
108******************************************************************************/
109void
110Debug_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
128
129static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv)
130{
131 Ntk_Network_t * ntk;
132 int c,verbose;
133 Dbg_Abnormal_t * abnormal;
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 }
139 while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
140 switch(c) {
141 case 'v':
142 verbose = 1;
143 break;
144 }
145 }
146 abnormal = Dbg_DebugAbnormalAlloc(ntk);
147 abnormal->verbose = verbose;
148 Dbg_AddAbnormalPredicatetoNetwork(abnormal);
149}
150/**Function********************************************************************
151
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******************************************************************************/
178static int
179checkIndex(
180 int index,
181 BmcCnfClauses_t *cnfClauses)
182{
183 int rtnValue = -1; /* it is not TRUE or FALSE*/
184
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}
199
200
201static int
202CommandSatDebug(
203Hrc_Manager_t ** hmgr,
204int argc,
205char ** argv){
206int c,i;
207int verbose = 0; /* default value */
208BmcOption_t *options = BmcOptionAlloc();
209Ntk_Network_t * network;
210bAig_Manager_t *manager;
211array_t *formulaArray;
212array_t *LTLformulaArray;
213char *ltlFileName = NIL(char);
214
215/*
216 * Parse command line options.
217 */
218util_getopt_reset();
219while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
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);
245 break;
246 case 'p':
247 ltlFileName = util_strsav(util_optarg);
248 break;
249
250 default:
251 goto usage;
252 }
253}
254printf("MAX K %d", options->maxK);
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
260if (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 */
272options->satOutFile = BmcCreateTmpFile();
273if (options->satOutFile == NIL(char)){
274 BmcOptionFree(options);
275 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
276 return 1;
277}
278
279options->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 }
298
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 }
311Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
312printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
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
352 /*
353 Compute the cone of influence
354 here : a list of state variables (latches)
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 */
386 Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
387 fprintf(vis_stdout, "\n");
388 BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
389 cnfClauses, nodeToMvfAigTable, CoiTable);
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
398 int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
399
400 int leftValue = checkIndex(noLoopIndex, cnfClauses);
401 printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
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);
407
408
409//TODO Add abnormal formula
410
411
412
413
414
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
419 Ctlsp_FormulaArrayFree(LTLformulaArray);
420 BmcWriteClauses(manager, cnfFile, cnfClauses, options);
421fclose(cnfFile);
422BmcCnfClausesFree(cnfClauses);
423BmcOptionFree(options);
424return 0;
425 usage:
426 (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
427 minimum length] [-o cnf_file] [-p ltl_file]\n");
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");
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");
434 return 1; /* error exit */
435
436}
437/**Function********************************************************************
438
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******************************************************************************/
465static int
466CommandDebug(
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
587/******************************************/
588/* function that build a bdd for the */
589/* simple example : */
590/* (state = 0) -> !(state = 1) */
591/******************************************/
592mdd_t * buildDummyBdd(mdd_manager *mddManager)
593{
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}
610
611
612/**Function********************************************************************
613
614 Synopsis [Implements the transtion command.]
615
616 CommandName [_transition]
617
618 CommandSynopsis [compute new transition relation]
619
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>
625
626 Command options:<p>
627
628 <dl>
629 <dt> -h
630 <dd> Print the command usage.
631 </dl>
632
633 <dt> -v
634 <dd> Verbose mode.
635 </dl>
636 ]
637
638 SideEffects [Change the fsm]
639
640******************************************************************************/
641
642static int
643CommandTransition (Hrc_Manager_t ** hmgr,
644 int argc, char ** argv){
645int c;
646int verbose = 0; /* default value */
647
648/*
649 * Parse command line options.
650 */
651util_getopt_reset();
652while ((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;
661 }
662}
663
664if (verbose) {
665 (void) fprintf(vis_stdout, "The _transition is under construction.\n");
666}
667
668Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
669Ntk_Network_t *network = NIL(Ntk_Network_t);
670mdd_manager *mddManager;
671mdd_t *rel = NIL(mdd_t);
672graph_t *partition;
673int i;
674/******************/
675network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
676if(network == NIL(Ntk_Network_t))
677 return 1;
678fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
679if(fsm == NIL(Fsm_Fsm_t))
680 return 1;
681mddManager = Fsm_FsmReadMddManager(fsm);
682
683
684
685/********** Build cex ***********/
686/* Here add the function */
687/* that build the Bdd to and */
688/* with the transtion relation */
689/***********************************/
690rel = buildDummyBdd(mddManager);
691if(rel == NIL(mdd_t))
692{
693 fprintf(vis_stdout,"Problem when building the new relation bdd");
694 return 1;
695}
696if (verbose)
697 mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
698
699
700/** Get image_info **/
701Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
702partition = 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 ***/
709ImgFunctionData_t * functionData = &(imageInfo->functionData);
710array_t *roots = functionData->roots;
711array_t *rangeVarMddIdArray = functionData->rangeVars;
712char * nodeName;
713arrayForEachItem(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);
730
731 }
732 /* Replace the function for the latch */
733 Part_VertexSetFunction(vertex, newMvf);
734// printf("vertex %s changed % d\n",PartVertexReadName(vertex));
735}
736
737/** Change the fsm and the network with a new partition and the new fsm **/
738Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
739 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
740 (void *) partition);
741fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
742mdd_t * init = Fsm_FsmComputeInitialStates(fsm);
743mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
744 0,0, 0,
745 0, 0, Fsm_Rch_Default_c,
746 0,1, NIL(array_t),
747 (verbose > 0), NIL(array_t));
748fsm->reachabilityInfo.initialStates = init;
749fsm->reachabilityInfo.reachableStates = reach;
750if(verbose)
751 Fsm_FsmReachabilityPrintResults(fsm,3, 0);
752
753Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
754 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
755 (void *) fsm);
756
757return 0; /* normal exit */
758
759usage:
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");
763return 1; /* error exit */
764
765}
766
767
Note: See TracBrowser for help on using the repository browser.