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

Last change on this file since 99 was 98, checked in by cecile, 14 years ago

add part of cex
File size: 38.4 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 %d \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("%d mdd %d ",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);
972array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
973array_t * nextIds = Fsm_FsmReadNextStateVars(fsm);
974array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
975printf("Next Names\n");
976printStringArray(nextNames);
977printf("Next Ids\n");
978printIntArray(nextIds);
979printf("Current Ids\n");
980printIntArray(currentIds);
981Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
982 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
983
984lsGen gen;
985vertex_t *vertexPtr;
986
987
988//foreach_vertex(part, gen, vertexPtr) {
989// if (PartVertexReadName(vertexPtr) != NIL(char)) {
990// (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr));
991// }
992//}
993vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
994Mvf_Function_t* vertexFunction = PartVertexReadFunction(v_s2);
995 if (vertexFunction != NIL(Mvf_Function_t)) {
996printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
997}
998else
999 printf("no fonction");
1000
1001Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2);
1002 mdd_t * s0 = mdd_eq_c(mddManager,20, 0);
1003 mdd_t * s1 = mdd_eq_c(mddManager,22, 0);
1004 mdd_t * state0 = mdd_one(mddManager);
1005 mdd_t * state1 = mdd_one(mddManager);
1006 state0 = mdd_and(s0,s1,1,1);
1007 state1 = mdd_not(state0);
1008 array_insert(mdd_t *, newMvf, 1, state0);
1009 array_insert(mdd_t *, newMvf, 0, state1);
1010Mvf_Function_t * newMvf2 = Mvf_FunctionAlloc( mddManager,2);
1011 mdd_t * s0_2 = mdd_eq_c(mddManager,20, 1);
1012 mdd_t * s1_2 = mdd_eq_c(mddManager,22, 0);
1013 mdd_t * state0_2 = mdd_one(mddManager);
1014 mdd_t * state1_2 = mdd_one(mddManager);
1015 state0_2 = mdd_and(s0_2,s1_2,1,1);
1016 state1_2 = mdd_not(state0_2);
1017 array_insert(mdd_t *, newMvf2, 1, state0_2);
1018 array_insert(mdd_t *, newMvf2, 0, state1_2);
1019FILE * file = fopen("mvf.txt","w");
1020foreach_vertex(part, gen, vertexPtr) {
1021fprintf(file,"********* (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) );
1022 Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr);
1023 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
1024 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file);
1025 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
1026 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file);
1027
1028 if(Part_VertexReadMddId(vertexPtr) == 17)
1029 {
1030 Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2);
1031
1032 mdd_t * new0 = Mvf_FunctionReadComponent(fun,0);
1033 new0 = mdd_and(new0,state1,1,1);
1034 mdd_t * new1 = Mvf_FunctionReadComponent(fun,1);
1035 new1 = mdd_and(new1,state0,1,1);
1036 array_insert(mdd_t *, newMvf, 1, new1);
1037 array_insert(mdd_t *, newMvf, 0, new0);
1038 mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
1039 mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
1040 Part_VertexSetFunction(vertexPtr, newMvf);
1041 }
1042 else{
1043 Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf);
1044 Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf);
1045 //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2);
1046 mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0);
1047 mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
1048 mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1);
1049 mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
1050
1051 Part_VertexSetFunction(vertexPtr, newFun);
1052 Part_VertexSetFunction(vertexPtr, newFun1);
1053// Part_VertexSetFunction(vertexPtr, newFun2);
1054 }
1055}
1056fclose(file);
1057
1058
1059
1060
1061 array_t * psVars = fsm->fsmData.presentStateVars;
1062 int numLatches = array_n(psVars);
1063
1064
1065 for (i=0; i<numLatches; i++){
1066 int latchMddId = array_fetch(int, psVars, i);
1067 Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
1068 Ntk_Node_t *initNode = Ntk_LatchReadInitialInput(latch);
1069 vertex_t *initVertex = Part_PartitionFindVertexByName(part,
1070 Ntk_NodeReadName(initNode));
1071 Mvf_Function_t * fun = PartVertexReadFunction(initVertex);
1072 printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode),
1073 Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) );
1074
1075 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
1076 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout);
1077 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
1078 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout);
1079
1080
1081 }
1082
1083
1084 /** Change the fsm and the network with a new partition and the new fsm **/
1085Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
1086 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1087 (void *) part);
1088fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
1089mdd_t * init = Fsm_FsmComputeInitialStates(fsm);
1090//mdd_t * n_init = Mvf_MddComposeWithFunction(init, 17 , newMvf);
1091mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
1092 0,0, 0,
1093 0, 0, Fsm_Rch_Default_c,
1094 0,1, NIL(array_t),
1095 (verbose > 0), NIL(array_t));
1096//mdd_t * n_reach = Mvf_MddComposeWithFunction(reach, 17 , newMvf);
1097//fsm->reachabilityInfo.initialStates = n_init;
1098//fsm->reachabilityInfo.reachableStates = n_reach;
1099//
1100//
1101
1102Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
1103 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1104 (void *) fsm);
1105
1106Fsm_FsmReachabilityPrintResults(fsm,3, 0);
1107//
1108//
1109mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
1110
1111/*
1112// Read_blif_mv
1113 FILE *fpC;
1114 fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
1115 boolean isCanonicalC = 0;
1116 boolean isIncrementalC = 0;
1117 boolean isVerboseC = 0;
1118 hmgrCex = Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
1119
1120//flatten_hier
1121 lsList varNameList = (lsList) NULL;
1122 Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
1123 networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
1124 Ntk_NetworkSetMddManager(networkCex, mddManager);
1125//static_order
1126 static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
1127 static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
1128 static Ord_OrderType suppliedOrderType = Ord_Unassigned_c;
1129 static Ord_OrderType generatedOrderType = Ord_InputAndLatch_c;
1130 static boolean nsAfterSupport = FALSE;
1131 lsList suppliedNodeList = (lsList) NULL;
1132
1133 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport,
1134 generatedOrderType, suppliedOrderType,
1135 suppliedNodeList, isVerboseC);
1136 //build_partition_mdd
1137 char * modelName = Hrc_NodeReadModelName(currentNode);
1138 static Part_PartitionMethod method = Part_Default_c;
1139 graph_t *partition;
1140 lsList nodeList = lsCreate();
1141 boolean inTermsOfLeaves = FALSE;
1142 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
1143 (lsList)0, NIL(mdd_t), method, nodeList,
1144 inTermsOfLeaves, isVerboseC, 0);
1145// PartPartitionPrint(vis_stdout, partition);
1146 printf(" Cex loaded \n");
1147fsmCex = Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
1148array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
1149array_t * nextIdsCex = Fsm_FsmReadNextStateVars(fsmCex);
1150printf("Next Names\n");
1151printStringArray(nextNamesCex);
1152printf("Next Ids\n");
1153printIntArray(nextIdsCex);
1154
1155mddManager = Fsm_FsmReadMddManager(fsm);
1156mdd_manager * mddManagerCex = Fsm_FsmReadMddManager(fsmCex);
1157
1158array_t *mvar_list, *bvar_list;
1159mvar_list = mdd_ret_mvar_list(mddManager);
1160bvar_list = mdd_ret_bvar_list(mddManager);
1161printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
1162printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
1163 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
1164// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
1165graph_t * part = Fsm_FsmReadPartition(fsm);
1166printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
1167*/
1168/** state0 = s0 **/
1169// mdd_t * s0 = mdd_eq_c(mddManager,0, 0);
1170// mdd_t * s1 = mdd_eq_c(mddManager,2, 0);
1171// mdd_t * state0 = mdd_one(mddManager);
1172// state0 = mdd_and(s0,s1,1,1);
1173///** Next state1 = s2 + !s2 **/
1174//
1175// mdd_t * ns0 = mdd_eq_c(mddManager,1, 1);
1176// mdd_t * ns1 = mdd_eq_c(mddManager,3, 0);
1177// mdd_t * state1 = mdd_one(mddManager);
1178// state1 = mdd_and(ns0,ns1,1,1);
1179// state1 = mdd_or(state1,state1,1,0);
1180//
1181///** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
1182// rel = mdd_one(mddManager);
1183// rel = mdd_or(state0,state1,0,0);
1184///**********/
1185///** state0 = s2 **/
1186// mdd_t * s02 = mdd_eq_c(mddManager,0, 0);
1187// mdd_t * s12 = mdd_eq_c(mddManager,2, 1);
1188// mdd_t * state02 = mdd_one(mddManager);
1189// state02 = mdd_and(s02,s12,1,1);
1190///** Next state1 = s3 **/
1191//
1192// mdd_t * ns02 = mdd_eq_c(mddManager,1, 1);
1193// mdd_t * ns12 = mdd_eq_c(mddManager,3, 1);
1194// mdd_t * state12 = mdd_one(mddManager);
1195// state12 = mdd_and(ns02,ns12,1,1);
1196//
1197///** state = s0) -> !(Nextstate = s3) **/
1198// mdd_t * new_rel = mdd_one(mddManager);
1199// new_rel = mdd_or(state02,state12,0,0);
1200// rel = mdd_and(new_rel,rel,1,1);
1201// mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
1202
1203return 0; /* normal exit */
1204
1205usage:
1206(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1207(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
1208(void) fprintf(vis_stderr, " -v\t\tverbose\n");
1209return 1; /* error exit */
1210
1211}
1212
1213
Note: See TracBrowser for help on using the repository browser.