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

Last change on this file since 103 was 101, checked in by syed, 14 years ago

final
File size: 34.9 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);
67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv);
68static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int argc, char ** argv);
69
70
71/**AutomaticEnd***************************************************************/
72
73
74/*---------------------------------------------------------------------------*/
75/* Definition of exported functions */
76/*---------------------------------------------------------------------------*/
77
78/**Function********************************************************************
79
80 Synopsis [Initializes the test package.]
81
82 SideEffects []
83
84 SeeAlso [Debug_End]
85
86******************************************************************************/
87void
88Debug_Init(void)
89{
90 /*
91 * Add a command to the global command table. By using the leading
92 * underscore, the command will be listed under "help -a" but not "help".
93 */
94 Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
95 Cmd_CommandAdd("_transition", CommandTransition, 1);
96 Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0);
97 Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1);
98 Cmd_CommandAdd("_cexbdd", CommandBuildCexBdd, 0);
99 Cmd_CommandAdd("print_network_cnf", CommandGenerateNetworkCNF, 0);
100
101}
102
103
104/**Function********************************************************************
105
106 Synopsis [Ends the test package.]
107
108 SideEffects []
109
110 SeeAlso [Debug_Init]
111
112******************************************************************************/
113void
114Debug_End(void)
115{
116 /*
117 * For example, free any global memory (if any) which the test package is
118 * responsible for.
119 */
120}
121
122
123/*---------------------------------------------------------------------------*/
124/* Definition of internal functions */
125/*---------------------------------------------------------------------------*/
126
127
128/*---------------------------------------------------------------------------*/
129/* Definition of static functions */
130/*---------------------------------------------------------------------------*/
131
132
133static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv)
134{
135 Ntk_Network_t * ntk;
136 int c,verbose = 0;
137 array_t * excludes = NIL(array_t);
138 Dbg_Abnormal_t * abnormal;
139 ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
140 char * subs;
141 if (ntk == NIL(Ntk_Network_t)) {
142 (void) fprintf(vis_stdout, "** abn error: No network\n");
143 return 1;
144 }
145 while ((c = util_getopt(argc, argv, "vhs:")) != EOF) {
146 switch(c) {
147 case 'h':
148 goto usage;
149 case 'v':
150 verbose = 1;
151 break;
152 case 's':
153 subs = util_strsav(util_optarg);
154 excludes = array_alloc(char*,0);
155 array_insert_last(char*,excludes,subs);
156 break;
157 default :
158 goto usage;
159 }
160 }
161 abnormal = Dbg_DebugAbnormalAlloc(ntk);
162 abnormal->verbose = verbose;
163 printf("SUBS %s \n",subs);
164 Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes);
165 printf("\t # Abnormal predicate created %d\n", array_n(abnormal->abnormal));
166 return 0;
167 usage :
168 (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n");
169 (void) fprintf(vis_stderr, " -h \tprint the command usage\n");
170 (void) fprintf(vis_stderr, " -v \t verbosity\n");
171 (void) fprintf(vis_stderr, " -s <subsystemName> \texclude the abnormal predicate\
172 for this subssytem\n");
173 return 1;
174}
175
176/**Function********************************************************************
177
178 Synopsis [Implements the _sat_debug command.]
179
180 CommandName [_sat_debug]
181
182 CommandSynopsis [locate faulty candidates]
183
184 CommandArguments [\[-h\] \[-v\]]
185
186 CommandDescription [This command compute the fault candidates of a given
187 properties.<p>
188
189 Command options:<p>
190
191 <dl>
192 <dt> -h
193 <dd> Print the command usage.
194 </dl>
195
196 <dt> -v
197 <dd> Verbose mode.
198 </dl>
199 ]
200
201 SideEffects []
202
203******************************************************************************/
204static int
205CommandSatDebug(
206Hrc_Manager_t ** hmgr,
207int argc,
208char ** argv){
209int c,i;
210int verbose = 0; /* default value */
211BmcOption_t * options = BmcOptionAlloc();
212Ntk_Network_t * network;
213bAig_Manager_t * manager;
214array_t * formulaArray;
215array_t * LTLformulaArray;
216array_t * faultNodes = array_alloc(Ntk_Node_t*,0);
217
218/*
219 * Parse command line options.
220 */
221if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
222 return 1;
223}
224
225
226
227if (verbose) {
228 (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
229}
230/*
231 * Read the network
232 */
233network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
234if (network == NIL(Ntk_Network_t)) {
235 (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
236 BmcOptionFree(options);
237 return 1;
238}
239manager = Ntk_NetworkReadMAigManager(network);
240if (manager == NIL(mAig_Manager_t)) {
241 (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
242 BmcOptionFree(options);
243 return 1;
244}
245
246Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
247if(abn == NIL(Dbg_Abnormal_t)){
248 (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
249 return 1;
250}
251if(verbose)
252 printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
253
254
255formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
256if (formulaArray == NIL(array_t)) {
257 (void) fprintf(vis_stderr,
258 "** bmc error: error in parsing CTL* Fromula from file\n");
259 BmcOptionFree(options);
260 return 1;
261}
262if (array_n(formulaArray) == 0) {
263 (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
264 BmcOptionFree(options);
265 Ctlsp_FormulaArrayFree(formulaArray);
266 return 1;
267}
268LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
269Ctlsp_FormulaArrayFree(formulaArray);
270if (LTLformulaArray == NIL(array_t)){
271 (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
272 BmcOptionFree(options);
273 return 1;
274}
275Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
276
277
278 /*
279 Compute the cone of influence
280 here : a list of state variables (latches)
281 TODO refine to COI of the property
282 */
283 st_table *CoiTable = generateAllLatches(network);
284 /*
285 Generate clauses for each time frame. This is the old way of generating
286 clauses in BMC.
287 */
288 if(verbose)
289 {
290 (void) fprintf(vis_stdout, "------ COI ----\n");
291 printLatch(CoiTable);
292 (void) fprintf(vis_stdout, "--------------------------\n");
293 }
294 BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable);
295
296
297 //Generate ltl CNF
298 // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
299 // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
300 // cf. BmcLtlVerifyGeneralLtl
301 Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
302 fprintf(vis_stdout, "\n");
303 int k = options->maxK;
304 int l;
305 // return the clause number
306 int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); printf("LTL %d \n",noLoopIndex);
307
308
309 array_t *objClause = NIL(array_t);
310 objClause = array_alloc(int, 0);
311 array_insert_last(int, objClause, noLoopIndex);
312 BmcCnfInsertClause(cnfClauses, objClause);
313 array_free(objClause);
314
315 //Add Abnormal
316 st_table * nodeToMvfAigTable = NIL(st_table);
317 nodeToMvfAigTable =
318 (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
319 assert(nodeToMvfAigTable != NIL(st_table));
320
321 Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
322
323 //loop abnormal
324 int aIndex;
325 Ntk_Node_t * abnNode;
326 Dbg_ForEachAbnormal(abn,aIndex,abnNode){
327 char * nodeName = Ntk_NodeReadName(abnNode);
328 //set abnormal for each step
329 array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex);
330 int cnfIndex;
331 int step;
332 bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
333 array_t * cnfVal = array_alloc(int,0);
334 arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
335 int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses);
336 array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
337 array_insert_last(int,cnfVal,abnIndex);
338 FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
339 BmcWriteClauses(manager, cnfFile, cnfClauses, options);
340 fclose(cnfFile);
341 printf("AINDEX %d\n",aIndex);
342 if(aIndex == 0)
343 {
344 FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0);
345 BmcWriteClauses(manager, cnfFile, cnfClauses, options);
346 fclose(cnfFile);
347
348 }
349 }//end for each step
350
351 //SAT procedure
352 //assig assig input from cex
353 //TODO build cex correctly
354 int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel);
355 // Build set of FaultCandidates
356 if (res == SAT_SAT)
357 {
358 char * realNodeName = util_strsav(nodeName);
359 realNodeName[strlen(nodeName)-3] = '\0';
360 printf("Real = %s\n", realNodeName);
361 Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName);
362 array_insert_last(Ntk_Node_t*,faultNodes,realNode);
363 }
364
365 arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
366 int abnIndex = array_fetch(int,cnfVal,step);
367 array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
368 }
369 }
370
371 if(verbose)
372 (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
373 latches \n",cnfClauses->noOfClauses,st_count(CoiTable));
374
375
376 (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
377 array_n(faultNodes));
378 (void) fprintf(vis_stdout,"gates : \n");
379
380
381 printNodeArray(faultNodes);
382
383
384Ctlsp_FormulaArrayFree(LTLformulaArray);
385BmcCnfClausesFree(cnfClauses);
386BmcOptionFree(options);
387array_free(faultNodes);
388return 0;
389}
390
391/**Function********************************************************************
392
393 Synopsis [Implements the generate_network_cnf.]
394
395 CommandName [generate_network_cnf]
396
397 CommandSynopsis [generate a CNF view of the network]
398
399 CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ]
400
401 CommandDescription [This command generate a CNF of the network in DMACS form.
402 The network may be unroll within k steps.
403 <p>
404
405 Command options:<p>
406
407 <dl>
408 <dt> -h
409 <dd> Print the command usage.
410 </dl>
411
412 <dt> -v
413 <dd> Verbose mode.
414 </dl>
415
416 <dt> -k
417 <dd> number of steps (default 1).
418 </dl>
419 ]
420
421 SideEffects []
422
423******************************************************************************/
424
425static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv)
426{
427 BmcOption_t *options = BmcOptionAlloc();
428 int c;
429 unsigned int i;
430 Ntk_Network_t * network;
431 bAig_Manager_t * manager;
432 char * outName = NIL(char);
433 FILE *cnfFile;
434 if (!options){
435 return 1;
436 }
437 options->dbgOut = 0;
438 /*
439 * Parse command line options.
440 */
441 util_getopt_reset();
442 while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
443 switch(c) {
444 case 'h':
445 goto usage;
446 case 'k':
447 options->maxK = atoi(util_optarg);
448 break;
449 case 'v':
450 for (i = 0; i < strlen(util_optarg); i++) {
451 if (!isdigit((int)util_optarg[i])) {
452 goto usage;
453 }
454 }
455 options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
456 break;
457 default:
458 goto usage;
459 }
460 }
461 if (argc - util_optind != 0)
462 {
463 outName = util_strsav(argv[util_optind]);
464 /* create SAT Solver input file */
465 options->cnfFileName= outName;
466 options->satInFile = options->cnfFileName;
467 cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
468 }
469
470
471/*
472 * Read the network
473 */
474network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
475if (network == NIL(Ntk_Network_t)) {
476 (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
477 BmcOptionFree(options);
478 return 1;
479}
480manager = Ntk_NetworkReadMAigManager(network);
481if (manager == NIL(mAig_Manager_t)) {
482 (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
483 BmcOptionFree(options);
484 return 1;
485}
486
487 /*
488 Compute the cone of influence
489 here : a list of state variables (latches)
490 */
491st_table *CoiTable = generateAllLatches(network);
492
493if(options->verbosityLevel)
494{
495 (void) fprintf(vis_stdout, "------ COI ----\n");
496 printLatch(CoiTable);
497 (void) fprintf(vis_stdout, "--------------------------\n");
498}
499BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable);
500 if(outName != NIL(char))
501 {
502 BmcWriteClauses(manager, cnfFile, cnfClauses, options);
503 fclose(cnfFile);
504 }
505 else
506 BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
507
508if(options->verbosityLevel)
509{
510 (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
511 (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
512 st_count(CoiTable));
513}
514
515BmcOptionFree(options);
516 return 0;
517 usage:
518 (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
519 (void) fprintf(vis_stderr, " -h \tprint the command usage\n");
520 (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n");
521 (void) fprintf(vis_stderr, " -v <verbosity_level>\n");
522 (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
523 (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n");
524 (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n");
525 (void) fprintf(vis_stderr, " <cnf_file> The output file containing CNF of the network.\n");
526
527 BmcOptionFree(options);
528 return 1;
529}
530
531/**Function********************************************************************
532
533 Synopsis [Implements the _Debug_test command.]
534
535 CommandName [_Debug_test]
536
537 CommandSynopsis [template for implementing commands]
538
539 CommandArguments [\[-h\] \[-v\]]
540
541 CommandDescription [This command does nothing useful. It merely serves as a
542 template for the implementation of new commands.<p>
543
544 Command options:<p>
545
546 <dl>
547 <dt> -h
548 <dd> Print the command usage.
549 </dl>
550
551 <dt> -v
552 <dd> Verbose mode.
553 </dl>
554 ]
555
556 SideEffects []
557
558******************************************************************************/
559static int
560CommandDebug(
561 Hrc_Manager_t ** hmgr,
562 int argc,
563 char ** argv)
564{
565 int c;
566 int verbose = 0; /* default value */
567
568 /*
569 * Parse command line options.
570 */
571 util_getopt_reset();
572 while ((c = util_getopt(argc, argv, "vh")) != EOF) {
573 switch(c) {
574 case 'v':
575 verbose = 1;
576 break;
577 case 'h':
578 goto usage;
579 default:
580 goto usage;
581 }
582 }
583
584 if (verbose) {
585 (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
586 }
587
588 Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
589 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
590 printf("** DEBUG MODE **\n");
591 Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
592 printf("model : %s\n", Hrc_NodeReadModelName(n));
593
594 mdd_t * safe = getSafe(fsm);
595 mdd_t * forbid = getForbidden(fsm);
596 mdd_t * reach = getReach(fsm);
597
598 if(safe == NIL(mdd_t))
599 {
600 printf("call command set_safe before\n");
601 return 1;
602 }
603 if(forbid == NIL(mdd_t))
604 {
605 printf("call command set_forbidden before\n");
606 return 1;
607 }
608
609 FILE* oFile;
610 oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
611 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
612// mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
613
614 mdd_t * EFState = mdd_and(reach,safe,1,1);
615// mdd_t * errorState = mdd_and(reach,forbid,1,1);
616
617 mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
618 array_t *careStatesArray = array_alloc(mdd_t *, 0);
619 array_insert(mdd_t *, careStatesArray, 0,mddOne);
620
621 mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
622 EFState,
623 fsm->fairnessInfo.states,
624 careStatesArray,
625 0,
626 McDcLevelNone_c);
627
628 mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
629 mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
630
631 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
632 EXEFState,
633 fsm->fairnessInfo.states,
634 careStatesArray,
635 0,
636 McDcLevelNone_c);
637 mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
638 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
639 mdd_t * andState = mdd_xor(EXEFState2,EXEFState);
640 mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
641 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
642 andState,
643 fsm->fairnessInfo.states,
644 careStatesArray,
645 0,
646 McDcLevelNone_c);
647 EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
648 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
649 andState = mdd_xor(EXEFState2,andState);
650 mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
651 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
652 andState,
653 fsm->fairnessInfo.states,
654 careStatesArray,
655 0,
656 McDcLevelNone_c);
657 EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
658 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
659 andState = mdd_xor(EXEFState2,andState);
660 mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
661
662
663
664 //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
665 //mdd_GetState_Values(mddManager , EFState, stdout);
666 fclose(oFile);
667
668
669
670
671
672 return 0; /* normal exit */
673
674 usage:
675 (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
676 (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
677 (void) fprintf(vis_stderr, " -v\t\tverbose\n");
678 return 1; /* error exit */
679}
680
681/******************************************/
682/* function that build a bdd for the */
683/* simple example : */
684/* (state = 0) -> !(state = 1) */
685/******************************************/
686mdd_t * buildDummyBdd(mdd_manager *mddManager)
687{
688/** state0 = 0 **/
689 mdd_t * s0 = mdd_eq_c(mddManager,0, 0);
690 mdd_t * s1 = mdd_eq_c(mddManager,2, 0);
691 mdd_t * state0 = mdd_one(mddManager);
692 state0 = mdd_and(s0,s1,1,1);
693/** state1 = 1 **/
694 mdd_t * ns0 = mdd_eq_c(mddManager,1, 1);
695 mdd_t * ns1 = mdd_eq_c(mddManager,3, 0);
696 mdd_t * state1 = mdd_one(mddManager);
697 state1 = mdd_and(ns0,ns1,1,1);
698/** state = 0) -> !(state = 1) **/
699 mdd_t * rel = mdd_one(mddManager);
700 rel = mdd_or(state0,state1,0,0);
701
702 return rel;
703}
704mdd_t * buildDummy2(mdd_manager * mddManager)
705{
706 mdd_t * rel = NIL(mdd_t);
707 mdd_t * state0 = mdd_one(mddManager);
708 mdd_t * state2 = mdd_one(mddManager);
709 mdd_t * state3 = mdd_one(mddManager);
710 // state0 = s0
711 mdd_t * s0 = mdd_eq_c(mddManager,0, 0);
712 mdd_t * s1 = mdd_eq_c(mddManager,2, 0);
713 state0 = mdd_and(s0,s1,1,1);
714 // state2 = s2
715 s0 = mdd_eq_c(mddManager,0, 0);
716 s1 = mdd_eq_c(mddManager,2, 1);
717 state2 = mdd_and(s0,s1,1,1);
718 // state3 = s3
719 s0 = mdd_eq_c(mddManager,0, 1);
720 s1 = mdd_eq_c(mddManager,2, 1);
721 state3 = mdd_and(s0,s1,1,1);
722// Build transition relation
723
724 array_t * mvarVal = array_alloc(int,0);
725 array_insert_last(int, mvarVal,2);
726 array_t * val = array_alloc(int,0);
727 array_t * mvarName = array_alloc(char*,0);
728 array_insert_last(char*, mvarName,"S1");
729 int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
730 array_insert(char*, mvarName,0,"I");
731 int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
732 array_insert_last(int, val,1);
733 mdd_t * e1 = mdd_literal(mddManager, e1Id,val);
734 mdd_t * e0 = mdd_literal(mddManager, e0Id,val);
735 mdd_t * tmp2 = mdd_and(e1,e0,0,0);
736mdd_t * ne2_1 = mdd_or(e1,tmp2,1,1);
737mdd_t * ne2_0 = mdd_and(e1,e0,0,1);
738
739array_insert(char*, mvarName,0,"Next_SI");
740int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
741Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2);
742Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1);
743Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0);
744mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id);
745
746//bdd_print(relation);
747mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout);
748 //bdd_ite
749 return rel;
750
751}
752
753/**Function********************************************************************
754
755 Synopsis [Implements the transtion command.]
756
757 CommandName [_transition]
758
759 CommandSynopsis [compute new transition relation]
760
761 CommandArguments [\[-h\] \[-v\]]
762
763 CommandDescription [This command create a new transition relation that is a
764 and of the Bdd of the old one and another bdd.
765 <p>
766
767 Command options:<p>
768
769 <dl>
770 <dt> -h
771 <dd> Print the command usage.
772 </dl>
773
774 <dt> -v
775 <dd> Verbose mode.
776 </dl>
777 ]
778
779 SideEffects [Change the fsm]
780
781******************************************************************************/
782
783static int
784CommandTransition (Hrc_Manager_t ** hmgr,
785 int argc, char ** argv){
786int c;
787int verbose = 0; /* default value */
788
789/*
790 * Parse command line options.
791 */
792util_getopt_reset();
793while ((c = util_getopt(argc, argv, "vh")) != EOF) {
794 switch(c) {
795 case 'v':
796 verbose = 1;
797 break;
798 case 'h':
799 goto usage;
800 default:
801 goto usage;
802 }
803}
804
805if (verbose) {
806 (void) fprintf(vis_stdout, "The _transition is under construction.\n");
807}
808
809Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
810Ntk_Network_t *network = NIL(Ntk_Network_t);
811mdd_manager *mddManager;
812mdd_t *rel = NIL(mdd_t);
813graph_t *partition;
814int i;
815/******************/
816network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
817if(network == NIL(Ntk_Network_t))
818 return 1;
819fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
820if(fsm == NIL(Fsm_Fsm_t))
821 return 1;
822mddManager = Fsm_FsmReadMddManager(fsm);
823
824
825
826/********** Build cex ***********/
827/* Here add the function */
828/* that build the Bdd to and */
829/* with the transtion relation */
830/***********************************/
831rel = buildDummyBdd(mddManager);
832if(rel == NIL(mdd_t))
833{
834 fprintf(vis_stdout,"Problem when building the new relation bdd\n");
835 return 1;
836}
837if (verbose)
838 mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
839
840
841/** Get image_info **/
842Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
843partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
844/**** The complete transtion relation ****/
845// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
846/*****************************************/
847/*** For each latch rebuild the transition function ***/
848/*** mvf table is composed of mdd for each possible ***/
849/*** value of the latch ***/
850ImgFunctionData_t * functionData = &(imageInfo->functionData);
851array_t *roots = functionData->roots;
852array_t *rangeVarMddIdArray = functionData->rangeVars;
853char * nodeName;
854arrayForEachItem(char *, roots, i, nodeName) {
855
856 /* The new relation */
857 vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
858 Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
859 int mddId = array_fetch(int, rangeVarMddIdArray, i);
860 mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
861 if(verbose){
862 int x;
863 mdd_t * comp;
864
865 Mvf_FunctionForEachComponent( mvf, x, comp){
866 printf("%s,%d mdd %d ",nodeName,x,mddId);
867 mdd_FunctionPrintMain (mddManager ,comp,"MVF",vis_stdout);
868 }
869 }
870
871 mdd_t * n_relation = mdd_and(relation,rel,1,1);
872 /* Build for each possible value */
873 int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
874 int v ;
875 Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
876 for(v = 0; v<nbValue;v++)
877 {
878 mdd_t * n_s1 = mdd_eq_c(mddManager,mddId, v);
879 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
880 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
881 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
882
883
884 }
885 /* Replace the function for the latch */
886 Part_VertexSetFunction(vertex, newMvf);
887// printf("vertex %s changed % d\n",PartVertexReadName(vertex));
888}
889
890/** Change the fsm and the network with a new partition and the new fsm **/
891Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
892 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
893 (void *) partition);
894fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
895mdd_t * init = Fsm_FsmComputeInitialStates(fsm);
896mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
897 0,0, 0,
898 0, 0, Fsm_Rch_Default_c,
899 0,1, NIL(array_t),
900 (verbose > 0), NIL(array_t));
901fsm->reachabilityInfo.initialStates = init;
902fsm->reachabilityInfo.reachableStates = reach;
903if(verbose)
904 Fsm_FsmReachabilityPrintResults(fsm,3, 0);
905
906Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
907 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
908 (void *) fsm);
909
910return 0; /* normal exit */
911
912usage:
913(void) fprintf(vis_stderr, "usage: _transition [-h] [-v]\n");
914(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
915(void) fprintf(vis_stderr, " -v\t\tverbose\n");
916return 1; /* error exit */
917
918}
919
920static int
921CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
922 int argc, char ** argv){
923int c;
924int verbose = 0; /* default value */
925
926/*
927 * Parse command line options.
928 */
929util_getopt_reset();
930while ((c = util_getopt(argc, argv, "vh")) != EOF) {
931 switch(c) {
932 case 'v':
933 verbose = 1;
934 break;
935 case 'h':
936 goto usage;
937 default:
938 goto usage;
939 }
940}
941
942if (verbose) {
943 (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
944}
945
946Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
947Ntk_Network_t *network = NIL(Ntk_Network_t);
948mdd_manager *mddManager;
949Hrc_Manager_t *hmgrCex = NIL(Hrc_Manager_t);
950Fsm_Fsm_t *fsmCex = NIL(Fsm_Fsm_t);
951Ntk_Network_t *networkCex = NIL(Ntk_Network_t);
952mdd_t *rel = NIL(mdd_t);
953int i;
954/******************/
955network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
956if(network == NIL(Ntk_Network_t))
957 return 1;
958fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
959if(fsm == NIL(Fsm_Fsm_t))
960 return 1;
961mddManager = Fsm_FsmReadMddManager(fsm);
962
963mdd_t * initOrig = Fsm_FsmComputeInitialStates(fsm);
964mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout);
965
966/********** Build cex ***********/
967/* Here add the function */
968/* that build the Bdd to and */
969/* with the transtion relation */
970/***********************************/
971//rel = buildDummyBdd(mddManager);
972 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
973 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
974Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2);
975 mdd_t * s0 = mdd_eq_c(mddManager,20, 0);
976 mdd_t * s1 = mdd_eq_c(mddManager,22, 0);
977 mdd_t * state0 = mdd_one(mddManager);
978 mdd_t * state1 = mdd_one(mddManager);
979 state0 = mdd_and(s0,s1,1,1);
980 mdd_t * state12 = mdd_and(s0,s1,0,1);
981 state1 = mdd_not(state0);
982 array_insert(mdd_t *, newMvf, 1, state0);
983 array_insert(mdd_t *, newMvf, 0, state1);
984 mdd_t * ns1 = mdd_eq_c(mddManager,17, 1);
985Mvf_Function_t * newNS = Mvf_FunctionAlloc( mddManager,2);
986Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1));
987Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0));
988
989mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout);
990vertex_t * vert;
991vert = Part_PartitionFindVertexByName(part,"cex.s2");
992Part_VertexSetFunction(vert, newNS);
993
994vert = Part_PartitionFindVertexByName(part,"cex.s3");
995 mdd_t * ns1S3 = mdd_eq_c(mddManager,14, 1);
996Mvf_Function_t * newS3 = Mvf_FunctionAlloc( mddManager,2);
997Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1));
998Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0));
999Part_VertexSetFunction(vert, newS3);
1000
1001// Initial state
1002mdd_t * ns1Init = mdd_eq_c(mddManager,3, 1);
1003
1004Mvf_Function_t * newNSInit = Mvf_FunctionAlloc(mddManager,2);
1005Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1));
1006Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0));
1007mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout);
1008Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"),
1009newNSInit);
1010
1011
1012
1013
1014 /** Change the fsm and the network with a new partition and the new fsm **/
1015Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
1016 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1017 (void *) part);
1018fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part);
1019
1020
1021mdd_t * init = Fsm_FsmComputeInitialStates(fsm);
1022//mdd_t * n_init = Mvf_MddComposeWithFunction(init, 17 , newMvf);
1023mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
1024 0,0, 0,
1025 0, 0, Fsm_Rch_Default_c,
1026 0,1, NIL(array_t),
1027 (verbose > 0), NIL(array_t));
1028fsm->reachabilityInfo.initialStates = init;
1029fsm->reachabilityInfo.reachableStates = reach;
1030
1031
1032
1033Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
1034 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1035 (void *) fsm);
1036
1037Img_ImageInfoUpdateVariables(fsm->imageInfo,
1038 fsm->partition,
1039 fsm->fsmData.presentStateVars,
1040 fsm->fsmData.inputVars,
1041 fsm->fsmData.presentStateCube,
1042 fsm->fsmData.inputCube);
1043Fsm_FsmReachabilityPrintResults(fsm,3, 0);
1044//
1045//
1046mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
1047
1048/*
1049// Read_blif_mv
1050 FILE *fpC;
1051 fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
1052 boolean isCanonicalC = 0;
1053 boolean isIncrementalC = 0;
1054 boolean isVerboseC = 0;
1055 hmgrCex = Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
1056
1057//flatten_hier
1058 lsList varNameList = (lsList) NULL;
1059 Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
1060 networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
1061 Ntk_NetworkSetMddManager(networkCex, mddManager);
1062//static_order
1063 static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
1064 static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
1065 static Ord_OrderType suppliedOrderType = Ord_Unassigned_c;
1066 static Ord_OrderType generatedOrderType = Ord_InputAndLatch_c;
1067 static boolean nsAfterSupport = FALSE;
1068 lsList suppliedNodeList = (lsList) NULL;
1069
1070 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport,
1071 generatedOrderType, suppliedOrderType,
1072 suppliedNodeList, isVerboseC);
1073 //build_partition_mdd
1074 char * modelName = Hrc_NodeReadModelName(currentNode);
1075 static Part_PartitionMethod method = Part_Default_c;
1076 graph_t *partition;
1077 lsList nodeList = lsCreate();
1078 boolean inTermsOfLeaves = FALSE;
1079 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
1080 (lsList)0, NIL(mdd_t), method, nodeList,
1081 inTermsOfLeaves, isVerboseC, 0);
1082// PartPartitionPrint(vis_stdout, partition);
1083 printf(" Cex loaded \n");
1084fsmCex = Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
1085array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
1086array_t * nextIdsCex = Fsm_FsmReadNextStateVars(fsmCex);
1087printf("Next Names\n");
1088printStringArray(nextNamesCex);
1089printf("Next Ids\n");
1090printIntArray(nextIdsCex);
1091
1092mddManager = Fsm_FsmReadMddManager(fsm);
1093mdd_manager * mddManagerCex = Fsm_FsmReadMddManager(fsmCex);
1094
1095array_t *mvar_list, *bvar_list;
1096mvar_list = mdd_ret_mvar_list(mddManager);
1097bvar_list = mdd_ret_bvar_list(mddManager);
1098printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
1099printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
1100 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
1101// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
1102graph_t * part = Fsm_FsmReadPartition(fsm);
1103printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
1104*/
1105return 0; /* normal exit */
1106
1107usage:
1108(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1109(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
1110(void) fprintf(vis_stderr, " -v\t\tverbose\n");
1111return 1; /* error exit */
1112
1113}
1114
1115
Note: See TracBrowser for help on using the repository browser.