source: vis_dev/vis-2.3/src/fsm/fsmFsm.c @ 35

Last change on this file since 35 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 84.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [fsmFsm.c]
4
5  PackageName [fsm]
6
7  Synopsis    [Routines to create and manipulate the FSM structure.]
8
9  Author      [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, In-Ho Moon]
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 "fsmInt.h"
33
34static char rcsid[] UNUSED = "$Id: fsmFsm.c,v 1.88 2007/04/02 17:03:13 hhkim Exp $";
35
36/**AutomaticStart*************************************************************/
37
38/*---------------------------------------------------------------------------*/
39/* Static function prototypes                                                */
40/*---------------------------------------------------------------------------*/
41
42static Fsm_Fsm_t * FsmStructAlloc(Ntk_Network_t *network, graph_t *partition);
43static void FsmCreateVariableCubes(Fsm_Fsm_t *fsm);
44static int nameCompare(const void * name1, const void * name2);
45static boolean VarIdArrayCompare(mdd_manager *mddMgr, array_t *vars1, array_t *vars2);
46static boolean NSFunctionNamesCompare(mdd_manager *mddMgr, array_t *names1, array_t *names2);
47static array_t * GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable, st_table *pseudoMddIdTable);
48
49/**AutomaticEnd***************************************************************/
50
51
52/*---------------------------------------------------------------------------*/
53/* Definition of exported functions                                          */
54/*---------------------------------------------------------------------------*/
55
56/**Function********************************************************************
57
58  Synopsis    [Creates an FSM from a network.]
59
60  Description [Creates an FSM from a network and a partition. The FSM is
61  initialized to the single fairness constraint TRUE, indicating that all
62  states are "accepting". Reachability information, fair states, and
63  imageInfo, are initialized to NIL, since these items are computed on
64  demand. If the network has no latches, then NULL is returned and a message
65  is written to error_string.<p>
66
67  The partition gives the MVFs defining the next state functions of the
68  network.  If the partition is NULL, then a duplicate of the default
69  partition of the network (found using Part_NetworkReadPartition) is used.
70  If the network has no default partition, then NULL is returned and a message
71  is written to error_string.  Having the partition as a parameter gives the
72  calling application the flexibility of using a different partition from the
73  default, possibly one representing different functions than those given by
74  the network (say for the purpose of computing approximations).  However, it
75  is assumed (though not checked), that the partition has the same
76  combinational input variables and next state function names as the network.
77  Finally, note that the given partition will be freed when the FSM is freed.]
78
79  SideEffects []
80
81  SeeAlso     [Fsm_FsmFree]
82
83******************************************************************************/
84Fsm_Fsm_t *
85Fsm_FsmCreateFromNetworkWithPartition(
86  Ntk_Network_t *network,
87  graph_t       *partition)
88{
89  lsGen       gen;
90  Ntk_Node_t *latch;
91  Ntk_Node_t *input;
92  Fsm_Fsm_t  *fsm;
93  int i;
94 
95  fsm = FsmStructAlloc(network, partition);
96  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
97  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);
98 
99  /* sort by name of latch */
100  Ntk_NetworkForEachLatch(network, gen, latch){
101    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
102                      Ntk_NodeReadName(latch));
103  }
104
105  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);
106
107  for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i ++) {
108    char *nodeName;
109    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
110    latch = Ntk_NetworkFindNodeByName(network, nodeName);
111    array_insert(char*, fsm->fsmData.nextStateFunctions, i,
112                 Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
113    array_insert_last(int, fsm->fsmData.presentStateVars,
114                      Ntk_NodeReadMddId(latch));
115    array_insert_last(int, fsm->fsmData.nextStateVars,
116                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
117  }
118 
119  Ntk_NetworkForEachInput(network, gen, input){
120    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
121  }
122 
123  FsmCreateVariableCubes(fsm);
124  return (fsm);
125}
126
127
128
129/**Function********************************************************************
130
131  Synopsis    [Creates a FSM given the set of latches and the inputs.]
132
133  Description [This function is primarily used to create a "reduced"
134  FSM specific to a particular property during model checking. The
135  given array of latches and inputs are associated with the FSM. If
136  partition is NIL, the default partition from network is
137  obtained. This partition will be used to obtain the next state
138  functions of the latches. The last argument is an arry of fairness
139  constraints which is used to restrict the reduced fsm to fair
140  paths. </p>
141  For a detailed desription of various fields of FSM, please refer to
142  the function Fsm_FsmCreateFromNetworkWithPartition.]
143
144  SideEffects []
145
146  SeeAlso     [Fsm_FsmFree Fsm_FsmCreateFromNetworkWithPartition]
147
148******************************************************************************/
149Fsm_Fsm_t *
150Fsm_FsmCreateReducedFsm(
151  Ntk_Network_t *network,
152  graph_t       *partition,
153  array_t       *latches,
154  array_t       *inputs,
155  array_t       *fairArray)
156{
157  Ntk_Node_t *latch;
158  Ntk_Node_t *input;
159  Fsm_Fsm_t  *fsm;
160  Fsm_Fairness_t *fairness;
161  int i,j;
162 
163  if (array_n(latches) == 0){
164    error_append("Number of latches passed = 0. Cannot create sub-FSM.");
165    return (NIL(Fsm_Fsm_t));
166  }
167 
168  fsm = FsmStructAlloc(network, partition);
169  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
170
171  /* initialize fairness constraints */
172  if (fairArray != NIL(array_t)){
173    fairness = FsmFairnessAlloc(fsm);   
174    for (j = 0; j < array_n(fairArray); j++) {
175      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j);
176     
177      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
178    }
179    fsm->fairnessInfo.constraint = fairness;
180  }
181  else {
182    fsm->fairnessInfo.constraint =
183        FsmFsmCreateDefaultFairnessConstraint(fsm);
184  }
185
186  /* sort latches by name */
187  for(i=0; i<array_n(latches); i++){
188    latch = array_fetch(Ntk_Node_t*, latches, i);
189    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
190                      Ntk_NodeReadName(latch));
191  }
192  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);
193
194  for(i=0; i<array_n(latches); i++){
195    char *nodeName;
196    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
197    latch = Ntk_NetworkFindNodeByName(network, nodeName); 
198    array_insert_last(int, fsm->fsmData.presentStateVars,
199                      Ntk_NodeReadMddId(latch));
200    array_insert_last(int, fsm->fsmData.nextStateVars,
201                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
202    array_insert(char*, fsm->fsmData.nextStateFunctions, i, 
203                      Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
204  }
205 
206  for(i=0; i<array_n(inputs); i++){
207    input = array_fetch(Ntk_Node_t*, inputs, i);
208    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
209  }
210
211  FsmCreateVariableCubes(fsm);
212  return (fsm);
213}
214
215/**Function********************************************************************
216
217  Synopsis    [Creates a FSM given the set of latches and the inputs.]
218
219  Description [This function is primarily used to create an "abstract"
220  FSM specific to a particular property during invariant checking with
221  abstraction refinement method Grab. The given array of latches and
222  inputs are associated with the FSM. the array of invisible latches
223  can be treated either as inputs (independentFlag==TRUE), or as
224  latches (independentFlag==FALSE). It is the user's responsibility to
225  make sure that latches, invisibleVars, and inputs are mutually
226  disjoint.
227
228  When independentFlag==TRUE, the FSM is defined by the pair
229  (fsmData.presentStateVars, fsmData.inputVars); when
230  independentFlag==FALSE, the FSM is defined by the pair
231  (fsmData.globalPsVars, fsmData.primaryInputVars). For more
232  information, please check the function
233  Fsm_FsmReadOrCreateImageInfo(). The two pairs are defined as
234  follows:
235
236                presentStateVars inputVars  globalPsVars primaryInputVars
237  -----------------------------------------------------------------------
238  absLatches   |        X                        X
239  invisibleVars|                     X           X
240  inputs       |                     X                          X 
241  -----------------------------------------------------------------------
242
243  If partition is NIL, the default partition from network is
244  obtained. This partition will be used to obtain the next state
245  functions of the latches. The last argument is an arry of fairness
246  constraints which is used to restrict the reduced fsm to fair
247  paths. </p> For a detailed desription of various fields of FSM,
248  please refer to the function Fsm_FsmCreateFromNetworkWithPartition.]
249
250  SideEffects []
251
252  SeeAlso     [Fsm_FsmFree Fsm_FsmCreateReducedFsm]
253
254******************************************************************************/
255Fsm_Fsm_t *
256Fsm_FsmCreateAbstractFsm(
257  Ntk_Network_t *network,
258  graph_t       *partition,
259  array_t       *latches,
260  array_t       *invisibleVars,
261  array_t       *inputs,
262  array_t       *fairArray,
263  boolean        independentFlag)
264{
265  Ntk_Node_t *latch;
266  Ntk_Node_t *input;
267  Ntk_Node_t *node;
268  Fsm_Fsm_t  *fsm;
269  Fsm_Fairness_t *fairness;
270  int i,j;
271 
272  if (FALSE && array_n(latches) == 0){
273    error_append("Number of latches passed = 0. Cannot create sub-FSM.");
274    return (NIL(Fsm_Fsm_t));
275  }
276 
277  fsm = FsmStructAlloc(network, partition);
278  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
279
280  /* initialize fairness constraints */
281  if (fairArray != NIL(array_t)){
282    fairness = FsmFairnessAlloc(fsm);   
283    for (j = 0; j < array_n(fairArray); j++) {
284      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j);
285     
286      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
287    }
288    fsm->fairnessInfo.constraint = fairness;
289  }
290  else {
291    fsm->fairnessInfo.constraint =
292        FsmFsmCreateDefaultFairnessConstraint(fsm);
293  }
294
295  /* when independentFlag==FALSE, use globalPsVars and
296   * primaryInputVars (instead of presentStateVars and inputVars) to
297   * build the transition relation
298   */
299  if (!independentFlag) {
300    fsm->fsmData.globalPsVars = array_alloc(int, 0);
301    fsm->fsmData.primaryInputVars = array_alloc(int, 0);
302  }
303
304
305  /* sort latches by name */
306  for(i=0; i<array_n(latches); i++){
307    latch = array_fetch(Ntk_Node_t*, latches, i);
308    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
309                      Ntk_NodeReadName(latch));
310  }
311  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);
312
313  for(i=0; i<array_n(latches); i++){
314    char *nodeName;
315    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
316    latch = Ntk_NetworkFindNodeByName(network, nodeName); 
317    array_insert_last(int, fsm->fsmData.presentStateVars,
318                      Ntk_NodeReadMddId(latch));
319    array_insert_last(int, fsm->fsmData.nextStateVars,
320                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
321    array_insert(char*, fsm->fsmData.nextStateFunctions, i, 
322                      Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
323   
324    if (!independentFlag)
325      array_insert_last(int, fsm->fsmData.globalPsVars,
326                        Ntk_NodeReadMddId(latch));     
327  }
328
329  for(i=0; i<array_n(inputs); i++){
330    input = array_fetch(Ntk_Node_t*, inputs, i);
331    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
332   
333    if (!independentFlag)
334      array_insert_last(int, fsm->fsmData.primaryInputVars, 
335                        Ntk_NodeReadMddId(input));
336  }
337
338
339  arrayForEachItem(Ntk_Node_t *, invisibleVars, i, node) {
340    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(node));
341
342    if (!independentFlag) {
343      array_insert_last(int, fsm->fsmData.globalPsVars, 
344                        Ntk_NodeReadMddId(node));
345    }
346  }
347
348
349  FsmCreateVariableCubes(fsm);
350  return (fsm);
351}
352
353
354/**Function********************************************************************
355
356  Synopsis    [Frees the memory associated with an FSM.]
357
358  Description [Frees the memory associated with an FSM. In particular, frees
359  all the MDDs, and frees the associated partition.  The FSM's corresponding
360  network is not modified in any way.]
361
362  SideEffects []
363
364  SeeAlso     [Fsm_FsmCreateFromNetwork]
365
366******************************************************************************/
367void
368Fsm_FsmFree(
369  Fsm_Fsm_t * fsm)
370{
371  Part_PartitionFree(fsm->partition);
372  Fsm_FsmSubsystemFree(fsm);
373}
374
375/**Function********************************************************************
376
377  Synopsis    [Frees the memory associated with an FSM.]
378
379  Description [Identical to Fsm_FsmFree() but does not free the partition.]
380
381  SideEffects []
382
383  SeeAlso     [Fsm_FsmCreateSubsystemFromNetwork]
384
385******************************************************************************/
386void
387Fsm_FsmSubsystemFree(
388  Fsm_Fsm_t * fsm)
389{
390
391  Fsm_FsmFreeImageInfo(fsm);
392 
393  /* Free reachability info. */
394  if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){
395    mdd_free(fsm->reachabilityInfo.initialStates);
396  }
397  if (fsm->reachabilityInfo.reachableStates != NIL(mdd_t)){
398    mdd_free(fsm->reachabilityInfo.reachableStates);
399  }
400  if (fsm->reachabilityInfo.apprReachableStates != NIL(array_t))
401    mdd_array_free(fsm->reachabilityInfo.apprReachableStates);
402  if (fsm->reachabilityInfo.subPsVars != NIL(array_t)){
403    int i;
404    array_t *psVars;
405    arrayForEachItem(array_t *, fsm->reachabilityInfo.subPsVars, i, psVars) {
406      array_free(psVars);
407    }
408    array_free(fsm->reachabilityInfo.subPsVars);
409  }
410  if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)){
411    mdd_array_free(Fsm_FsmReadReachabilityOnionRings(fsm));
412  }
413
414  /* Free fairness info. */
415  FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t));
416
417  array_free(fsm->fsmData.presentStateVars);
418  array_free(fsm->fsmData.nextStateVars);
419  array_free(fsm->fsmData.inputVars);
420  array_free(fsm->fsmData.nextStateFunctions);
421  if (fsm->fsmData.pseudoInputVars)
422    array_free(fsm->fsmData.pseudoInputVars);
423  if (fsm->fsmData.primaryInputVars)
424    array_free(fsm->fsmData.primaryInputVars);
425  if (fsm->fsmData.globalPsVars)
426    array_free(fsm->fsmData.globalPsVars);
427
428  if (fsm->fsmData.presentStateCube)
429    mdd_free(fsm->fsmData.presentStateCube);
430  if (fsm->fsmData.nextStateCube)
431    mdd_free(fsm->fsmData.nextStateCube);
432  if (fsm->fsmData.inputCube)
433    mdd_free(fsm->fsmData.inputCube);
434  if (fsm->fsmData.pseudoInputCube)
435    mdd_free(fsm->fsmData.pseudoInputCube);
436  if (fsm->fsmData.primaryInputCube)
437    mdd_free(fsm->fsmData.primaryInputCube);
438  if (fsm->fsmData.globalPsCube)
439    mdd_free(fsm->fsmData.globalPsCube);
440
441  if (fsm->fsmData.pseudoInputBddVars)
442    mdd_array_free(fsm->fsmData.pseudoInputBddVars);
443  if (fsm->fsmData.presentStateBddVars)
444    mdd_array_free(fsm->fsmData.presentStateBddVars);
445
446  FREE(fsm);
447}
448
449/**Function********************************************************************
450
451  Synopsis    [Callback function to free an FSM.]
452
453  Description [Typecasts data to (Fsm_Fsm_t *) and then calls Fsm_FsmFree.
454  This function should only be used as a callback for other applications that
455  don't know the FSM type, for example the network ApplInfoTable.]
456
457  SideEffects []
458
459  SeeAlso     [Fsm_FsmFree]
460
461******************************************************************************/
462void
463Fsm_FsmFreeCallback(
464  void * data /* an object of type Fsm_Fsm_t*  type casted to void* */)
465{
466  Fsm_FsmFree((Fsm_Fsm_t *) data);
467}
468
469
470/**Function********************************************************************
471
472  Synopsis    [Returns the corresponding network of an FSM.]
473
474  SideEffects []
475
476  SeeAlso     [Fsm_FsmCreateFromNetwork]
477
478******************************************************************************/
479Ntk_Network_t *
480Fsm_FsmReadNetwork(
481  Fsm_Fsm_t * fsm)
482{
483  return (fsm->network);
484}
485
486/**Function********************************************************************
487
488  Synopsis    [Read UnquantifiedFlag of an FSM.]
489
490  Description [This is function for FateAndFreeWill counterexample generation.]
491
492  SideEffects []
493
494  SeeAlso     [Fsm_FsmCreateFromNetwork]
495
496******************************************************************************/
497boolean
498Fsm_FsmReadUseUnquantifiedFlag(
499  Fsm_Fsm_t * fsm)
500{
501  return (fsm->useUnquantifiedFlag);
502}
503
504/**Function********************************************************************
505
506  Synopsis    [Returns the MDD manager of the corresponding network of an FSM.]
507
508  SideEffects []
509
510  SeeAlso     [Fsm_FsmCreateFromNetwork]
511
512******************************************************************************/
513mdd_manager *
514Fsm_FsmReadMddManager(
515  Fsm_Fsm_t * fsm)
516{
517  return (Ntk_NetworkReadMddManager(fsm->network));
518}
519
520
521/**Function********************************************************************
522
523  Synopsis    [Returns the FSM of a network; creates FSM if necessary.]
524
525  Description [If there is an FSM associated with network, then returns it.
526  Otherwise, creates an FSM from network (using a duplicate of the partition
527  associated with the network), registers the FSM with the network, and then
528  returns the newly created FSM.  Note that if the network has no latches or
529  the network has no partition, then a NULL FSM is returned.]
530
531  SideEffects []
532
533  SeeAlso     [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo
534  Fsm_NetworkReadFsm]
535
536******************************************************************************/
537Fsm_Fsm_t *
538Fsm_NetworkReadOrCreateFsm(
539  Ntk_Network_t * network)
540{
541  Fsm_Fsm_t *fsm = (Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network, FSM_NETWORK_APPL_KEY);
542     
543  if (fsm == NIL(Fsm_Fsm_t)) {
544    fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
545    if (fsm != NIL(Fsm_Fsm_t)) {
546      (void) Ntk_NetworkAddApplInfo(network, FSM_NETWORK_APPL_KEY,
547                             (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
548                             (void *) fsm);
549    }
550  }
551 
552  return fsm;
553}
554
555
556/**Function********************************************************************
557
558  Synopsis    [Returns the FSM of a network.]
559
560  Description [Returns the FSM of a network, which may be NULL.]
561
562  SideEffects []
563
564  SeeAlso     [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo
565  Fsm_NetworkReadOrCreateFsm]
566
567******************************************************************************/
568Fsm_Fsm_t *
569Fsm_NetworkReadFsm(
570  Ntk_Network_t * network)
571{
572  return ((Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network,
573                                               FSM_NETWORK_APPL_KEY));
574}
575
576
577/**Function********************************************************************
578
579  Synopsis    [Returns the imageInfo struct stored by the FSM.]
580
581  Description [Returns the imageInfo struct stored by the FSM, which may be
582  NULL.]
583
584  SideEffects []
585
586  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]
587
588******************************************************************************/
589Img_ImageInfo_t *
590Fsm_FsmReadImageInfo(
591  Fsm_Fsm_t *fsm)
592{
593  return (fsm->imageInfo);
594}
595
596/**Function********************************************************************
597
598  Synopsis    [Set the imageInfo.]
599
600  Description [Set the imageInfo. ]
601
602  SideEffects []
603
604  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]
605
606******************************************************************************/
607void
608Fsm_FsmSetImageInfo(
609  Fsm_Fsm_t *fsm, Img_ImageInfo_t *imageInfo)
610{
611  fsm->imageInfo = imageInfo;
612}
613
614/**Function********************************************************************
615
616  Synopsis    [Returns the imageInfo struct stored by the FSM.]
617
618  Description [Returns the imageInfo struct stored by the FSM, which may be
619  NULL.]
620
621  SideEffects []
622
623  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]
624
625******************************************************************************/
626void
627Fsm_FsmFreeImageInfo(
628  Fsm_Fsm_t *fsm)
629{
630  if(fsm->imageInfo) {
631    Img_ImageInfoFree(fsm->imageInfo);
632    fsm->imageInfo = NIL(Img_ImageInfo_t);
633  }
634
635  if(fsm->unquantifiedImageInfo) {
636    Img_ImageInfoFree(fsm->unquantifiedImageInfo);
637    fsm->unquantifiedImageInfo = NIL(Img_ImageInfo_t);
638  }
639}
640
641/**Function********************************************************************
642
643  Synopsis    [Returns the partition associated with the FSM.]
644
645  Description [Returns the partition associated with the FSM.  This is the
646  graph of MVFs defining the combinational output functions of the FSM.]
647
648  SideEffects []
649
650  SeeAlso     [Fsm_FsmCreateFromNetwork]
651
652******************************************************************************/
653graph_t *
654Fsm_FsmReadPartition(
655  Fsm_Fsm_t *fsm)
656{
657  return (fsm->partition);
658}
659
660/**Function********************************************************************
661
662  Synopsis    [Test if reachability has been performed on the FSM.]
663
664  Description [Return TRUE if reachability has already been performed, else FALSE.]
665
666  SideEffects []
667
668  SeeAlso     [Fsm_FsmComputeReachableStates]
669
670******************************************************************************/
671boolean
672Fsm_FsmTestIsReachabilityDone(
673  Fsm_Fsm_t *fsm)
674{
675 
676  if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
677        return TRUE;
678  }
679  return FALSE;
680}
681
682/**Function********************************************************************
683
684  Synopsis    [Test if approximate reachability has been performed on the FSM.]
685
686  Description [Return TRUE if approximate reachability has already been
687  performed, else FALSE.]
688
689  SideEffects []
690
691  SeeAlso     [Fsm_FsmComputeReachableStates]
692
693******************************************************************************/
694boolean
695Fsm_FsmTestIsOverApproximateReachabilityDone(
696  Fsm_Fsm_t *fsm)
697{
698 
699  if (Fsm_FsmReadOverApproximateReachableStates(fsm) != NIL(array_t)) {
700        return TRUE;
701  }
702  return FALSE;
703}
704
705
706/**Function********************************************************************
707
708  Synopsis    [Returns the reachable states of an FSM.]
709
710  SideEffects [Returns the reachable states of an FSM.]
711
712  SeeAlso     [Fsm_FsmComputeReachableStates]
713
714******************************************************************************/
715mdd_t *
716Fsm_FsmReadReachableStates(
717  Fsm_Fsm_t *fsm)
718{
719  if (fsm->reachabilityInfo.rchStatus == Fsm_Rch_Exact_c)
720    return(fsm->reachabilityInfo.reachableStates);
721  else
722    return(NIL(mdd_t));
723}
724
725
726/**Function********************************************************************
727
728  Synopsis    [Returns the reachable states of an FSM.]
729
730  SideEffects [Returns the reachable states of an FSM. May be an under
731  approximation or an over approximation.]
732
733  SeeAlso     [Fsm_FsmComputeReachableStates]
734
735******************************************************************************/
736mdd_t *
737Fsm_FsmReadCurrentReachableStates(
738  Fsm_Fsm_t *fsm)
739{
740  return(fsm->reachabilityInfo.reachableStates);
741}
742
743
744/**Function********************************************************************
745
746  Synopsis    [Returns the approximate reachable states of an FSM.]
747
748  SideEffects []
749
750  SeeAlso     [Fsm_ArdcComputeOverApproximateReachableStates]
751
752******************************************************************************/
753array_t *
754Fsm_FsmReadOverApproximateReachableStates(
755  Fsm_Fsm_t *fsm)
756{
757  if (fsm->reachabilityInfo.overApprox >= 2)
758    return(fsm->reachabilityInfo.apprReachableStates);
759  else
760    return(NIL(array_t));
761}
762
763
764/**Function********************************************************************
765
766  Synopsis    [Returns the current approximate reachable states of an FSM.]
767
768  SideEffects []
769
770  SeeAlso     [Fsm_ArdcComputeOverApproximateReachableStates]
771
772******************************************************************************/
773array_t *
774Fsm_FsmReadCurrentOverApproximateReachableStates(
775  Fsm_Fsm_t *fsm)
776{
777  return(fsm->reachabilityInfo.apprReachableStates);
778}
779
780/**Function********************************************************************
781
782  Synopsis    [Return array of onion rings from reachability computation]
783
784  Description [Return array of onion rings from reachability
785  computation; NIL if reachability has not been performed. DO NOT free
786  this array.]
787
788  SideEffects []
789
790  SeeAlso     [Fsm_FsmComputeReachableStates]
791
792******************************************************************************/
793array_t *
794Fsm_FsmReadReachabilityOnionRings(
795  Fsm_Fsm_t *fsm)
796{
797  return fsm->reachabilityInfo.onionRings;
798}
799
800/**Function********************************************************************
801
802  Synopsis [Checks whether the onion rings are consistent with the
803  reachable states.]
804
805  Description [Checks whether the onion rings are consistent with the
806  reachable states. Returns FALSE if no states in onion
807  rings.]
808
809  SideEffects [result is set to the union of the onion rings]
810
811  SeeAlso     [Fsm_FsmbtainBFSShells]
812
813******************************************************************************/
814boolean
815Fsm_FsmReachabilityOnionRingsStates(
816  Fsm_Fsm_t *fsm,
817  mdd_t ** result)
818{
819  int i;
820  mdd_t *tmpMdd;
821  mdd_t *ring;
822  array_t *onionRings;
823
824  onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
825  if ( onionRings == NIL(array_t) ) {
826    *result = NIL(mdd_t);
827    return 0;
828  }
829
830  *result = bdd_zero(Fsm_FsmReadMddManager(fsm));
831  arrayForEachItem(mdd_t *, onionRings, i, ring) {
832    tmpMdd = mdd_or(*result, ring, 1, 1);
833    mdd_free(*result);
834    *result = tmpMdd;
835  }
836  if (Fsm_FsmReadCurrentReachableStates(fsm)) {
837    if (mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm), *result, 1,1)) {
838      FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
839    }
840  }
841  return (Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm));
842}
843
844/**Function********************************************************************
845
846  Synopsis    [Checks if the onion rings are consistent with the
847  reachable states.]
848
849  Description [Checks if the onion rings are consistent with the
850  reachable states.]
851
852  SideEffects []
853
854  SeeAlso     [Fsm_FsmComputeReachableStates]
855
856******************************************************************************/
857boolean
858Fsm_FsmTestReachabilityOnionRingsUpToDate(
859  Fsm_Fsm_t *fsm)
860{
861  return fsm->reachabilityInfo.onionRingsUpToDate;
862}
863
864/**Function********************************************************************
865
866  Synopsis    [Checks if the onion rings are due to BFS or not.]
867
868  Description [Checks if the onion rings are due to BFS or not.]
869
870  SideEffects []
871
872  SeeAlso     [Fsm_FsmComputeReachableStates]
873
874******************************************************************************/
875Fsm_RchType_t
876Fsm_FsmReadReachabilityOnionRingsMode(
877  Fsm_Fsm_t *fsm)
878{
879  return fsm->reachabilityInfo.onionRingsMode;
880}
881
882 
883/**Function********************************************************************
884
885  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
886  necessary.]
887
888  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
889  currently exist in the FSM, then one is initialized and set, before it is
890  returned.  The imageInfo is initialized using the default image method, and
891  is initialized for both forward and backward image computations. It uses the
892  partition with which this FSM was created when the function
893  Fsm_FsmCreateFromNetwork was called.]
894
895  SideEffects []
896
897  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]
898
899******************************************************************************/
900Img_ImageInfo_t *
901Fsm_FsmReadOrCreateImageInfo(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
902{
903  Img_DirectionType     imgFlag = Img_Forward_c;
904  array_t               *presentStateVars, *inputVars;
905  mdd_t                 *presentStateCube, *inputCube;
906
907  if (bwdImgFlag && fwdImgFlag)
908    imgFlag = Img_Both_c;
909  else if (bwdImgFlag)
910    imgFlag = Img_Backward_c;
911
912  if (fsm->fsmData.globalPsVars) {
913    presentStateVars = fsm->fsmData.globalPsVars;
914    inputVars = fsm->fsmData.primaryInputVars;
915    presentStateCube = fsm->fsmData.globalPsCube;
916    inputCube = fsm->fsmData.primaryInputCube;
917  } else {
918    presentStateVars = fsm->fsmData.presentStateVars;
919    inputVars = fsm->fsmData.inputVars;
920    presentStateCube = fsm->fsmData.presentStateCube;
921    inputCube = fsm->fsmData.inputCube;
922  }
923
924  fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo,
925                                           fsm->partition,
926                                           fsm->fsmData.nextStateFunctions,
927                                           presentStateVars,
928                                           fsm->fsmData.nextStateVars,
929                                           inputVars,
930                                           presentStateCube,
931                                           fsm->fsmData.nextStateCube,
932                                           inputCube,
933                                           fsm->network,
934                                           Img_Default_c, imgFlag, 0, 0);
935
936  if (fsm->fsmData.globalPsVars) {
937    Img_ImageInfoUpdateVariables(fsm->imageInfo,
938                                 fsm->partition,
939                                 fsm->fsmData.presentStateVars,
940                                 fsm->fsmData.inputVars,
941                                 fsm->fsmData.presentStateCube,
942                                 fsm->fsmData.inputCube);
943  }
944
945  return(fsm->imageInfo);
946}
947
948/**Function********************************************************************
949
950  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
951  necessary.]
952
953  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
954  currently exist in the FSM, then one is initialized and set, before it is
955  returned.  The imageInfo is initialized using the default image method, and
956  is initialized for both forward and backward image computations. It uses the
957  partition with which this FSM was created when the function
958  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo
959  that has no quntified input for Fate and Free will.]
960
961  SideEffects []
962
963  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]
964
965******************************************************************************/
966Img_ImageInfo_t *
967Fsm_FsmReadOrCreateImageInfoFAFW(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
968{
969  Img_DirectionType     imgFlag = Img_Forward_c;
970  array_t               *presentStateVars, *inputVars;
971  mdd_t                 *presentStateCube, *inputCube;
972  mdd_manager           *mgr;
973
974  mgr = Fsm_FsmReadMddManager(fsm);
975
976  if (bwdImgFlag && fwdImgFlag)
977    imgFlag = Img_Both_c;
978  else if (bwdImgFlag)
979    imgFlag = Img_Backward_c;
980
981  presentStateVars = fsm->fsmData.presentStateVars;
982  inputVars = array_alloc(int , 0);
983  presentStateCube = fsm->fsmData.presentStateCube;
984  inputCube = mdd_one(mgr);
985
986  fsm->unquantifiedImageInfo = Img_ImageInfoInitialize(
987                                           fsm->unquantifiedImageInfo,
988                                           fsm->partition,
989                                           fsm->fsmData.nextStateFunctions,
990                                           presentStateVars,
991                                           fsm->fsmData.nextStateVars,
992                                           inputVars,
993                                           presentStateCube,
994                                           fsm->fsmData.nextStateCube,
995                                           inputCube,
996                                           fsm->network,
997                                           Img_Default_c, imgFlag, 1, 0);
998
999  if(!Img_IsQuantifyArraySame(fsm->unquantifiedImageInfo, inputVars)) {
1000    array_free(inputVars);
1001  }
1002
1003  if(!Img_IsQuantifyCubeSame(fsm->unquantifiedImageInfo, inputCube)) {
1004    mdd_free(inputCube);
1005  }
1006
1007  return(fsm->unquantifiedImageInfo);
1008}
1009
1010/**Function********************************************************************
1011
1012  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
1013  necessary.]
1014
1015  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
1016  currently exist in the FSM, then one is initialized and set, before it is
1017  returned.  The imageInfo is initialized using the default image method, and
1018  is initialized for both forward and backward image computations. It uses the
1019  partition with which this FSM was created when the function
1020  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo
1021  that has no quntified input for Fate and Free will.]
1022
1023  SideEffects []
1024
1025  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]
1026
1027******************************************************************************/
1028Img_ImageInfo_t *
1029Fsm_FsmReadOrCreateImageInfoPrunedFAFW(Fsm_Fsm_t *fsm, mdd_t *Winning, int bwdImgFlag, int fwdImgFlag)
1030{
1031  Img_DirectionType     imgFlag = Img_Forward_c;
1032  array_t               *presentStateVars, *inputVars;
1033  mdd_t                 *presentStateCube, *inputCube;
1034  mdd_manager           *mgr;
1035  Img_ImageInfo_t *imageInfo;
1036
1037  mgr = Fsm_FsmReadMddManager(fsm);
1038
1039  if (bwdImgFlag && fwdImgFlag)
1040    imgFlag = Img_Both_c;
1041  else if (bwdImgFlag)
1042    imgFlag = Img_Backward_c;
1043
1044  presentStateVars = fsm->fsmData.presentStateVars;
1045  inputVars = array_alloc(int , 0);
1046  presentStateCube = fsm->fsmData.presentStateCube;
1047  inputCube = mdd_one(mgr);
1048
1049  imageInfo = Img_ImageInfoInitialize(
1050                                           0,
1051                                           fsm->partition,
1052                                           fsm->fsmData.nextStateFunctions,
1053                                           presentStateVars,
1054                                           fsm->fsmData.nextStateVars,
1055                                           inputVars,
1056                                           presentStateCube,
1057                                           fsm->fsmData.nextStateCube,
1058                                           inputCube,
1059                                           fsm->network,
1060                                           Img_Default_c, imgFlag, 0, Winning);
1061
1062  if(!Img_IsQuantifyArraySame(imageInfo, inputVars)) {
1063    array_free(inputVars);
1064  }
1065
1066  if(!Img_IsQuantifyCubeSame(imageInfo, inputCube)) {
1067    mdd_free(inputCube);
1068  }
1069
1070  return(imageInfo);
1071}
1072
1073
1074/**Function********************************************************************
1075
1076  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
1077  necessary.]
1078
1079  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
1080  currently exist in the FSM, then one is initialized and set, before it is
1081  returned.  The imageInfo is initialized using the default image method, and
1082  is initialized for both forward and backward image computations. It uses the
1083  partition with which this FSM was created when the function
1084  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo
1085  that has no quntified input for Fate and Free will.]
1086
1087  SideEffects []
1088
1089  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]
1090
1091******************************************************************************/
1092Img_ImageInfo_t *
1093Fsm_FsmReadOrCreateImageInfoForComputingRange(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
1094{
1095  Img_DirectionType     imgFlag = Img_Forward_c;
1096  array_t               *presentStateVars, *inputVars;
1097  mdd_t                 *presentStateCube, *inputCube;
1098
1099  if (bwdImgFlag && fwdImgFlag)
1100    imgFlag = Img_Both_c;
1101  else if (bwdImgFlag)
1102    imgFlag = Img_Backward_c;
1103
1104  if (fsm->fsmData.globalPsVars) {
1105    presentStateVars = fsm->fsmData.globalPsVars;
1106    inputVars = fsm->fsmData.primaryInputVars;
1107    presentStateCube = fsm->fsmData.globalPsCube;
1108    inputCube = fsm->fsmData.primaryInputCube;
1109  } else {
1110    presentStateVars = fsm->fsmData.presentStateVars;
1111    inputVars = fsm->fsmData.inputVars;
1112    presentStateCube = fsm->fsmData.presentStateCube;
1113    inputCube = fsm->fsmData.inputCube;
1114  }
1115
1116  fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo,
1117                                           fsm->partition,
1118                                           fsm->fsmData.nextStateFunctions,
1119                                           presentStateVars,
1120                                           fsm->fsmData.nextStateVars,
1121                                           inputVars,
1122                                           presentStateCube,
1123                                           fsm->fsmData.nextStateCube,
1124                                           inputCube,
1125                                           fsm->network,
1126                                           Img_Linear_Range_c, imgFlag, 0, 0);
1127
1128  if (fsm->fsmData.globalPsVars) {
1129    Img_ImageInfoUpdateVariables(fsm->imageInfo,
1130                                 fsm->partition,
1131                                 fsm->fsmData.presentStateVars,
1132                                 fsm->fsmData.inputVars,
1133                                 fsm->fsmData.presentStateCube,
1134                                 fsm->fsmData.inputCube);
1135  }
1136
1137  return(fsm->imageInfo);
1138}
1139
1140/**Function********************************************************************
1141
1142  Synopsis [Computes the set of initial states of an FSM.]
1143
1144  Description [Computes the set of initial states of an FSM.  If this set
1145  has already been computed, then just returns the result of the previous
1146  computation.  The calling application is responsible for freeing the
1147  returned MDD in all cases.<p>
1148
1149  The nodes driving the initial inputs of the latches, called the initial
1150  nodes, must not have latches in their support.  If an initial node is found
1151  that has a latch in its transitive fanin, then a NULL MDD is returned, and a
1152  message is written to the error_string.<p>
1153 
1154  The initial states are computed as follows. For each latch i, the relation
1155  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
1156  and g_i(u) is the multi-valued initialization function of latch i, in terms
1157  of the input variables u.  These relations are then conjuncted, and the
1158  input variables are existentially quantified from the result
1159  (i.e. init_states(x) = \exists u \[\prod (x_i = g_i(u))\]).]
1160
1161  SideEffects [The result of the initial state computation is stored with
1162  the FSM.]
1163
1164  SeeAlso [Fsm_FsmComputeReachableStates]
1165 
1166******************************************************************************/
1167mdd_t *
1168Fsm_FsmComputeInitialStates(Fsm_Fsm_t *fsm)
1169{
1170  int            i = 0;
1171  lsGen          gen;
1172  mdd_t         *initStates;
1173  Ntk_Node_t    *node;
1174  array_t       *initRelnArray;
1175  array_t       *initMvfs;
1176  array_t       *initNodes;
1177  array_t       *initVertices;
1178  array_t       *latchMddIds;
1179  st_table      *supportNodes;
1180  st_table      *supportVertices;
1181  mdd_manager   *mddManager = Fsm_FsmReadMddManager(fsm);
1182  graph_t       *partition  = fsm->partition;
1183  Ntk_Network_t *network    = fsm->network;
1184  int            numLatches;
1185  array_t       *psVars;
1186  Img_MethodType imageMethod;
1187 
1188  /* If already computed, just return a copy. */
1189  if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){
1190    return (mdd_dup(fsm->reachabilityInfo.initialStates));
1191  }
1192
1193  psVars = fsm->fsmData.presentStateVars;
1194  numLatches = array_n(psVars);
1195
1196  /*
1197   * Get the array of initial nodes, both as network nodes and as partition
1198   * vertices.
1199   */
1200  initNodes    = array_alloc(Ntk_Node_t *, numLatches);
1201  initVertices = array_alloc(vertex_t *, numLatches);
1202  latchMddIds  = array_alloc(int, numLatches);
1203  for (i=0; i<numLatches; i++){
1204    int latchMddId = array_fetch(int, psVars, i);
1205    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
1206    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
1207    vertex_t   *initVertex = Part_PartitionFindVertexByName(partition,
1208                                Ntk_NodeReadName(initNode));
1209    array_insert(Ntk_Node_t *, initNodes, i, initNode);
1210    array_insert(vertex_t *, initVertices, i, initVertex);
1211    array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
1212  }
1213
1214  /*
1215   * Get the table of legal support nodes, both as network nodes and
1216   * as partition vertices. Inputs (both primary and pseudo) and constants
1217   * constitute the legal support nodes.
1218   */
1219  supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
1220  supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
1221  Ntk_NetworkForEachNode(network, gen, node) {
1222    vertex_t *vertex = Part_PartitionFindVertexByName(partition,
1223                                                      Ntk_NodeReadName(node));
1224
1225    if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
1226      st_insert(supportNodes, (char *) node, NIL(char));
1227      st_insert(supportVertices, (char *) vertex, NIL(char));
1228    }
1229  }
1230
1231  /*
1232   * If the initial nodes are not covered by the legal support nodes, then
1233   * return NIL.
1234   */
1235  if (!Ntk_NetworkTestLeavesCoverSupportOfRoots(network, initNodes,
1236                                                supportNodes)) {
1237    array_free(initNodes);
1238    array_free(initVertices);
1239    array_free(latchMddIds);
1240    st_free_table(supportNodes);
1241    st_free_table(supportVertices);
1242    return NIL(mdd_t);
1243  }
1244
1245  /*
1246   * At this point, we are certain that the initialization functions are
1247   * well-defined. Get the MVF for each initialization node, in terms of the
1248   * support vertices.  Note that the MVF for each initial node is guaranteed to
1249   * exist in the partition, since an initial node is a combinational
1250   * output.
1251   */
1252  array_free(initNodes);
1253  st_free_table(supportNodes);
1254  initMvfs = Part_PartitionCollapse(partition, initVertices,
1255                                    supportVertices, NIL(mdd_t)); 
1256  array_free(initVertices);
1257  st_free_table(supportVertices);
1258
1259  /* Compute the relation (x_i = g_i(u)) for each latch. */
1260  initRelnArray = array_alloc(mdd_t*, numLatches);
1261  for (i = 0; i < numLatches; i++) {
1262    int latchMddId = array_fetch(int, latchMddIds, i);
1263    Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
1264    mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
1265                                                                latchMddId);
1266    array_insert(mdd_t *, initRelnArray, i, initLatchReln);
1267  }
1268
1269  array_free(latchMddIds);
1270  Mvf_FunctionArrayFree(initMvfs);
1271
1272  /* init_states(x) = \exists u \[\prod (x_i = g_i(u))\] */
1273  /*initStates = Fsm_MddMultiwayAndSmooth(mddManager, initRelnArray,
1274                                        fsm->fsmData.inputVars);
1275  */   
1276
1277  imageMethod = Img_UserSpecifiedMethod();
1278  if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c)
1279    imageMethod = Img_Iwls95_c;
1280  initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray,
1281                                           fsm->fsmData.inputVars, psVars,
1282                                           imageMethod, Img_Forward_c); 
1283
1284  mdd_array_free(initRelnArray); 
1285
1286  fsm->reachabilityInfo.initialStates = initStates;
1287  return mdd_dup(initStates);
1288}
1289
1290
1291
1292/**Function********************************************************************
1293
1294  Synopsis [Returns the array of MDD ids of the present state variables of an
1295  FSM.]
1296
1297  Description [Returns the array of MDD ids of the present state variables of
1298  an FSM.  This array should not be modified or freed in any way.]
1299
1300  SideEffects []
1301
1302  SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars
1303  Fsm_FsmReadNextStateFunctionNames]
1304
1305******************************************************************************/
1306array_t *
1307Fsm_FsmReadPresentStateVars(Fsm_Fsm_t *fsm)
1308{
1309  return fsm->fsmData.presentStateVars;
1310}
1311
1312/**Function********************************************************************
1313
1314  Synopsis [Returns the array of MDD ids of the next state variables of an
1315  FSM.]
1316
1317  Description [Returns the array of MDD ids of the next state variables of
1318  an FSM.  This array should not be modified or freed in any way.]
1319
1320  SideEffects []
1321
1322  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadInputVars
1323  Fsm_FsmReadNextStateFunctionNames]
1324
1325******************************************************************************/
1326array_t *
1327Fsm_FsmReadNextStateVars(Fsm_Fsm_t *fsm)
1328{
1329  return fsm->fsmData.nextStateVars;
1330}
1331
1332/**Function********************************************************************
1333
1334  Synopsis [Returns an array of strings containing the names of the nodes
1335  driving the data inputs of the latches.]
1336
1337  Description [Returns the array of strings containing the names of the nodes
1338  driving the data inputs of the latches. This array should not be modified or
1339  freed in any way.]
1340
1341  SideEffects []
1342
1343  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars
1344  Fsm_FsmReadInputVars]
1345
1346******************************************************************************/
1347array_t *
1348Fsm_FsmReadNextStateFunctionNames(Fsm_Fsm_t *fsm)
1349{
1350  return fsm->fsmData.nextStateFunctions;
1351}
1352
1353/**Function********************************************************************
1354
1355  Synopsis [Returns the array of MDD ids of the input variables of an
1356  FSM.]
1357
1358  Description [Returns the array of MDD ids of the input variables of an FSM.
1359  This includes both primary inputs and pseudo inputs. This array should not
1360  be modified or freed in any way.]
1361
1362  SideEffects []
1363
1364  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars
1365  Fsm_FsmReadNextStateFunctionNames]
1366
1367******************************************************************************/
1368array_t *
1369Fsm_FsmReadInputVars(Fsm_Fsm_t *fsm)
1370{
1371  return fsm->fsmData.inputVars;
1372}
1373
1374array_t *
1375Fsm_FsmReadPrimaryInputVars(Fsm_Fsm_t *fsm)
1376{
1377  return fsm->fsmData.primaryInputVars;
1378}
1379
1380
1381/**Function********************************************************************
1382
1383  Synopsis [Returns the array of MDD ids of the pseudo input variables
1384  of a sub FSM.]
1385
1386  Description [Returns the array of MDD ids of the pseudo input variables
1387  of a sub FSM.  This array should not be modified or freed in any way.]
1388
1389  SideEffects []
1390
1391  SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars
1392  Fsm_FsmReadNextStateFunctionNames]
1393
1394******************************************************************************/
1395array_t *
1396Fsm_FsmReadPseudoInputVars(Fsm_Fsm_t *fsm)
1397{
1398  return fsm->fsmData.pseudoInputVars;
1399}
1400
1401/**Function********************************************************************
1402
1403  Synopsis [Set input variables into the FSM structure.]
1404
1405  Description []
1406
1407  SideEffects []
1408
1409  SeeAlso     []
1410
1411******************************************************************************/
1412void
1413Fsm_FsmSetInputVars(Fsm_Fsm_t *fsm, array_t *inputVars)
1414{
1415  fsm->fsmData.inputVars = inputVars;
1416}
1417
1418/**Function********************************************************************
1419
1420  Synopsis [Set useUnquantifiedFlag into the FSM structure.]
1421
1422  Description [This is function for FateAndFreeWill counterexample generation.]
1423
1424  SideEffects []
1425
1426  SeeAlso     []
1427
1428******************************************************************************/
1429void
1430Fsm_FsmSetUseUnquantifiedFlag(Fsm_Fsm_t *fsm, boolean value)
1431{
1432  fsm->useUnquantifiedFlag = value;
1433}
1434
1435/**Function********************************************************************
1436
1437  Synopsis [Set the initial states of an FSM.]
1438
1439  Description []
1440
1441  SideEffects [Old mdd_t representing the initial states is deleted and
1442  replaced by the argument provided.]
1443
1444  SeeAlso     []
1445
1446******************************************************************************/
1447void
1448Fsm_FsmSetInitialStates(Fsm_Fsm_t *fsm, mdd_t *initStates)
1449{
1450  mdd_t *init;
1451 
1452  init = fsm->reachabilityInfo.initialStates;
1453  if (init != NIL(mdd_t)) {
1454    mdd_free(init);
1455  }
1456  fsm->reachabilityInfo.initialStates = initStates;
1457}
1458
1459/**Function********************************************************************
1460
1461  Synopsis [Read FAFWFlag from the FSM structure.]
1462
1463  Description [This is function for FateAndFreeWill counterexample generation.]
1464
1465  SideEffects []
1466
1467  SeeAlso     []
1468
1469******************************************************************************/
1470int
1471Fsm_FsmReadFAFWFlag(Fsm_Fsm_t *fsm) 
1472{
1473  return((int)(fsm->FAFWFlag));
1474}
1475
1476/**Function********************************************************************
1477
1478  Synopsis [Set FAFWFlag in the FSM structure.]
1479
1480  Description [This is function for FateAndFreeWill counterexample generation.]
1481
1482  SideEffects []
1483
1484  SeeAlso     []
1485
1486******************************************************************************/
1487void
1488Fsm_FsmSetFAFWFlag(Fsm_Fsm_t *fsm, boolean FAFWFlag) 
1489{
1490  fsm->FAFWFlag = FAFWFlag;
1491}
1492
1493/**Function********************************************************************
1494
1495  Synopsis [Set input variables that are controlled by system and environment
1496            in the FSM structure.]
1497
1498  Description [This is function for FateAndFreeWill counterexample generation.]
1499
1500  SideEffects []
1501
1502  SeeAlso     []
1503
1504******************************************************************************/
1505void
1506Fsm_FsmSetSystemVariableFAFW(Fsm_Fsm_t *fsm, st_table *bddIdTable)
1507{
1508  mdd_manager *mgr;
1509  array_t *inputVars, *bddIdArray;
1510  bdd_t *extCube, *uniCube;
1511  bdd_t *newCube, *varBdd;
1512  st_generator *gen;
1513  int mddId, bddId, tbddId, i, j;
1514
1515  if(bddIdTable == 0 && fsm->FAFWFlag == 0) {
1516    if(fsm->extQuantifyInputCube)
1517      bdd_free(fsm->extQuantifyInputCube);
1518    if(fsm->uniQuantifyInputCube)
1519      bdd_free(fsm->uniQuantifyInputCube);
1520    fsm->extQuantifyInputCube = 0;
1521    fsm->uniQuantifyInputCube = 0;
1522    return;
1523  }
1524
1525  mgr = Fsm_FsmReadMddManager(fsm);
1526  inputVars = Fsm_FsmReadInputVars(fsm);
1527
1528  extCube = mdd_one(mgr);
1529  for(i=0; i<array_n(inputVars); i++) {
1530    mddId = array_fetch(int, inputVars, i);
1531    bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
1532    for(j=0; j<array_n(bddIdArray); j++) {
1533      bddId = array_fetch(int, bddIdArray, j);
1534      if(bddIdTable && st_lookup_int(bddIdTable, (char *)(long)bddId, &tbddId)) {
1535        continue;
1536      }
1537      varBdd = bdd_get_variable(mgr, bddId);
1538      newCube = bdd_and(extCube, varBdd, 1, 1);
1539      bdd_free(extCube); bdd_free(varBdd);
1540      extCube = newCube;
1541    }
1542    array_free(bddIdArray);
1543  }
1544  uniCube = mdd_one(mgr);
1545  if(bddIdTable) {
1546    st_foreach_item(bddIdTable, gen, &bddId, &bddId) {
1547      varBdd = bdd_get_variable(mgr, bddId);
1548      newCube = bdd_and(uniCube, varBdd, 1, 1);
1549      bdd_free(uniCube); bdd_free(varBdd);
1550      uniCube = newCube;
1551    }
1552  }
1553  fsm->extQuantifyInputCube = extCube;
1554  fsm->uniQuantifyInputCube = uniCube;
1555}
1556
1557/**Function********************************************************************
1558
1559  Synopsis [Read input variables that is controlled by environment
1560            in the FSM structure.]
1561
1562  Description [This is function for FateAndFreeWill counterexample generation.]
1563
1564  SideEffects []
1565
1566  SeeAlso     []
1567
1568******************************************************************************/
1569bdd_t *
1570Fsm_FsmReadExtQuantifyInputCube(Fsm_Fsm_t *fsm)
1571{
1572  return(fsm->extQuantifyInputCube);
1573}
1574
1575/**Function********************************************************************
1576
1577  Synopsis [Read input variables that is controlled by system
1578            in the FSM structure.]
1579
1580  Description [This is function for FateAndFreeWill counterexample generation.]
1581
1582  SideEffects []
1583
1584  SeeAlso     []
1585
1586******************************************************************************/
1587bdd_t *
1588Fsm_FsmReadUniQuantifyInputCube(Fsm_Fsm_t *fsm)
1589{
1590  return(fsm->uniQuantifyInputCube);
1591}
1592
1593/**Function********************************************************************
1594
1595  Synopsis    [Returns the current FSM of a hierarchy manager.]
1596
1597  Description [Returns the FSM of the network of the current node of a
1598  hierarchy manager. If the 1) hmgr is NULL, 2) current node is NULL, 3)
1599  network is NULL, 4) the variables of the network have not been ordered, 5) a
1600  partition doesn't exist for the network, or 6) the network does not have any
1601  latches, then a message is printed to vis_stderr, and NULL is returned.  If
1602  all the above conditions have been satisfied, and the network doesn't
1603  already have an FSM, then one is created.]
1604
1605  SideEffects []
1606
1607  SeeAlso     [Hrc_ManagerReadCurrentNode Ntk_HrcManagerReadCurrentNetwork
1608  Fsm_NetworkReadOrCreateFsm]
1609
1610******************************************************************************/
1611Fsm_Fsm_t *
1612Fsm_HrcManagerReadCurrentFsm(Hrc_Manager_t *hmgr)
1613{
1614  Fsm_Fsm_t     *fsm;
1615  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(hmgr);
1616 
1617  if (network == NIL(Ntk_Network_t)) {
1618    return NIL(Fsm_Fsm_t);
1619  }
1620
1621  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
1622    (void) fprintf(vis_stderr, "** fsm error: The MDD variables have not been ordered.  ");
1623    (void) fprintf(vis_stderr, "Use static_order.\n");
1624    return NIL(Fsm_Fsm_t);
1625  }
1626
1627  if (Part_NetworkReadPartition(network) == NIL(graph_t)){
1628    (void) fprintf(vis_stderr, "** fsm error: Network has not been partitioned.  ");
1629    (void) fprintf(vis_stderr, "Use build_partition_mdds.\n");
1630    return NIL(Fsm_Fsm_t);
1631  }
1632
1633  error_init();
1634  fsm = Fsm_NetworkReadOrCreateFsm(network);
1635  if (fsm == NIL(Fsm_Fsm_t)) {
1636    (void) fprintf(vis_stderr, "%s", error_string());
1637    (void) fprintf(vis_stderr, "\n");
1638  }
1639 
1640  return fsm;
1641}
1642
1643/**Function********************************************************************
1644
1645  Synopsis    [Creates a subFSM from a network.]
1646
1647  Description [Given a vertex table, the routine creates a subFSM. The routine
1648  reads in the vertex table  and stores only corresponding next state functions
1649  into the subFSM. Every present, next state and input variables in the system
1650  are stored into the subFSM.
1651  ]
1652
1653  SideEffects []
1654
1655  SeeAlso     [Fsm_FsmCreateFromNetworkWithPartition, Fsm_FsmFree]
1656
1657******************************************************************************/
1658Fsm_Fsm_t *
1659Fsm_FsmCreateSubsystemFromNetwork(
1660  Ntk_Network_t *network,
1661  graph_t       *partition,
1662  st_table      *vertexTable,
1663  boolean       independentFlag,
1664  int           createPseudoVarMode)
1665{
1666  lsGen       gen;
1667  Ntk_Node_t *latch;
1668  Ntk_Node_t *input;
1669  Fsm_Fsm_t  *fsm;
1670  char *latchName;
1671  int i;
1672  st_table *pseudoMddIdTable = NIL(st_table);
1673
1674  fsm = FsmStructAlloc(network, partition);
1675  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
1676  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);
1677
1678  /*
1679   * Creates an FSM for the subsystem.
1680   */
1681  /* sort latches by name. */
1682  Ntk_NetworkForEachLatch(network, gen, latch) {
1683    latchName = Ntk_NodeReadName(latch); 
1684    if(st_lookup(vertexTable, latchName, (char **)0)) {
1685      array_insert_last(char*, fsm->fsmData.nextStateFunctions, latchName);
1686    } /* end of if(st_lookup(vertexTable)) */
1687  }
1688
1689  if (independentFlag && createPseudoVarMode) {
1690    fsm->fsmData.pseudoInputVars = array_alloc(int, 0);
1691    fsm->fsmData.primaryInputVars = array_alloc(int, 0);
1692    fsm->fsmData.globalPsVars = array_alloc(int, 0);
1693    if (createPseudoVarMode == 2)
1694      pseudoMddIdTable = st_init_table(st_numcmp, st_numhash);
1695  }
1696
1697  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);
1698 
1699  arrayForEachItem(char *, fsm->fsmData.nextStateFunctions, i, latchName) {
1700    latch = Ntk_NetworkFindNodeByName(network, latchName); 
1701    array_insert(char*, fsm->fsmData.nextStateFunctions, i,
1702                 Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
1703    array_insert_last(int, fsm->fsmData.nextStateVars,
1704                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
1705    array_insert_last(int, fsm->fsmData.presentStateVars,
1706                      Ntk_NodeReadMddId(latch));
1707  } /* end of Ntk_NetworkForEachLatch(network, gen, latch) */
1708
1709  /* Fill in remaining latch for nextStateVars */
1710  if (!independentFlag || createPseudoVarMode) {
1711    Ntk_NetworkForEachLatch(network, gen, latch) {
1712      char *latchName = Ntk_NodeReadName(latch); 
1713      if(!st_lookup(vertexTable, latchName, (char **)0)) {
1714        if (independentFlag) {
1715          if (createPseudoVarMode == 1) {
1716            array_insert_last(int, fsm->fsmData.pseudoInputVars,
1717                                Ntk_NodeReadMddId(latch));
1718            array_insert_last(int, fsm->fsmData.inputVars,
1719                                Ntk_NodeReadMddId(latch));
1720          } else {
1721            st_insert(pseudoMddIdTable, (char *)(long)Ntk_NodeReadMddId(latch),
1722                        NIL(char));
1723          }
1724        } else {
1725          array_insert_last(int, fsm->fsmData.nextStateVars, 
1726                            Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
1727          array_insert_last(int, fsm->fsmData.presentStateVars,
1728                            Ntk_NodeReadMddId(latch));
1729        }
1730      }
1731    }
1732  }
1733
1734  /* Input variables are identical for every subsystems */
1735  Ntk_NetworkForEachInput(network, gen, input){
1736    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
1737    if (independentFlag && createPseudoVarMode) {
1738      array_insert_last(int, fsm->fsmData.primaryInputVars,
1739                        Ntk_NodeReadMddId(input));
1740    }
1741  }
1742
1743  if (independentFlag && createPseudoVarMode) {
1744    if (createPseudoVarMode == 2) {
1745      int       mddId;
1746      array_t   *supportMddIdArray;
1747      st_table  *mddIdTable;
1748
1749      mddIdTable = st_init_table(st_numcmp, st_numhash);
1750      arrayForEachItem(int, fsm->fsmData.presentStateVars, i, mddId) {
1751        st_insert(mddIdTable, (char *)(long)mddId, NIL(char));
1752      }
1753      arrayForEachItem(int, fsm->fsmData.inputVars, i, mddId) {
1754        st_insert(mddIdTable, (char *)(long)mddId, NIL(char));
1755      }
1756
1757      supportMddIdArray = GetMddSupportIdArray(fsm, mddIdTable,
1758                                                pseudoMddIdTable);
1759
1760      arrayForEachItem(int, supportMddIdArray, i, mddId) {
1761        if (!st_lookup(mddIdTable, (char *)(long)mddId, NIL(char *))) {
1762          array_insert_last(int, fsm->fsmData.pseudoInputVars, mddId);
1763          array_insert_last(int, fsm->fsmData.inputVars, mddId);
1764        }
1765      }
1766      st_free_table(mddIdTable);
1767      st_free_table(pseudoMddIdTable);
1768      array_free(supportMddIdArray);
1769    }
1770
1771    array_append(fsm->fsmData.globalPsVars, fsm->fsmData.presentStateVars);
1772    array_append(fsm->fsmData.globalPsVars, fsm->fsmData.pseudoInputVars);
1773  }
1774
1775  FsmCreateVariableCubes(fsm);
1776  fsm->fsmData.presentStateBddVars = mdd_id_array_to_bdd_array(
1777    Fsm_FsmReadMddManager(fsm), fsm->fsmData.presentStateVars);
1778  return (fsm);
1779}
1780
1781/**Function********************************************************************
1782
1783  Synopsis [Instantiate a given hint]
1784
1785  Description [Instantiate a given hint. The fwd and bwd flags
1786  indicate whether the fwd transition relation or the backward
1787  transition relation is created. A non-zero value will cause the hint
1788  to be instantiated in that direction.  The type flag indicates
1789  whether the hint should be applied as an overapproximation or an
1790  underapproximation.
1791
1792  After minimization wrt the hint is done, the TR is minimized wrt the
1793  conjunction of the care states in careStatesArray (an array of mdd_t *),
1794  unless this array is NULL, in which case it is ignored.]
1795
1796  SideEffects []
1797
1798  SeeAlso [Fsm_CleanUpHints]
1799
1800******************************************************************************/
1801void
1802Fsm_InstantiateHint(
1803  Fsm_Fsm_t *fsm,
1804  mdd_t *hint,
1805  int fwdFlag,
1806  int bwdFlag,
1807  Ctlp_Approx_t type,
1808  int printStatus)
1809{
1810  boolean underApprox = FALSE;
1811  Img_DirectionType imgFlag = Img_Forward_c;
1812
1813  assert(type != Ctlp_Incomparable_c);
1814 
1815  if (bwdFlag && fwdFlag)
1816    imgFlag = Img_Both_c;
1817  else if (bwdFlag)
1818    imgFlag = Img_Backward_c;
1819
1820  switch (type) {
1821  case (Ctlp_Underapprox_c): underApprox = TRUE; break;
1822  case (Ctlp_Overapprox_c): underApprox = FALSE; break;
1823  case (Ctlp_Exact_c):
1824    underApprox = TRUE;
1825    hint = mdd_one(Fsm_FsmReadMddManager(fsm));
1826    break;
1827  default: assert(0); break;
1828  }
1829  /* If we reach this point, underApprox has been explicitly assigned
1830   * by the switch. */
1831 
1832  Img_ImageConstrainAndClusterTransitionRelation(
1833    Fsm_FsmReadOrCreateImageInfo(fsm, bwdFlag, fwdFlag),
1834    imgFlag,
1835    hint,
1836    ((underApprox == TRUE) ?
1837     Img_GuidedSearchReadUnderApproxMinimizeMethod() :
1838     Img_GuidedSearchReadOverApproxMinimizeMethod()),
1839    underApprox, /* underapprox */
1840    0, /* dont clean up */
1841    0, /* no variable reordering */
1842    printStatus);
1843
1844  Fsm_MinimizeTransitionRelationWithReachabilityInfo(fsm, imgFlag,
1845                                                     printStatus); 
1846 
1847  if (type == Ctlp_Exact_c) mdd_free(hint);
1848
1849  return;
1850}
1851
1852/**Function********************************************************************
1853
1854  Synopsis [Clean up after hints]
1855
1856  Description [Clean up after hints.]
1857
1858  SideEffects []
1859
1860  SeeAlso [Fsm_InstantiateHint]
1861 
1862******************************************************************************/
1863void
1864Fsm_CleanUpHints( Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus)
1865{
1866  Img_DirectionType     imgFlag = Img_Forward_c;
1867  mdd_t *one = bdd_one(Fsm_FsmReadMddManager(fsm));
1868  if (bwdFlag && fwdFlag)
1869    imgFlag = Img_Both_c;
1870  else if (bwdFlag)
1871    imgFlag = Img_Backward_c;
1872
1873  Img_ImageConstrainAndClusterTransitionRelation(fsm->imageInfo,
1874                                                 imgFlag,
1875                                                 one,
1876                                                 Img_GuidedSearchReadUnderApproxMinimizeMethod(),
1877                                                 1, /* under approx */
1878                                                 1, /* clean up */
1879                                                 0, /* no variable reordering */
1880                                                 printStatus);
1881  mdd_free(one);
1882  return;
1883}
1884
1885
1886/**Function********************************************************************
1887
1888  Synopsis    [Frees the reachable states of an FSM.]
1889
1890  Description [Frees the reachable states of an FSM.]
1891
1892  SideEffects []
1893
1894  SeeAlso     [Fsm_FsmFree, Fsm_FsmFreeOverApproximateReachableStates]
1895
1896******************************************************************************/
1897void
1898Fsm_FsmFreeReachableStates(Fsm_Fsm_t *fsm)
1899{
1900  if (fsm->reachabilityInfo.reachableStates) {
1901    mdd_free(fsm->reachabilityInfo.reachableStates);
1902    fsm->reachabilityInfo.reachableStates = NIL(mdd_t);
1903  }
1904}
1905
1906/**Function********************************************************************
1907
1908  Synopsis    [Frees the approximate reachable states of an FSM.]
1909
1910  Description [Frees the approximate reachable states of an FSM.]
1911
1912  SideEffects []
1913
1914  SeeAlso     [Fsm_FsmFree, Fsm_FsmFreeReachableStates]
1915
1916******************************************************************************/
1917void
1918Fsm_FsmFreeOverApproximateReachableStates(Fsm_Fsm_t *fsm)
1919{
1920  if (fsm->reachabilityInfo.apprReachableStates) {
1921    mdd_array_free(fsm->reachabilityInfo.apprReachableStates);
1922    fsm->reachabilityInfo.apprReachableStates = NIL(array_t);
1923    fsm->reachabilityInfo.overApprox = Fsm_Ardc_NotConverged_c;
1924  }
1925  if (fsm->reachabilityInfo.subPsVars) {
1926    int i;
1927    array_t *psVars;
1928
1929    for (i = 0; i < array_n(fsm->reachabilityInfo.subPsVars); i++) {
1930      psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
1931      array_free(psVars);
1932    }
1933    array_free(fsm->reachabilityInfo.subPsVars);
1934    fsm->reachabilityInfo.subPsVars = NIL(array_t);
1935  }
1936}
1937
1938
1939/**Function********************************************************************
1940
1941  Synopsis    [Returns the reachable depth of an FSM.]
1942
1943  Description [Returns the reachable depth of an FSM.]
1944
1945  SideEffects []
1946
1947  SeeAlso     []
1948
1949******************************************************************************/
1950int
1951Fsm_FsmGetReachableDepth(Fsm_Fsm_t *fsm)
1952{
1953    return(fsm->reachabilityInfo.depth);
1954}
1955
1956/**Function********************************************************************
1957
1958  Synopsis [Checks if the 2 given fsms are the same, given that they
1959  are from the same total fsm. ]
1960
1961  Description [Checks if the 2 given fsms are the same, given that
1962  they are from the same total fsm. Compares present, next state,
1963  input, real present state and abstract variables. Also compares the
1964  next state function NAMES ONLY. Since the 2 fsms are guaranteed to
1965  be parts of te same total fsm and they share the same network, the
1966  mdds of next state function nodes with the same name are guaranteed
1967  to be the same. ]
1968
1969  SideEffects []
1970
1971  SeeAlso     []
1972
1973******************************************************************************/
1974boolean
1975Fsm_FsmCheckSameSubFsmInTotalFsm(Fsm_Fsm_t *fsm,
1976                                 Fsm_Fsm_t *subFsm1,
1977                                 Fsm_Fsm_t *subFsm2)
1978{
1979  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
1980  boolean result;
1981 
1982  assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm1));
1983  assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm2));
1984  assert(Fsm_FsmReadMddManager(subFsm1) == mddMgr);
1985  assert(Fsm_FsmReadMddManager(subFsm2) == mddMgr);
1986
1987  /* compare present state variables */
1988  result = VarIdArrayCompare(mddMgr,
1989                             Fsm_FsmReadPresentStateVars(subFsm1),
1990                             Fsm_FsmReadPresentStateVars(subFsm2));
1991  if (!result) return FALSE;
1992
1993  /* compare next state variables */
1994  result = VarIdArrayCompare(mddMgr,
1995                             Fsm_FsmReadNextStateVars(subFsm1),
1996                             Fsm_FsmReadNextStateVars(subFsm2));
1997  if (!result) return FALSE;
1998
1999  /* compare input variables */
2000  result = VarIdArrayCompare(mddMgr,
2001                             Fsm_FsmReadInputVars(subFsm1),
2002                             Fsm_FsmReadInputVars(subFsm2));
2003  if (!result) return FALSE;
2004
2005  /* compare the pseudo input variables */
2006  result = VarIdArrayCompare(mddMgr,
2007                             Fsm_FsmReadPseudoInputVars(subFsm1),
2008                             Fsm_FsmReadPseudoInputVars(subFsm2));
2009  if (!result) return FALSE;
2010
2011  /* compare next state functions */
2012  result = NSFunctionNamesCompare(mddMgr,
2013                                  Fsm_FsmReadNextStateFunctionNames(subFsm1),
2014                                  Fsm_FsmReadNextStateFunctionNames(subFsm2));
2015  if (!result) return FALSE;
2016
2017  return TRUE;
2018}
2019
2020/**Function********************************************************************
2021
2022  Synopsis    [Returns whether reachability analysis was an approximation or
2023  exact.]
2024
2025  Description [Returns whether reachability analysis was an approximation or
2026  exact.]
2027
2028  SideEffects []
2029
2030  SeeAlso     []
2031
2032******************************************************************************/
2033Fsm_RchStatus_t
2034Fsm_FsmReadReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm)
2035{
2036  return fsm->reachabilityInfo.rchStatus;
2037}
2038
2039/**Function********************************************************************
2040
2041  Synopsis    [Minimize the transition relation wrt either ARDCs or exact
2042  reachability information]
2043
2044  Description [Prefers exact rdcs when available, if neither exact nor
2045  approximate rdcs are availablem, the TR is not touched.]
2046
2047  SideEffects []
2048
2049  SeeAlso     []
2050
2051******************************************************************************/
2052void
2053Fsm_MinimizeTransitionRelationWithReachabilityInfo(
2054  Fsm_Fsm_t *fsm,
2055  Img_DirectionType fwdbwd,
2056  boolean verbosity)
2057{
2058  Img_ImageInfo_t *imageInfo;
2059  array_t *minimizeArray = NIL(array_t);
2060  boolean fwd            = FALSE;
2061  boolean bwd            = FALSE;
2062  int     oldVerbosity;
2063  Fsm_RchStatus_t status;
2064  boolean  freeArray;
2065  mdd_t *exactrdc;
2066 
2067  switch (fwdbwd) {
2068  case Img_Forward_c:
2069    fwd = 1;
2070    break;
2071  case Img_Backward_c:
2072    bwd = 1;
2073    break;
2074  case Img_Both_c:
2075    fwd = 1;
2076    bwd= 1;
2077    break;
2078  default:
2079    assert(0);
2080    break;
2081  }
2082 
2083  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd);
2084  oldVerbosity = Img_ReadPrintMinimizeStatus(imageInfo);
2085 
2086  status = Fsm_FsmReadReachabilityApproxComputationStatus(fsm);
2087  exactrdc = Fsm_FsmReadCurrentReachableStates(fsm);
2088 
2089  if((status == Fsm_Rch_Exact_c || status == Fsm_Rch_Over_c) &&
2090     exactrdc != NIL(mdd_t) ){
2091    freeArray = TRUE;
2092    minimizeArray = array_alloc(mdd_t *, 1);
2093    array_insert_last(mdd_t *, minimizeArray, mdd_dup(exactrdc)); 
2094  }else{
2095    freeArray = FALSE;
2096    minimizeArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
2097    if(minimizeArray == NIL(array_t))
2098      return;
2099  }
2100
2101  if(verbosity)
2102    Img_SetPrintMinimizeStatus(imageInfo, 1);
2103
2104  /* We never reorder the clusters of the iwls structure.  It is probably
2105     better to reorder them, but as this is written, there is no time to
2106     evaluate the effect of reordering. */
2107    Img_MinimizeTransitionRelation(imageInfo, minimizeArray,
2108                                 Img_DefaultMinimizeMethod_c, fwdbwd, FALSE);
2109 
2110  if(verbosity)
2111    Img_SetPrintMinimizeStatus(imageInfo, oldVerbosity);
2112
2113  if(freeArray)
2114    mdd_array_free(minimizeArray);
2115
2116  return;
2117}
2118
2119
2120
2121/*---------------------------------------------------------------------------*/
2122/* Definition of internal functions                                          */
2123/*---------------------------------------------------------------------------*/
2124
2125/**Function********************************************************************
2126
2127  Synopsis    [Sets array of onion rings from reachability computation]
2128
2129  Description [Sets array of onion rings from reachability
2130  computation.]
2131
2132  SideEffects []
2133
2134  SeeAlso     [Fsm_FsmReadReachabilityOnionRings]
2135
2136******************************************************************************/
2137void
2138FsmSetReachabilityOnionRings(
2139  Fsm_Fsm_t *fsm, array_t *onionRings)
2140{
2141  fsm->reachabilityInfo.onionRings = onionRings;
2142}
2143
2144/**Function********************************************************************
2145
2146  Synopsis    [Sets whether  onion rings are due to BFS.]
2147
2148  Description [Sets whether onion rings are due to BFS.]
2149
2150  SideEffects []
2151
2152  SeeAlso     [Fsm_FsmReadReachabilityOnionRingsMode]
2153
2154******************************************************************************/
2155void
2156FsmSetReachabilityOnionRingsMode(
2157  Fsm_Fsm_t *fsm, Fsm_RchType_t value)
2158{
2159  fsm->reachabilityInfo.onionRingsMode = value;
2160}
2161
2162/**Function********************************************************************
2163
2164  Synopsis    [Sets whether  onion rings are up to date.]
2165
2166  Description [Sets whether  onion rings are up to date.]
2167
2168  SideEffects []
2169
2170  SeeAlso     [Fsm_FsmReachabilityOnionRingsUpToDate]
2171
2172******************************************************************************/
2173void
2174FsmSetReachabilityOnionRingsUpToDateFlag(
2175  Fsm_Fsm_t *fsm,  boolean value)
2176{
2177  fsm->reachabilityInfo.onionRingsUpToDate = value;
2178}
2179
2180/**Function********************************************************************
2181
2182  Synopsis    [Sets whether reachability analysis was an approximation.]
2183
2184  Description [Sets whether reachability analysis was an approximation.]
2185
2186  SideEffects []
2187
2188  SeeAlso     []
2189
2190******************************************************************************/
2191void
2192FsmSetReachabilityApproxComputationStatus(
2193  Fsm_Fsm_t *fsm,  Fsm_RchStatus_t value)
2194{
2195  fsm->reachabilityInfo.rchStatus = value;
2196}
2197
2198/**Function********************************************************************
2199
2200  Synopsis    [Sets the status of overapproxiate reachable computation.]
2201
2202  Description [Sets the status of overapproxiate reachable computation.]
2203
2204  SideEffects []
2205
2206  SeeAlso     []
2207
2208******************************************************************************/
2209void
2210FsmSetReachabilityOverApproxComputationStatus(
2211  Fsm_Fsm_t *fsm,  Fsm_Ardc_StatusType_t status)
2212{
2213  fsm->reachabilityInfo.overApprox = status;
2214}
2215
2216/**Function********************************************************************
2217
2218  Synopsis    [Reads the status of overapproxiate reachable computation.]
2219
2220  Description [Reads the status of overapproxiate reachable computation.]
2221
2222  SideEffects []
2223
2224  SeeAlso     []
2225
2226******************************************************************************/
2227Fsm_Ardc_StatusType_t
2228FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm)
2229{
2230  return(fsm->reachabilityInfo.overApprox);
2231}
2232
2233/**Function********************************************************************
2234
2235  Synopsis [Sets the mode field to indicate whether computation has
2236  always been BFS.]
2237
2238  Description [Sets the mode field to indicate whether computation has
2239  always been BFS.]
2240
2241  SideEffects []
2242
2243  SeeAlso     []
2244
2245******************************************************************************/
2246void
2247FsmSetReachabilityComputationMode(
2248  Fsm_Fsm_t *fsm,  Fsm_RchType_t value)
2249{
2250  fsm->reachabilityInfo.reachabilityMode = value;
2251}
2252
2253/**Function********************************************************************
2254
2255  Synopsis [Reads the mode field to indicate whether computation has
2256  always been BFS.]
2257
2258  Description [Reads the mode field to indicate whether computation has
2259  always been BFS.]
2260
2261  SideEffects []
2262
2263  SeeAlso     []
2264
2265******************************************************************************/
2266Fsm_RchType_t
2267FsmReadReachabilityComputationMode(
2268  Fsm_Fsm_t *fsm)
2269{
2270  return fsm->reachabilityInfo.reachabilityMode;
2271}
2272
2273
2274/**Function********************************************************************
2275
2276  Synopsis [Reset fsm fields]
2277
2278  Description [Reset fsm fields. Free reachable states, onion rings.
2279  Reset the onion ring up-to-date flag, onion rings BFS, depth and
2280  under approximation flag.]
2281
2282  SideEffects []
2283
2284******************************************************************************/
2285void
2286FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag)
2287{
2288  int i;
2289  mdd_t *reachableStates;
2290  /* free reachable states if it is necessary to recompute anyway. */
2291  if (approxFlag != Fsm_Rch_Oa_c) {
2292    if (Fsm_FsmReadCurrentReachableStates(fsm)) {
2293      Fsm_FsmFreeReachableStates(fsm);
2294    }
2295  } else if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) {
2296    Fsm_FsmFreeOverApproximateReachableStates(fsm);
2297  }
2298       
2299  /* free onion rings */
2300  if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) {
2301    arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm), i,
2302        reachableStates) {
2303      mdd_free(reachableStates);
2304    }
2305    array_free(Fsm_FsmReadReachabilityOnionRings(fsm));
2306    FsmSetReachabilityOnionRings(fsm, NIL(array_t));
2307  }
2308  fsm->reachabilityInfo.depth = 0;
2309  FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c);
2310  FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c);
2311  FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
2312  FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c);
2313  return;
2314} /* end of FsmResetReachabilityFields */
2315
2316
2317/*---------------------------------------------------------------------------*/
2318/* Definition of internal functions                                          */
2319/*---------------------------------------------------------------------------*/
2320/**Function********************************************************************
2321
2322  Synopsis    [Allocates HD Info structure.]
2323
2324  Description [Allocates HD Info structure.]
2325
2326  SideEffects []
2327
2328  SeeAlso     [Fsm_FsmHdStructFree]
2329
2330******************************************************************************/
2331FsmHdStruct_t *
2332FsmHdStructAlloc(int nvars)
2333{
2334  FsmHdStruct_t *hdInfo = ALLOC(FsmHdStruct_t, 1);
2335  if (hdInfo == NIL(FsmHdStruct_t)) return hdInfo;
2336  hdInfo->numDeadEnds = 0;
2337  hdInfo->firstSubset = TRUE;
2338  hdInfo->lastIter = -1;
2339  hdInfo->partialImage = FALSE;
2340  hdInfo->residueCount = 0;
2341  hdInfo->interiorStates = NIL(mdd_t);
2342  hdInfo->interiorStateCandidate = NIL(mdd_t);
2343  hdInfo->deadEndResidue = NIL(mdd_t);
2344  hdInfo->options = Fsm_FsmHdGetTravOptions(nvars);
2345  hdInfo->stats = FsmHdStatsStructAlloc();
2346  hdInfo->imageOfReachedComputed = FALSE;
2347  hdInfo->onlyPartialImage = FALSE;
2348  hdInfo->slowGrowth = 0;
2349  hdInfo->deadEndWithOriginalTR = FALSE;
2350  hdInfo->deadEndComputation = FALSE;
2351  return hdInfo;
2352}
2353
2354
2355/**Function********************************************************************
2356
2357  Synopsis    [Frees HD info struct.]
2358
2359  Description [Frees HD info struct.]
2360
2361  SideEffects []
2362
2363  SeeAlso     [Fsm_FsmHdStructAllocate]
2364
2365******************************************************************************/
2366void
2367FsmHdStructFree(FsmHdStruct_t *hdInfo)
2368{
2369  if (hdInfo->interiorStates != NULL) mdd_free(hdInfo->interiorStates);
2370  if (hdInfo->interiorStateCandidate != NULL)
2371    mdd_free(hdInfo->interiorStateCandidate);
2372  if (hdInfo->deadEndResidue != NULL) mdd_free(hdInfo->deadEndResidue);
2373 
2374  FsmHdStatsStructFree(hdInfo->stats);
2375  Fsm_FsmHdFreeTravOptions(hdInfo->options);
2376  FREE(hdInfo);
2377  return;
2378}
2379
2380/**Function********************************************************************
2381
2382  Synopsis    [Prints all options that are related to guided search.]
2383
2384  Description [Prints all options that are related to guided search.]
2385
2386  SideEffects []
2387
2388  SeeAlso     [CommandGuidedSearchOptions]
2389
2390******************************************************************************/
2391void
2392FsmGuidedSearchPrintOptions(void)
2393{
2394  char *string =  Cmd_FlagReadByName("guided_search_hint_type");
2395  if (string == NIL(char)) string = "local";
2396  fprintf(vis_stdout, "Flag guided_search_hint_type is set to %s.\n", string);
2397  string = Cmd_FlagReadByName("guided_search_underapprox_minimize_method");
2398  if (string == NIL(char)) string = "and";
2399  fprintf(vis_stdout, "Flag guided_search_underapprox_minimize_method is set to %s.\n", string);
2400  string = Cmd_FlagReadByName("guided_search_overapprox_minimize_method");
2401  if (string == NIL(char)) string = "ornot";
2402  fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string);
2403  string = Cmd_FlagReadByName("guided_search_sequence");
2404  if (string == NIL(char)) string = "all hints to convergence";
2405  fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string);
2406  return;
2407}
2408
2409
2410
2411/*---------------------------------------------------------------------------*/
2412/* Definition of static functions                                          */
2413/*---------------------------------------------------------------------------*/
2414/**Function********************************************************************
2415
2416  Synopsis    [Allocates structure]
2417
2418  Description [Allocates structure]
2419
2420  SideEffects []
2421
2422  SeeAlso     []
2423
2424******************************************************************************/
2425static Fsm_Fsm_t *
2426FsmStructAlloc(Ntk_Network_t *network,
2427            graph_t     *partition)
2428{
2429  Fsm_Fsm_t *fsm;
2430  if (Ntk_NetworkReadNumLatches(network) == 0) {
2431    error_append("Network has no latches. Cannot create FSM.");
2432    return (NIL(Fsm_Fsm_t));
2433  }
2434 
2435  fsm = ALLOC(Fsm_Fsm_t, 1);
2436  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
2437  memset(fsm, 0, sizeof(Fsm_Fsm_t));
2438
2439  fsm->network = network;
2440
2441  if (partition == NIL(graph_t)) {
2442    partition = Part_NetworkReadPartition(network);
2443
2444    if (partition == NIL(graph_t)) {
2445      error_append("Network has no partition. Cannot create FSM.");
2446      return (NIL(Fsm_Fsm_t));
2447    } else {
2448      fsm->partition = Part_PartitionDuplicate(partition);
2449    }
2450  } else {
2451    fsm->partition = partition;
2452  }
2453 
2454  FsmSetReachabilityOnionRings(fsm, NIL(array_t));
2455  FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
2456  FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c);
2457  FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c);
2458  FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c);
2459  FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
2460
2461  fsm->fsmData.presentStateVars   = array_alloc(int, 0);
2462  fsm->fsmData.nextStateVars      = array_alloc(int, 0);
2463  fsm->fsmData.inputVars          = array_alloc(int, 0);
2464  fsm->fsmData.nextStateFunctions = array_alloc(char *, 0);
2465
2466  return (fsm);
2467} /* end of FsmStructAlloc */
2468
2469
2470/**Function********************************************************************
2471
2472  Synopsis    [Allocates structure]
2473
2474  Description [Allocates structure]
2475
2476  SideEffects []
2477
2478  SeeAlso     []
2479
2480******************************************************************************/
2481static void
2482FsmCreateVariableCubes(Fsm_Fsm_t *fsm)
2483{
2484  mdd_manager *manager = Fsm_FsmReadMddManager(fsm);
2485  char *flagValue;
2486  boolean createVariableCubesFlag = TRUE;
2487
2488  if (bdd_get_package_name() != CUDD)
2489    return;
2490
2491  flagValue = Cmd_FlagReadByName("fsm_create_var_cubes");
2492  if (flagValue != NIL(char)) {
2493    if (strcmp(flagValue, "yes") == 0)
2494      createVariableCubesFlag = TRUE;
2495    else if (strcmp(flagValue, "no") == 0)
2496      createVariableCubesFlag = FALSE;
2497    else {
2498      fprintf(vis_stderr,
2499        "** ardc error : invalid value %s for create_var_cubes[yes/no]. **\n",
2500        flagValue);
2501    }
2502  }
2503
2504  if (!createVariableCubesFlag)
2505    return;
2506
2507  fsm->fsmData.createVarCubesFlag = TRUE;
2508  fsm->fsmData.presentStateCube =
2509        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.presentStateVars);
2510  fsm->fsmData.nextStateCube =
2511        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.nextStateVars);
2512  fsm->fsmData.inputCube =
2513        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.inputVars);
2514  if (fsm->fsmData.pseudoInputVars) {
2515    fsm->fsmData.pseudoInputCube =
2516        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.pseudoInputVars);
2517  }
2518  if (fsm->fsmData.primaryInputVars) {
2519    fsm->fsmData.primaryInputCube =
2520        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.primaryInputVars);
2521  }
2522  if (fsm->fsmData.globalPsVars) {
2523    fsm->fsmData.globalPsCube =
2524        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.globalPsVars);
2525  }
2526}
2527
2528
2529/**Function********************************************************************
2530
2531  Synopsis    [Compare procedure for name comparison.]
2532
2533  Description [Compare procedure for name comparison.]
2534
2535  SideEffects []
2536
2537******************************************************************************/
2538static int
2539nameCompare(
2540  const void * name1,
2541  const void * name2)
2542{
2543    return(strcmp(*(char **)name1, *(char **)name2));
2544
2545} /* end of signatureCompare */
2546
2547
2548/**Function********************************************************************
2549
2550  Synopsis    [ Checks that 2 arrays of variables ids are the same.]
2551
2552  Description [ Checks that 2 arrays of variables ids are the same by
2553  computing the bdd of the cube.]
2554 
2555  SideEffects []
2556
2557  SeeAlso     [Fsm_FsmCheckSameSubFsmInTotalFsm]
2558
2559******************************************************************************/
2560static boolean
2561VarIdArrayCompare(mdd_manager *mddMgr,
2562                  array_t *vars1,
2563                  array_t *vars2)
2564{
2565 
2566  mdd_t *cube1, *cube2;
2567  boolean result = FALSE;
2568  cube1 = bdd_compute_cube(mddMgr, vars1);
2569  cube2 = bdd_compute_cube(mddMgr, vars2);
2570  if ((cube1 == NIL(mdd_t)) || (cube2 == NIL(mdd_t))) {
2571    result = (cube1 == cube2) ? TRUE : FALSE;
2572  } else {
2573    result =  bdd_equal(cube1, cube2) ? TRUE : FALSE;
2574  }
2575  if (cube1 != NIL(bdd_t)) bdd_free(cube1);
2576  if (cube2 != NIL(bdd_t)) bdd_free(cube2);
2577  return result;
2578} /* end of VarIdArrayCompare */
2579
2580
2581/**Function********************************************************************
2582
2583  Synopsis    [ Checks that 2 arrays of variables ids are the same.]
2584
2585  Description [ Checks that 2 arrays of variables ids are the same by
2586  computing the bdd of the cube.]
2587 
2588  SideEffects []
2589
2590  SeeAlso     [Fsm_FsmCheckSameSubFsmInTotalFsm]
2591
2592******************************************************************************/
2593static boolean
2594NSFunctionNamesCompare(mdd_manager *mddMgr,
2595                       array_t *names1,
2596                       array_t *names2)
2597{
2598  int sizeArray = array_n(names1);
2599  int i, count;
2600  char *name;
2601  st_table *nameTable = st_init_table(strcmp, st_strhash);
2602
2603  if (sizeArray != array_n(names2)) return FALSE;
2604  /* check if elements in names2 is in names1 */
2605  arrayForEachItem(char *, names1, i, name) {
2606    if (st_lookup_int(nameTable, name, &count)) {
2607      count++;
2608    } else {
2609      count = 1;
2610    }
2611    st_insert(nameTable, name, (char *)(long)count);
2612  }
2613 
2614  arrayForEachItem(char *, names2, i, name) {
2615    if (!st_lookup_int(nameTable, name, &count)) {
2616      st_free_table(nameTable);
2617      return FALSE;
2618    } else if (count == 0) { 
2619      st_free_table(nameTable);
2620      return FALSE;
2621    } else {
2622      count--;
2623      st_insert(nameTable, name, (char *)(long)count);   
2624    }
2625  }
2626  st_free_table(nameTable);
2627
2628  /* check if elements in names1 is in names2 */
2629  nameTable = st_init_table(strcmp, st_strhash);
2630  arrayForEachItem(char *, names2, i, name) {
2631    if (st_lookup_int(nameTable, name, &count)) {
2632      count++;
2633    } else {
2634      count = 1;
2635    }
2636    st_insert(nameTable, name, (char *)(long)count);
2637  }
2638 
2639  arrayForEachItem(char *, names1, i, name) {
2640    if (!st_lookup_int(nameTable, name, &count)) {
2641      st_free_table(nameTable);
2642      return FALSE;
2643    } else if (count == 0) { 
2644      st_free_table(nameTable);
2645      return FALSE;
2646    } else {
2647      count--;
2648      st_insert(nameTable, name, (char *)(long)count);   
2649    }
2650  }
2651  st_free_table(nameTable);
2652  return TRUE;
2653} /* end of NSFunctionNamesCompare */
2654
2655
2656/**Function********************************************************************
2657
2658  Synopsis    [Returns an array of mdd Ids of an FSM.]
2659
2660  Description [Returns an array of mdd Ids of an FSM.]
2661 
2662  SideEffects []
2663
2664  SeeAlso     []
2665
2666******************************************************************************/
2667static array_t *
2668GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable,
2669                     st_table *pseudoMddIdTable)
2670{
2671  mdd_t                 *func;
2672  char                  *nodeName;
2673  vertex_t              *vertex;
2674  Mvf_Function_t        *mvf;
2675  int                   i, j, k;
2676  long                  mddId;
2677  array_t               *varBddFunctionArray;
2678  mdd_manager           *mddManager;
2679  array_t               *supportMddIdArray, *support;
2680  st_table              *supportMddIdTable;
2681  st_generator          *stGen;
2682
2683  supportMddIdTable = st_init_table(st_numcmp, st_numhash);
2684  mddManager = Part_PartitionReadMddManager(fsm->partition);
2685
2686  for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i++) {
2687    nodeName = array_fetch(char*, fsm->fsmData.nextStateFunctions, i);
2688    vertex = Part_PartitionFindVertexByName(fsm->partition, nodeName);
2689    mvf = Part_VertexReadFunction(vertex);
2690    mddId = (long) array_fetch(int, fsm->fsmData.nextStateVars, i);
2691    varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager,
2692                                                       (int) mddId, mvf);
2693
2694    for (j = 0; j < array_n(varBddFunctionArray); j++) {
2695      func = array_fetch(mdd_t *, varBddFunctionArray, j);
2696      support = mdd_get_support(mddManager, func);
2697      arrayForEachItem(int, support, k, mddId) {
2698        if (!st_lookup(supportMddIdTable, (char *)mddId, NIL(char *))) {
2699          if (st_lookup(mddIdTable, (char *)mddId, NIL(char *)) ||
2700              st_lookup(pseudoMddIdTable, (char *)mddId, NIL(char *))) {
2701            st_insert(supportMddIdTable, (char *)mddId, NIL(char));
2702          } else { /* intermediate variables */
2703            /* NEEDS to get the supports of an intermediate variable */
2704            assert(0);
2705          }
2706        }
2707      }
2708    }
2709    array_free(varBddFunctionArray);
2710  }
2711
2712  supportMddIdArray = array_alloc(int, 0);
2713  st_foreach_item(supportMddIdTable, stGen, &mddId, NIL(char *)) {
2714    array_insert_last(int, supportMddIdArray, (int) mddId);
2715  }
2716
2717  return(supportMddIdArray);
2718}
2719
2720
Note: See TracBrowser for help on using the repository browser.