source: vis_dev/vis-2.3/src/ltl/ltlCompose.c @ 43

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

vis2.3
File size: 51.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltlCompose.c]
4
5  PackageName [ltl]
6
7  Synopsis    [Write the Buechi automaton into a file.]
8
9  Author      [Chao Wang<chao.wang@colorado.EDU>]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "ltlInt.h"
18
19static char rcsid[] UNUSED = "$Id: ltlCompose.c,v 1.30 2005/04/28 08:51:19 bli Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Structure declarations                                                    */
27/*---------------------------------------------------------------------------*/
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Variable declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37/*---------------------------------------------------------------------------*/
38/* Macro declarations                                                        */
39/*---------------------------------------------------------------------------*/
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static void AutomatonGetInputNames(Ltl_Automaton_t *A, array_t *InputNames, array_t *Name2LabelIdx);
48static int AutomatonCountSelector(Ltl_Automaton_t *A);
49static int AutomatonComputeInitState(Ltl_Automaton_t *A);
50/*static lsList AutomatonLabelGetCubes(Ltl_Automaton_t *A, LtlSet_t *compositeLabel, Ntk_Network_t *network);*/
51static lsList GetCubes_Aux(Ltl_Automaton_t *A, int index);
52static char * StringNormalize(char *inputString);
53static void AutomatonVtxLabelToBlifMv(FILE *fp, Ltl_Automaton_t *A, vertex_t *vtx);
54static void VtxLabelToBlifMv_Aux(FILE *fp, Ltl_Automaton_t *A, int node_idx, int index, st_table *CreatedSignals);
55
56/**AutomaticEnd***************************************************************/
57   
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62/**Function********************************************************************
63
64  Synopsis    [Translate the Automaton into Dot format.]
65
66  Description []
67
68  SideEffects []
69
70  SeeAlso     []
71
72******************************************************************************/
73void
74Ltl_AutomatonToDot(
75  FILE *fp,
76  Ltl_Automaton_t *aut,
77  int level)
78{
79  edge_t   *edge;
80  vertex_t *vtx1, *vtx2;         
81  Ltl_AutomatonNode_t *node, *node2;
82  lsGen     lsgen, lsgen2;
83  st_table  *FairSet;
84  st_generator *stgen;
85  Ctlsp_Formula_t *F;
86  char *tmpString;
87  int fairindex, first, i, n;
88 
89  /*-------------------------------------------------
90   * digraph "G(F(p=1))" {
91   * node [shape=ellipse];
92   * size = "7.5,10"
93   * center = true;
94   * "title" [label="G(F(p=1))", shape=plaintext];
95   *-------------------------------------------------
96   */
97  if (aut->name)
98    tmpString = aut->name;
99  else
100    tmpString = "";
101 
102  fprintf(fp, "\ndigraph \"%s\" {\nnode [shape=ellipse];\nsize = \"7.5,10\"\ncenter = true;\n\"title\" [label=\"%s\",shape=plaintext];", tmpString, tmpString);
103 
104  /*-------------------------------------------------
105   * "n1" [label="n1\n{p=1}\n(1)"];
106   *-------------------------------------------------
107   */
108  foreach_vertex( aut->G, lsgen, vtx1) {
109    node = (Ltl_AutomatonNode_t *)vtx1->user_data;
110    fprintf(fp,"\n\"n%d\" [label=\"n%d\\n{", node->index, node->index);
111    if (node->Labels) {
112      first = 1; n = array_n(aut->labelTable);
113      for (i=0; i<n; i++) {
114        if (LtlSetGetElt(node->Labels, i)) {
115          if (!first)     fprintf(fp, ",");
116          else            first = 0;
117          F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i);
118          Ctlsp_FormulaPrint(fp, F);
119        }
120      }
121    }
122    fprintf(fp, "}\\n(");
123    fairindex = 1;
124    lsForEachItem(aut->Fair, lsgen2, FairSet) {
125      if (st_is_member(FairSet, vtx1))
126        fprintf(fp, " %d ", fairindex);
127      fairindex++;
128    }
129    fprintf(fp, ")\"];");
130  }
131
132  /*-------------------------------------------------
133   * "init-n2" [style=invis]
134   * "init-n2" -> "n2";
135   *-------------------------------------------------
136   */
137  st_foreach_item(aut->Init, stgen, &vtx1, NIL(char *)) {
138    node = (Ltl_AutomatonNode_t *) vtx1->user_data;
139    fprintf(fp, "\n\"init-n%d\" [style=invis]", node->index);
140    fprintf(fp, "\n\"init-n%d\" -> \"n%d\";", node->index, node->index);
141  }
142
143
144  /*-------------------------------------------------
145   * "n1" -> "n1";
146   *-------------------------------------------------
147   */
148  foreach_edge(aut->G, lsgen, edge) {
149    vtx1 = g_e_source(edge);
150    vtx2 = g_e_dest(edge);
151    node = (Ltl_AutomatonNode_t *) vtx1->user_data;
152    node2 = (Ltl_AutomatonNode_t *) vtx2->user_data;
153    fprintf(fp, "\n\"n%d\" -> \"n%d\";", node->index, node2->index);
154  }
155  fprintf(fp, "\n}\n");
156}
157
158
159/**Function********************************************************************
160   
161  Synopsis    [Translate the automaton to a BlifMv file.]
162 
163  Description [The Hrc_Manager may or may not be provided. If not, the blifmv
164  file generated is not complete (all the inputs are assummed to be boolean).
165 
166  Notice that the labels on each state are propositional subformulae, not
167  necessarily atomic propositions.]
168 
169  SideEffects []
170 
171  SeeAlso     []
172
173******************************************************************************/
174int
175Ltl_AutomatonToBlifMv(
176  FILE *fp,             
177  Ntk_Network_t *network,
178  Ltl_Automaton_t *A)     
179{
180  Var_Variable_t *inputVar;
181  array_t *InputNames = array_alloc(char *, 0);
182  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
183  Ntk_Node_t *ntknode;
184  char *inputName;
185  st_generator *stgen;
186  lsGen lsgen, lsgen2;
187  int i, j, is_enum, range;
188  int sel_num, sel_cnt;
189  edge_t *edge;
190  vertex_t *vtx, *vtx2;
191  st_table *FairSet, *tmptbl;
192  int InitIdx = AutomatonComputeInitState(A);
193  char InitStr[10];
194  int result = 1;
195  array_t *labelArray;
196 
197  /* The initState of the automaton */
198  if (InitIdx == -1) 
199    sprintf(InitStr, "Init");
200  else
201    sprintf(InitStr, "n%d", InitIdx);
202 
203  if (network == NIL(Ntk_Network_t)) {
204    result = 0;
205    fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n");
206  }
207
208  /* Retrieve all the input names on the labels; For each input, create a
209   *  hash table and add all the label subformulae contains that input;
210   *  Finally, calculate the size of the "selector"
211   */
212  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
213  sel_num = AutomatonCountSelector(A);
214  fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name);
215 
216  /*-------------------------------------------------------
217   * .model Buechi$AUT
218   * .root  Buechi$AUT
219   *-------------------------------------------------------
220   */
221   fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT");
222 
223   /*-------------------------------------------------------
224    * .inputs in1 in2 in3 ... inN
225    *-------------------------------------------------------
226    */
227   fprintf(fp, "\n.inputs ");
228   for (i=0; i<array_n(InputNames); i++) {
229     inputName = array_fetch(char *, InputNames, i);
230     fprintf(fp, "%s ", inputName);
231   }
232
233   /*-------------------------------------------------------
234    * .outputs fair1 fair2 fair3... fairN
235    *-------------------------------------------------------
236    */
237   fprintf(fp, "\n.outputs ");
238   if ( lsLength(A->Fair) != 0) {
239     for (i=0; i<lsLength(A->Fair); i++) {
240       fprintf(fp, "fair%d$AUT ", i+1);
241     }
242   }else
243     fprintf(fp, "fair1$AUT");
244
245   /*-------------------------------------------------------
246    * .mv in1 3 RED GREEN YELLOW
247    *-------------------------------------------------------
248    */
249   if (network != NIL(Ntk_Network_t)) {
250     for (i=0; i<array_n(InputNames); i++) {
251       inputName = array_fetch(char *, InputNames, i);
252       ntknode = Ntk_NetworkFindNodeByName(network, inputName);
253       assert(ntknode != NIL(Ntk_Node_t));
254       inputVar = Ntk_NodeReadVariable(ntknode);
255       is_enum = Var_VariableTestIsEnumerative(inputVar);
256       range = Var_VariableReadNumValues(inputVar);
257       if (is_enum) {
258         if (range != 2) 
259           fprintf(fp, "\n.mv %s %d\n", inputName, range);
260       }else {
261         fprintf(fp, "\n.mv %s %d ", inputName, range);
262         for (j=0; j<range; j++) {
263           fprintf(fp, "%s ",
264                   Var_VariableReadSymbolicValueFromIndex(inputVar,j));
265         }
266       }
267     }
268   }
269
270   /*------------------------------------------------------- 
271    * .mv stateD$AUT N Init n1 n2 n3 ... nN
272    * .mv state$AUT  N Init n1 n2 n3 ... nN
273    *-------------------------------------------------------
274    */
275   if (InitIdx == -1) 
276     fprintf(fp, "\n.mv stateD$AUT %d Init Trap ",
277             lsLength(g_get_vertices(A->G)) + 2);
278   else
279     fprintf(fp, "\n.mv stateD$AUT %d Trap ",
280             lsLength(g_get_vertices(A->G)) + 1);
281   foreach_vertex(A->G, lsgen, vtx) {
282     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
283   }
284   if (InitIdx == -1)
285     fprintf(fp, "\n.mv state$AUT %d Init Trap ",
286             lsLength(g_get_vertices(A->G)) + 2);
287   else
288     fprintf(fp, "\n.mv state$AUT %d Trap ",
289             lsLength(g_get_vertices(A->G)) + 1);
290   foreach_vertex(A->G, lsgen, vtx) { 
291     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
292   }
293
294   /*-------------------------------------------------------
295    * .mv selector n
296    * .table selector
297    * -
298    *-------------------------------------------------------
299    */
300   if (sel_num > 1) 
301     fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num);
302
303   /*-------------------------------------------------------
304    * for each state label, create a signal n1_##_label$AUT (recursively)
305    *-------------------------------------------------------
306    */
307   labelArray = array_alloc(vertex_t *, 0);
308   foreach_vertex(A->G, lsgen, vtx) {
309     AutomatonVtxLabelToBlifMv(fp, A, vtx);
310     array_insert_last(vertex_t *, labelArray, vtx);
311   }
312   
313   /*------------------------------------------------------- 
314    * .latch stateD$AUT state$AUT
315    * .reset state$AUT
316    * Init (or ns)
317    *-------------------------------------------------------
318    */
319   fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s",
320           InitStr);
321
322
323   /*------------------------------------------------------
324    * .table selector$AUT state$AUT n1_label$AUT n2_label... -> stateD$AUT
325    * .default Trap
326    * 0 1 0 0 ... n1
327    * 1 0 1       n2
328    * ...
329    *------------------------------------------------------
330    */
331   if (sel_num >1)
332     fprintf(fp, "\n.table selector$AUT state$AUT ");
333   else
334     fprintf(fp, "\n.table state$AUT ");
335
336   arrayForEachItem(vertex_t *, labelArray, i, vtx) {
337     fprintf(fp, "n%d_label$AUT ", Ltl_AutomatonVtxGetNodeIdx(vtx));
338   }
339   fprintf(fp, " -> stateD$AUT\n.default Trap");
340
341   if (InitIdx == -1) {
342     sel_cnt = 0;
343     arrayForEachItem(vertex_t *, labelArray, i, vtx) {
344       if (!st_is_member(A->Init, vtx))
345         continue;
346       if (sel_num > 1) {
347         if (st_count(A->Init) == 1) 
348           fprintf(fp, "\n- Init ");
349         else
350           fprintf(fp, "\n%d Init ", sel_cnt);
351       }else
352         fprintf(fp, "\nInit ");
353       
354       for(j=0; j<array_n(labelArray); j++)
355         fprintf(fp, "%s ", ((i==j)?"1":"-"));
356
357       fprintf(fp, "   n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
358
359       if (sel_num > 1)
360         sel_cnt++;
361     }
362   }
363
364   /* for each edge (n1, n2) with n2 labeled n2_label$AUT, add entry:
365    *-------------------------------------------------------     
366    * selector 1 0 0  ...     n1
367    * selector 0 1 0  ...     n2
368    * ...
369    *-------------------------------------------------------
370    */
371   foreach_vertex(A->G, lsgen, vtx) {
372     int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
373     int outDegree = lsLength(g_get_out_edges(vtx));
374     sel_cnt = 0;
375     foreach_out_edge(vtx, lsgen2, edge) {
376       int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
377
378       if (sel_num > 1) {
379         if (outDegree == 1) 
380           fprintf(fp, "\n- n%d ", n1);
381         else
382           fprintf(fp, "\n%d n%d ", sel_cnt, n1);
383       }else {
384         fprintf(fp, "\nn%d ", n1);
385       }
386       
387       arrayForEachItem(vertex_t *, labelArray, i, vtx2) {
388         fprintf(fp, "%s ", ((vtx2 == g_e_dest(edge))?"1":"-"));
389       }
390       fprintf(fp, "   n%d", n2);
391         
392       if (sel_num > 1)
393         sel_cnt++;
394     }
395   }
396   array_free(labelArray);
397
398   /*------------------------------------------------------- 
399    * .table state -> fair1
400    * .default 0
401    * ------------------------------------------------------
402    */
403   if (lsLength(A->Fair) != 0) {
404     i = 1;
405     lsForEachItem(A->Fair, lsgen, FairSet) {
406       int isFirst = 1;
407       fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++);
408       fprintf(fp, "\n.default 0\n(");
409       st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
410         if (isFirst)
411           isFirst = 0;
412         else
413           fprintf(fp, ",");
414         fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
415       }
416       fprintf(fp, ")   1");
417     }
418   }else {
419     fprintf(fp, "\n.table state$AUT -> fair1$AUT ");
420     if (InitIdx == -1)
421       fprintf(fp, "\n.default 0\n!(Trap,Init)   1");
422     else
423       fprintf(fp, "\n.default 0\n!(Trap)   1");
424   }
425
426   /*------------------------------------------------------- 
427    * .end
428    * ------------------------------------------------------
429    */
430   fprintf(fp, "\n.end\n");
431
432   /* free the name array
433    */
434   array_free(InputNames);
435   arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
436     st_free_table(tmptbl);
437   }
438   array_free(Name2LabelIdx);
439 
440   return result;
441}
442
443#if 0
444int
445Ltl_AutomatonToBlifMv_Old(
446  FILE *fp,             
447  Ntk_Network_t *network,
448  Ltl_Automaton_t *A)     
449{
450  Var_Variable_t *inputVar;
451  array_t *InputNames = array_alloc(char *, 0);
452  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
453  Ntk_Node_t *ntknode;
454  char *inputName;
455  st_generator *stgen, *stgen2;
456  lsGen lsgen, lsgen2, lsgen3;
457  int i, j, is_enum, range;
458  long index;
459  int sel_num, sel_cnt;
460  edge_t *edge;
461  vertex_t *vtx;
462  st_table *FairSet, *tmptbl;
463  LtlSet_t *label;
464  int InitIdx = AutomatonComputeInitState(A);
465  char InitStr[10];
466  int result = 1;
467
468  /* The initState of the automaton */
469  if (InitIdx == -1)
470    sprintf(InitStr, "Init");
471  else
472    sprintf(InitStr, "n%d", InitIdx);
473 
474  if (network == NIL(Ntk_Network_t)) {
475    result = 0;
476    fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n");
477  }
478
479  /* Retrieve all the input names on the labels; For each input, create a
480   *  hash table and add all the label subformulae contains that input;
481   *  Finally, calculate the size of the "selector"
482   */
483  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
484  sel_num = AutomatonCountSelector(A);
485  fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name);
486 
487  /*-------------------------------------------------------
488   * .model Buechi$AUT
489   * .root  Buechi$AUT
490   *-------------------------------------------------------
491   */
492   fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT");
493 
494   /*-------------------------------------------------------
495    * .inputs in1 in2 in3 ... inN
496    *-------------------------------------------------------
497    */
498   fprintf(fp, "\n.inputs ");
499   for (i=0; i<array_n(InputNames); i++) {
500     inputName = array_fetch(char *, InputNames, i);
501     fprintf(fp, "%s ", inputName);
502   }
503
504   /*-------------------------------------------------------
505    * .outputs fair1 fair2 fair3... fairN
506    *-------------------------------------------------------
507    */
508   fprintf(fp, "\n.outputs ");
509   if ( lsLength(A->Fair) != 0) {
510     for (i=0; i<lsLength(A->Fair); i++) {
511       fprintf(fp, "fair%d$AUT ", i+1);
512     }
513   }else
514     fprintf(fp, "fair1$AUT");
515
516   /*-------------------------------------------------------
517    * .mv in1 3 RED GREEN YELLOW
518    *-------------------------------------------------------
519    */
520   if (network != NIL(Ntk_Network_t)) {
521     for (i=0; i<array_n(InputNames); i++) {
522       inputName = array_fetch(char *, InputNames, i);
523       ntknode = Ntk_NetworkFindNodeByName(network, inputName);
524       assert(ntknode != NIL(Ntk_Node_t));
525       inputVar = Ntk_NodeReadVariable(ntknode);
526       is_enum = Var_VariableTestIsEnumerative(inputVar);
527       range = Var_VariableReadNumValues(inputVar);
528       if (is_enum) {
529         if (range != 2)
530           fprintf(fp, "\n.mv %s %d\n", inputName, range);
531       }else {
532         fprintf(fp, "\n.mv %s %d ", inputName, range);
533         for (j=0; j<range; j++) {
534           fprintf(fp, "%s ",
535                   Var_VariableReadSymbolicValueFromIndex(inputVar,j));
536         }
537       }
538     }
539   }
540
541   /*------------------------------------------------------- 
542    * .mv stateD$AUT N Init n1 n2 n3 ... nN
543    * .mv state$AUT  N Init n1 n2 n3 ... nN
544    *-------------------------------------------------------
545    */
546   if (InitIdx == -1)
547     fprintf(fp, "\n.mv stateD$AUT %d Init Trap ",
548             lsLength(g_get_vertices(A->G)) + 2);
549   else
550     fprintf(fp, "\n.mv stateD$AUT %d Trap ",
551             lsLength(g_get_vertices(A->G)) + 1);
552   foreach_vertex(A->G, lsgen, vtx) {
553     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
554   }
555   if (InitIdx == -1)
556     fprintf(fp, "\n.mv state$AUT %d Init Trap ",
557             lsLength(g_get_vertices(A->G)) + 2);
558   else
559     fprintf(fp, "\n.mv state$AUT %d Trap ",
560             lsLength(g_get_vertices(A->G)) + 1);
561   foreach_vertex(A->G, lsgen, vtx) { 
562     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
563   }
564
565   /*-------------------------------------------------------
566    * .mv selector n
567    * .table selector
568    * -
569    *-------------------------------------------------------
570    */
571   if (sel_num > 1)
572     fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num);
573
574   /*------------------------------------------------------- 
575    * .latch stateD$AUT state$AUT
576    * .reset state$AUT
577    * Init (or ns)
578    *-------------------------------------------------------
579    */
580   fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s",
581           InitStr);
582   
583   /*------------------------------------------------------
584    * .table selector$AUT state$AUT in1 in2 ... inN -> stateD$AUT
585    * .default Trap
586    *------------------------------------------------------
587    */
588   if (sel_num >1)
589     fprintf(fp, "\n.table selector$AUT state$AUT ");
590   else
591     fprintf(fp, "\n.table state$AUT ");
592   
593   for (i=0; i<array_n(InputNames); i++) {
594     inputName = array_fetch(char *, InputNames, i);
595     fprintf(fp, "%s ", inputName);
596   }
597   fprintf(fp, " -> stateD$AUT\n.default Trap");
598   
599 
600   /* for each initial state n2 with label "in1=p  !in3=q...", add entry:
601    *-------------------------------------------------------
602    *  selector Init (p) -  (!(q)) ..  n2   
603    *-------------------------------------------------------
604    */
605   if (InitIdx == -1) {
606     sel_cnt = 0;
607     st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
608       int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx);
609       /* each 'compLabel' is a set of "propositional formulae" */
610       LtlSet_t *compLabel = LtlAutomatonVertexGetLabels(vtx);
611       /* each item in labelList is a set of "atomic proposition" */
612       lsList labelList = AutomatonLabelGetCubes(A, compLabel, network);
613       lsForEachItem(labelList, lsgen, label) {
614         if (sel_num > 1) {
615           if (st_count(A->Init) == 1)
616             fprintf(fp, "\n- Init ");
617           else
618             fprintf(fp, "\n%d Init ", sel_cnt);
619         }else
620           fprintf(fp, "\nInit ");
621         arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
622           int isFirst = 1;
623           int is_universe = 1;
624           /* The value is the universe '-' iff it is not in the label */
625           if (!LtlSetIsEmpty(label)) {
626             st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) {
627               if (LtlSetGetElt(label, (int) index)) {
628                 is_universe = 0;
629                 st_free_gen(stgen2);
630                 break;
631               }
632             }
633           }
634           if (is_universe) {
635             fprintf(fp, "- ");
636             continue;
637           }
638           /* Otherwise, write the value. Note that the value should be
639            * the conjunction of the values of the atomic propositions.
640            * A * B * C = !(!A + !B +!C)
641            */
642           fprintf(fp, "!(");
643           st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) {
644             if (LtlSetGetElt(label, (int) index)) {
645               Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
646                                                A->labelTable,
647                                                (int) index);
648               if (isFirst)
649                 isFirst = 0;
650               else
651                 fprintf(fp, ",");
652               if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c) {
653                 F = Ctlsp_FormulaReadLeftChild(F);
654               }else {
655                 fprintf(fp, "!");
656               }
657               
658               fprintf(fp, "(%s)", Ctlsp_FormulaReadValueName(F));
659             }
660           }
661           fprintf(fp, ") ");
662         }
663         fprintf(fp, "   n%d", n2);
664       }
665       lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree);
666       
667       if (sel_num > 1)
668         sel_cnt++;
669     }
670   }
671
672   /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry:
673    *-------------------------------------------------------     
674    * selector n1 (p) - (!(q)) ...     n2
675    *-------------------------------------------------------
676    */
677   foreach_vertex(A->G, lsgen, vtx) {
678     int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
679     int outDegree = lsLength(g_get_out_edges(vtx));
680     sel_cnt = 0;
681     foreach_out_edge(vtx, lsgen2, edge) {
682       int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
683       /* 'compLabel' contains a set of "propositional formulae" */
684       LtlSet_t *compLabel =   LtlAutomatonVertexGetLabels(g_e_dest(edge));
685       /* each item in 'labelList' is a set of "atomic propositions" */
686       lsList labelList = AutomatonLabelGetCubes(A, compLabel, network);
687       lsForEachItem(labelList, lsgen3, label) {
688         if (sel_num > 1) {
689           if (outDegree == 1)
690             fprintf(fp, "\n- n%d ", n1);
691           else
692             fprintf(fp, "\n%d n%d ", sel_cnt, n1);
693         }else {
694           fprintf(fp, "\nn%d ", n1);
695         }
696         arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
697           int isFirst = 1;
698           int is_universe = 1;
699           /* the value is universe '-' iff it is not in the label */
700           if (!LtlSetIsEmpty(label)) {
701             st_foreach_item(tmptbl,stgen2,&index, NIL(char *)){
702               if (LtlSetGetElt(label, (int) index)) {
703                 is_universe = 0;
704                 st_free_gen(stgen2);
705                 break;
706               }
707             }
708           }
709           if (is_universe) {
710             fprintf(fp, "- ");
711             continue;
712           }
713           /* write the value as the conjunction of the values in the
714            * atomic proposition. for example, if the state is labeled
715            * 'in1={R,G,B}' and 'in1={G}', we should write as
716            * !( !(R,G,B), !(G) )
717            * Note that it's the same as {R,G,B}^{G}={G}
718            */
719           fprintf(fp, "!(");
720           st_foreach_item(tmptbl, stgen, &index, NIL(char *)) {
721             if (LtlSetGetElt(label, (int) index)) {
722               Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
723                                                A->labelTable,
724                                                (int) index);
725               if (isFirst)
726                 isFirst = 0;
727               else
728                 fprintf(fp, ",");
729               if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c)
730                 F = Ctlsp_FormulaReadLeftChild(F);
731               else
732                 fprintf(fp, "!");
733               fprintf(fp, "(%s)",      Ctlsp_FormulaReadValueName(F));
734             }
735           }
736           fprintf(fp, ") ");
737         }
738         fprintf(fp, "   n%d", n2);
739       }
740       lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree);
741         
742       if (sel_num > 1)
743         sel_cnt++;
744     }
745   }
746 
747
748   /*------------------------------------------------------- 
749    * .table state -> fair1
750    * .default 0
751    * ------------------------------------------------------
752    */
753   if (lsLength(A->Fair) != 0) {
754     i = 1;
755     lsForEachItem(A->Fair, lsgen, FairSet) {
756       int isFirst = 1;
757       fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++);
758       fprintf(fp, "\n.default 0\n(");
759       st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
760         if (isFirst)
761           isFirst = 0;
762         else
763           fprintf(fp, ",");
764         fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
765       }
766       fprintf(fp, ")   1");
767     }
768   }else {
769     fprintf(fp, "\n.table state$AUT -> fair1$AUT ");
770     if (InitIdx == -1)
771       fprintf(fp, "\n.default 0\n!(Trap,Init)   1");
772     else
773       fprintf(fp, "\n.default 0\n!(Trap)   1");
774   }
775
776   /*------------------------------------------------------- 
777    * .end
778    * ------------------------------------------------------
779    */
780   fprintf(fp, "\n.end\n");
781
782   /* free the name array
783    */
784   array_free(InputNames);
785   arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
786     st_free_table(tmptbl);
787   }
788   array_free(Name2LabelIdx);
789   
790   return result;
791}
792#endif
793
794     
795/**Function********************************************************************
796
797  Synopsis    [Translate the automaton to Verilog file.]
798
799  Description [The Hrc_Manager may or may not be provided. If not, the verilog
800  file generated is not accurate (all the inputs are assummed to be boolean).]
801
802  SideEffects []
803
804  SeeAlso     []
805
806******************************************************************************/
807int
808Ltl_AutomatonToVerilog(
809  FILE *fp,             
810  Ntk_Network_t *network,
811  Ltl_Automaton_t *A)     
812{
813  Var_Variable_t *inputVar;
814  array_t *InputNames = array_alloc(char *, 0);
815  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
816  Ntk_Node_t *ntknode;
817  char *inputName, *formulaString, *normalString;
818  st_generator *stgen;
819  lsGen lsgen, lsgen2;
820  int i, j, is_enum, range, isFirst;
821  int sel_num, sel_cnt;
822  edge_t *edge;
823  vertex_t *vtx;
824  st_table *FairSet;
825  int InitIdx = AutomatonComputeInitState(A);
826  char InitStr[10];
827  int result = 1;
828 
829  /* The initState of the automaton */
830  if (InitIdx == -1) 
831    sprintf(InitStr, "Init");
832  else
833    sprintf(InitStr, "n%d", InitIdx);
834
835  if (network == NIL(Ntk_Network_t)) {
836    result = 0;
837    fprintf(vis_stderr, "Warning: the Verilog output is incomplete. (The current node is empty. Read in design.)\n");
838  }
839
840  /* Retrieve all the input names of the automaton into 'InputNames', And for
841   * each name, put into a hash table all the subformulae contains it
842   */
843  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
844  sel_num = AutomatonCountSelector(A);
845  fprintf(fp, "\n// Buechi automaton: %s", A->name);
846   
847  /*-------------------------------------------------------
848   * typedef enum {Init, trap, n1, n2, ... nN} states;
849   * typedef enum {READ, GREEN, YELLOW} type_in1;
850   *-------------------------------------------------------
851   */   
852  if (InitIdx == -1)
853    fprintf(fp, "\ntypedef enum {Init,Trap");
854  else
855    fprintf(fp, "\ntypedef enum {Trap");
856  foreach_vertex(A->G, lsgen, vtx) {
857    fprintf(fp, ",n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
858  }
859  fprintf(fp, "} type_states;");
860
861  if (network != NIL(Ntk_Network_t)) {
862    arrayForEachItem(char *, InputNames, i, inputName) {
863      /* replace illegal characters in the input name string */
864      normalString = StringNormalize(inputName);
865      fprintf(fp, "\n//Input name mapping:\t %s => %s;", inputName,
866              normalString);
867
868      ntknode = Ntk_NetworkFindNodeByName(network, inputName);
869      assert(ntknode != NIL(Ntk_Node_t));
870      inputVar = Ntk_NodeReadVariable(ntknode);
871     
872      is_enum = Var_VariableTestIsEnumerative(inputVar);
873      range = Var_VariableReadNumValues(inputVar);
874      if (is_enum) {
875        if (range>2)
876          fprintf(fp, "\ntypedef enum {0-%d}  type_%s;", 
877                  range-1, normalString);
878      }else {
879        fprintf(fp, "\ntypedef enum {");
880        isFirst = 1;
881        for (j=0; j<range; j++) {
882          char *vstr =
883            Var_VariableReadSymbolicValueFromIndex(inputVar,j);
884          if (isFirst)  {
885            fprintf(fp, "%s ", vstr);
886            isFirst = 0;
887          } else 
888            fprintf(fp, ",%s ", vstr);
889        }
890        fprintf(fp, "}  type_%s;", normalString);
891      }
892     
893      FREE(normalString);
894    }
895  }
896 
897  /*-------------------------------------------------------   
898   * module Buechi (clock, in1, in2 ... inN, fair1, ...);
899   *-------------------------------------------------------
900   */
901  fprintf(fp, "\n//Buechi Buechi (clock");
902  for (i=0; i<array_n(InputNames); i++) {
903    inputName = array_fetch(char *, InputNames, i);
904    fprintf(fp, ",%s", inputName);
905  }
906  for (i=0; i<lsLength(A->Fair); i++) {
907    fprintf(fp, ",fair%d", i+1);
908  }
909  fprintf(fp, ");");
910 
911  fprintf(fp, "\nmodule Buechi (clock");
912  for (i=0; i<array_n(InputNames); i++) {
913    inputName = array_fetch(char *, InputNames, i);
914    normalString = StringNormalize(inputName);
915    fprintf(fp, ",%s", normalString);
916    FREE(normalString);
917  }
918  for (i=0; i<lsLength(A->Fair); i++) {
919    fprintf(fp, ",fair%d", i+1);
920  }
921  fprintf(fp, ");");
922
923 
924  /*-------------------------------------------------------
925   * input clock, in1, in2 ... inN ;
926   * output fair1, fair2 ... fairN ;
927   *-------------------------------------------------------
928   */
929  fprintf(fp, "\n\tinput clock");
930  for (i=0; i<array_n(InputNames); i++) {
931    inputName = array_fetch(char *, InputNames, i);
932    normalString = StringNormalize(inputName);
933    fprintf(fp, ", %s", normalString);
934    FREE(normalString);
935  }
936  if (lsLength(A->Fair)>0) {
937    fprintf(fp, ";\n\toutput ");
938    isFirst = 1;
939    for (i=0; i<lsLength(A->Fair); i++) {
940      if (isFirst)  {
941        fprintf(fp, "fair%d", i+1);
942        isFirst = 0;
943      } else {
944        fprintf(fp, ",fair%d", i+1);
945      }
946    }
947  }
948  fprintf(fp, ";");
949
950 
951  /*-------------------------------------------------------
952   * type_in1 wire in1;
953   * type_in2 wire in2;
954   * ...
955   * type_states reg state;
956   * wire[0:logN] sel;
957   *-------------------------------------------------------
958   */
959  if (network != NIL(Ntk_Network_t)) {
960    arrayForEachItem(char *, InputNames, i, inputName) {
961      normalString = StringNormalize(inputName);
962
963      ntknode = Ntk_NetworkFindNodeByName(network, inputName);
964      assert(ntknode != NIL(Ntk_Node_t));
965      inputVar = Ntk_NodeReadVariable(ntknode);
966     
967      is_enum = Var_VariableTestIsEnumerative(inputVar);
968      range = Var_VariableReadNumValues(inputVar);
969     
970      if (!is_enum || range > 2)
971        fprintf(fp, "\n\ttype_%s  wire  %s;", normalString,normalString);
972      FREE(normalString);
973    }
974  }
975  fprintf(fp, "\n\ttype_states reg state;");
976  if (sel_num >1) {
977    if (sel_num == 2)
978      fprintf(fp, "\n\twire sel;");
979    else
980      fprintf(fp, "\n\twire [0:%d] sel;", (int)(ceil(log(sel_num)))-1);
981  }
982 
983  /*-------------------------------------------------------
984   * assign sel = $ND( {0-N} );
985   * assign fair = (state==n1 || state==n2 || ... );
986   *-------------------------------------------------------
987   */
988  fprintf(fp, "\n\tassign sel = $ND( {0-%d} );", sel_num-1 );
989  i = 1;
990  lsForEachItem(A->Fair, lsgen, FairSet) {
991    int isFirst = 1;
992    fprintf(fp, "\n\tassign fair%d = (state==", i++);
993    st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
994      if (isFirst)
995        isFirst = 0;
996      else
997        fprintf(fp, "|| state==");
998      fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
999    }
1000    fprintf(fp, ");");
1001  }
1002 
1003  /*-------------------------------------------------------
1004   * initial state = Init;
1005   *-------------------------------------------------------
1006   */
1007  fprintf(fp, "\n\tinitial state = %s;", InitStr);
1008
1009  /*-------------------------------------------------------
1010   * always @ (posedge clock) begin
1011   *    case (state)
1012   *-------------------------------------------------------
1013   */
1014  fprintf(fp, "\n\talways @ (posedge clock) begin");
1015  fprintf(fp, "\n\t\tcase (state)"); 
1016
1017  /* for each initial state n2 with label "in1=p  !in3=q...", add entry:
1018   *-------------------------------------------------------
1019   *      Init:
1020   *         if( sel==0 && in1==p && !in3=q ... )
1021   *            state = n2;
1022   *         else if( sel==1 && ...)
1023   *            state = n3;
1024   *         else
1025   *            state = Trap;
1026   *------------------------------------------------------
1027   */
1028  if (InitIdx == -1) {
1029    fprintf(fp, "\n\t\tInit:");
1030    sel_cnt = 0;
1031    st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
1032      int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx);
1033      LtlSet_t *label = LtlAutomatonVertexGetLabels(vtx);
1034     
1035      /* universal label (no label) on n2 */
1036      if (LtlSetIsEmpty(label)) {
1037        if (st_count(A->Init) == 1 || sel_num == 0)
1038          fprintf(fp,"\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
1039        else if (sel_cnt == 0)
1040          fprintf(fp,"\n\t\t\tif(sel==%d)\n\t\t\t\tstate = n%d;",
1041                  sel_cnt++, n2);
1042        else 
1043          fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
1044                  sel_cnt++, n2);
1045      }else {
1046        /* there is at least one label on n2 */
1047        if (st_count(A->Init) == 1 || sel_num == 0)
1048          fprintf(fp, "\n\t\t\tif(");
1049        else if (sel_cnt==0)
1050          fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
1051        else 
1052          fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
1053       
1054        isFirst = 1;
1055        for (i=0; i<array_n(A->labelTable); i++) {
1056          if (LtlSetGetElt(label, i)) {
1057            Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
1058                                             A->labelTable, i);
1059            formulaString = Ctlsp_FormulaConvertToString(F);
1060            normalString = StringNormalize(formulaString);
1061            FREE(formulaString);
1062           
1063            if (isFirst)
1064              isFirst = 0;
1065            else
1066              fprintf(fp, " && ");
1067           
1068            fprintf(fp, "%s", normalString);
1069            FREE(normalString);
1070          }
1071        }
1072        fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
1073      }
1074    }     
1075    fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
1076  }
1077 
1078  /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry:
1079   *-------------------------------------------------------     
1080   *      n1:
1081   *         if( sel==0 && in1==p && !in3=q ... )
1082   *            state = n2;
1083   *         else if( sel==1 && ...)
1084   *            state = n3;
1085   *         else
1086   *            state = Trap;
1087   *-------------------------------------------------------
1088   */
1089  foreach_vertex(A->G, lsgen, vtx) {
1090    int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
1091    int outDegree = lsLength(g_get_out_edges(vtx));
1092    fprintf(fp, "\n\t\tn%d:", n1);
1093    sel_cnt = 0;
1094    foreach_out_edge(vtx, lsgen2, edge) {
1095      int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
1096      LtlSet_t *label =   LtlAutomatonVertexGetLabels(g_e_dest(edge));
1097         
1098      /* universal label (no label) on n2 */
1099      if (LtlSetIsEmpty(label)) {
1100        if (outDegree == 1 || sel_num == 0)
1101          fprintf(fp, "\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
1102        else if (sel_cnt == 0)
1103          fprintf(fp, "\n\t\t\tif(sel==%d) \n\t\t\t\tstate = n%d;",
1104                  sel_cnt++, n2);
1105        else 
1106          fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
1107                  sel_cnt++, n2);
1108      }else { 
1109        /* at least 1 label on n2 */
1110        if (outDegree == 1 || sel_num == 0)
1111          fprintf(fp, "\n\t\t\tif(");
1112        else if (sel_cnt==0)
1113          fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
1114        else 
1115          fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
1116       
1117        isFirst = 1;
1118        for (i=0; i<array_n(A->labelTableNegate); i++) {
1119          if (LtlSetGetElt(label, i)) {
1120            Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
1121                                             A->labelTable, i);
1122            formulaString = Ctlsp_FormulaConvertToString(F);
1123            normalString = StringNormalize(formulaString);
1124            FREE(formulaString);
1125           
1126            if (isFirst)  isFirst = 0;
1127            else fprintf(fp, " && ");
1128           
1129            fprintf(fp, "%s", normalString);
1130            FREE(normalString);
1131          }
1132        }
1133        fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
1134      }
1135    }     
1136    fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
1137  }
1138 
1139  /*-------------------------------------------------------
1140   *        default: state = Trap;
1141   *      endcase
1142   *    end
1143   * endmodule
1144   *-------------------------------------------------------
1145   */
1146  fprintf(fp, "\n\t\tdefault: state = Trap;\n\t\tendcase\n\tend\nendmodule\n");
1147 
1148  /* free the name array */
1149  array_free(InputNames);
1150  for(i=0; i<array_n(Name2LabelIdx); i++) {
1151    st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, i);
1152    st_free_table(tmptbl);
1153  }
1154  array_free(Name2LabelIdx);
1155 
1156  return result;
1157}
1158
1159     
1160/**Function********************************************************************
1161
1162  Synopsis    [Translate the automaton to SMV file.]
1163
1164  Description [The Hrc_Manager may or may not be provided. If not, the blifmv
1165  file generated is not complete (inputs are assummed to be boolean.]
1166
1167  SideEffects []
1168
1169  SeeAlso     []
1170
1171******************************************************************************/
1172int
1173Ltl_AutomatonToSmv(
1174  FILE *fp,             
1175  Ntk_Network_t *network,
1176  Ltl_Automaton_t *A)     
1177{
1178    return 1;
1179}
1180
1181/*---------------------------------------------------------------------------*/
1182/* Definition of static functions                                          */
1183/*---------------------------------------------------------------------------*/
1184
1185
1186/**Function********************************************************************
1187
1188  Synopsis    [Return a array of all the inputnames of the automaton.]
1189 
1190  Description [InputNames and Name2LabelIdx are two "array_t" provided by the
1191  caller. InputNames will be filled by all the labels on the automaton nodes;
1192  Each item of Name2LabelIdx is a "st_table" from a label to all the related
1193  formulae in A->labelTable that contains the label.]
1194 
1195  SideEffects []
1196
1197******************************************************************************/
1198static void
1199AutomatonGetInputNames(
1200  Ltl_Automaton_t *A,
1201  array_t *InputNames,
1202  array_t *Name2LabelIdx)
1203{
1204  st_table *Visited = st_init_table(strcmp, st_strhash);
1205  Ctlsp_Formula_t *F;
1206  Ctlsp_FormulaType F_type;
1207  long i, index, counter;
1208
1209  counter = 0;
1210  for (i=0; i<array_n(A->labelTable); i++) {
1211    /* get the positive formula string */
1212    F = array_fetch(Ctlsp_Formula_t *, A->labelTable, i);
1213    F_type = Ctlsp_FormulaReadType(F);
1214    /* if it's not an AP (just a propositional formula), skip ... */
1215    if (F_type != Ctlsp_NOT_c && F_type != Ctlsp_ID_c)
1216      continue;
1217    if (F_type == Ctlsp_NOT_c) 
1218      F = Ctlsp_FormulaReadLeftChild(F);
1219    /* put into the InputNames array */
1220    if (!st_lookup(Visited, Ctlsp_FormulaReadVariableName(F),&index)){
1221      st_table *tmptbl = st_init_table(st_numcmp, st_numhash);
1222      st_insert(tmptbl, (char *) i, (char *)i);
1223     
1224      array_insert(st_table *, Name2LabelIdx, counter, tmptbl);
1225      array_insert(char *, InputNames, counter,
1226                   Ctlsp_FormulaReadVariableName(F));
1227     
1228      st_insert(Visited, Ctlsp_FormulaReadVariableName(F), (char *)counter++);
1229    }else {
1230      st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, index);
1231      st_insert(tmptbl, (char *)i, (char *)i);
1232    }
1233  }
1234 
1235  st_free_table(Visited);
1236}
1237   
1238/**Function********************************************************************
1239
1240  Synopsis    [Return the upper bound number of nondeterministic selectors.]
1241 
1242  Description [The automaton is nondeterministic, but the blif_mv file should
1243  be deterministic. Selector (variable with random output) is used to make
1244  the .table determinstic. We need to know how many outputs the Selector
1245  should have. Here we take the maximum out-degree among all nodes as the
1246  upper bound estimation.]
1247 
1248  SideEffects []
1249
1250******************************************************************************/
1251static int
1252AutomatonCountSelector(
1253  Ltl_Automaton_t *A)
1254{
1255  int sel_num = st_count(A->Init);
1256  int local_num;
1257  lsGen lsgen;
1258  vertex_t *vtx;
1259 
1260  foreach_vertex(A->G, lsgen, vtx) {
1261    local_num = lsLength(g_get_out_edges(vtx));
1262    if (sel_num < local_num)
1263      sel_num = local_num;
1264  }
1265 
1266  return sel_num;
1267}
1268
1269
1270/**Function********************************************************************
1271
1272  Synopsis    [Determine if "Init" state is necessary.]
1273 
1274  Description [If there exists such a state 'ns', "Init" is not necessary:
1275  (1) ns  is in Aut->Init
1276  (2) there is a edge from ns to every state in Aut->Init (including itself)
1277  In another word, ns is equivalent to "Init".
1278  (3) there is no edge fron ns to states not in Aut->Init.
1279
1280  Return the index of the state 'ns' if exist, otherwise return -1.  ]
1281 
1282  SideEffects []
1283
1284******************************************************************************/
1285static int
1286AutomatonComputeInitState(
1287  Ltl_Automaton_t *A)
1288{
1289  int initIdx = -1;
1290  vertex_t *vtx, *vtx2, *s;
1291  edge_t *e;
1292  st_generator *stgen, *stgen2;
1293  lsGen lsgen;
1294
1295  st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
1296    int isInit = 1;
1297    /* first, compute the set of sucessors of 'vtx' */
1298    lsList Img = g_get_out_edges(vtx);
1299    st_table *uTable = st_init_table(st_ptrcmp, st_ptrhash);
1300    lsForEachItem(Img, lsgen, e) {
1301      s = g_e_dest(e);
1302      st_insert(uTable,  s,  s);
1303    }
1304    /* then, test if it is equivalent to 'A->Init': No more, No less */
1305    st_foreach_item(A->Init, stgen2, &vtx2, NIL(char *)) {
1306      if (!st_is_member(uTable, vtx2)) {
1307        isInit = 0;
1308        st_free_gen(stgen2);
1309        break;
1310      }
1311    }
1312    if (isInit) {
1313      st_foreach_item(uTable, stgen2, &vtx2, NIL(char *)) {
1314        if (!st_is_member(A->Init, vtx2)) {
1315          isInit = 0;
1316          st_free_gen(stgen2);
1317          break;
1318        }
1319      }
1320    }
1321    st_free_table(uTable);
1322
1323    if (isInit == 1) {
1324      initIdx = ((Ltl_AutomatonNode_t *)vtx->user_data)->index;
1325      st_free_gen(stgen);
1326      break;
1327    }
1328  }
1329   
1330  return initIdx;
1331}
1332
1333/**Function********************************************************************
1334
1335  Synopsis    [Given a composite label, return a list of label (each of which
1336  is a cube.]
1337 
1338  Description [The composite label can any combination of !, + , *.]
1339   
1340  SideEffects []
1341
1342******************************************************************************/
1343/*static lsList
1344AutomatonLabelGetCubes(
1345  Ltl_Automaton_t *A,
1346  LtlSet_t *compositeLabel,
1347  Ntk_Network_t *network)
1348{
1349  LtlTableau_t *tableau = A->tableau;
1350  int size = tableau->labelIndex;
1351  LtlSet_t *tempSet, *tempSet2, *tempSet3;
1352  lsList conjunctList;
1353  lsList disjunctList;
1354  lsList tempList, tempList2, tempList3;
1355  lsGen lsgen, lsgen2;
1356  int i;
1357
1358  if (LtlSetIsEmpty(compositeLabel)) {
1359    tempList = lsCreate();
1360    lsNewEnd(tempList, (lsGeneric)LtlSetNew(size), (lsHandle *)0);
1361    return tempList;
1362  }
1363 
1364  first, get a list of disjunctLists (which should be conjoin together
1365    to form a cartesian product
1366   
1367  conjunctList = lsCreate();
1368  tempSet = LtlSetNew(size);
1369  for (i=0; i<size; i++) {
1370    if (LtlSetGetElt(compositeLabel, i)) {
1371      if (Ctlsp_LtlFormulaIsAtomicPropositional(tableau->labelTable[i]))
1372        LtlSetSetElt(tempSet, i);
1373      else {
1374        disjunctList = GetCubes_Aux(A, i);
1375        lsNewEnd(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0);
1376      }
1377    }
1378  }
1379  if (LtlSetIsEmpty(tempSet))
1380    LtlSetFree(tempSet);
1381  else {
1382    disjunctList = lsCreate();
1383    lsNewEnd(disjunctList, (lsGeneric)tempSet, (lsHandle *)0);
1384    lsNewBegin(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0);
1385  }
1386   
1387
1388  compute the cartesian product of the conjuncts
1389  while(lsLength(conjunctList)>1) {
1390    lsList thisList;
1391    lsList leftList;
1392    lsList rightList;
1393   
1394    lsDelBegin(conjunctList, (lsGeneric *)&leftList);
1395    lsDelBegin(conjunctList, (lsGeneric *)&rightList);
1396     form the cartesian product of the two lists
1397    thisList = lsCreate();
1398    lsForEachItem(leftList, lsgen, tempSet) {
1399      lsForEachItem(rightList, lsgen2, tempSet2) {
1400        tempSet3 = LtlSetNew(size);
1401        LtlSetOR(tempSet3, tempSet, tempSet2);
1402       
1403        if (0)
1404          fprintf(vis_stdout,
1405                  "tempSet = %d  tempSet2 = %d tempSet3 = %d\n",
1406                  LtlSetIsEmpty(tempSet),
1407                  LtlSetIsEmpty(tempSet2),
1408                  LtlSetIsEmpty(tempSet3));
1409       
1410         if no contradictory, retain it
1411        if (LtlSetIsContradictory(tempSet3,tableau->labelTableNegate))
1412          LtlSetFree(tempSet3);
1413        else
1414          lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0);
1415      }
1416    }
1417    lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree);
1418    lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree);
1419   
1420    lsNewBegin(conjunctList, (lsGeneric)thisList, (lsHandle *)0);
1421  }
1422 
1423  lsDelBegin(conjunctList, (lsGeneric *)&tempList);
1424  lsDestroy(conjunctList, (void(*)(lsGeneric))0);
1425
1426   remove redundant minterms from 'tempList'
1427  tempList3 = lsCreate();
1428  tempList2 = lsCopy(tempList, (lsGeneric(*)(lsGeneric))0);
1429  lsForEachItem(tempList, lsgen, tempSet) {
1430     If tempSet is a superset of other cubes, discard it
1431    int flag = 1;
1432    lsForEachItem(tempList2, lsgen2, tempSet2) {
1433      if (tempSet != tempSet2 && LtlSetInclude(tempSet, tempSet2)) {
1434        flag = 0;
1435        lsFinish(lsgen2);
1436        break;
1437      }
1438    }
1439    if (!flag) continue;
1440     If tempSet is an "emptyset" (for example, comtains both
1441     signal=0 and signal=1, where signal has only these two
1442      values),  discard it
1443     
1444    flag = 1;
1445    if (network != NIL(Ntk_Network_t)) {
1446      Fsm_Fsm_t *fsm = Fsm_NetworkReadOrCreateFsm(network);
1447      if (fsm != NIL(Fsm_Fsm_t)) {
1448        mdd_t *minterm = LtlSetModelCheckFormulae(tempSet,
1449                                                  A->labelTable,
1450                                                  fsm);
1451        flag = !(mdd_is_tautology(minterm, 0));
1452        mdd_free(minterm);
1453      }
1454    }
1455    if (!flag) continue;
1456     otherwise, save a copy into tempList3
1457    lsNewBegin(tempList3, (lsGeneric)LtlSetCopy(tempSet), (lsHandle *)0);
1458  }
1459  lsDestroy(tempList2, (void(*)(lsGeneric))0);
1460  lsDestroy(tempList, (void (*)(lsGeneric))LtlSetFree);
1461  tempList = tempList3;
1462
1463  return tempList;
1464}
1465  */
1466
1467/**Function********************************************************************
1468
1469  Synopsis    [Given a index in A->tableau->labelTable, return a list of label
1470  (each of which  is a cube.]
1471 
1472  Description [The formula A->tableau->labelTable[index] can be  any
1473  combination of !, + , *.]
1474   
1475  SideEffects []
1476
1477******************************************************************************/
1478static lsList
1479GetCubes_Aux(
1480  Ltl_Automaton_t *A,
1481  int index)
1482{
1483  Ctlsp_Formula_t *F = A->tableau->labelTable[index];
1484  int size = A->tableau->labelIndex;
1485  lsList leftList;
1486  lsList rightList;
1487  lsList thisList =(lsList)0;
1488  lsGen lsgen, lsgen2;
1489  LtlSet_t *tempSet, *tempSet2, *tempSet3;
1490 
1491  if (Ctlsp_LtlFormulaIsAtomicPropositional(F)) {
1492    thisList = lsCreate();
1493    tempSet = LtlSetNew(size);
1494    LtlSetSetElt(tempSet, Ctlsp_FormulaReadLabelIndex(F));
1495    lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
1496  }else {
1497    Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
1498    Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
1499   
1500    switch(Ctlsp_FormulaReadType(F)) {
1501    case Ctlsp_OR_c:
1502      leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
1503      rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
1504      /* merge two list together */
1505      thisList = leftList;
1506      lsForEachItem(rightList, lsgen, tempSet) {
1507        lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
1508      }
1509      lsDestroy(rightList, (void (*)(lsGeneric))0);
1510      break;
1511    case Ctlsp_AND_c:
1512      leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
1513      rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
1514      /* generate the cartesian product of the two lists */
1515      thisList = lsCreate();
1516      lsForEachItem(leftList, lsgen, tempSet) {
1517        lsForEachItem(rightList, lsgen2, tempSet2) {
1518          tempSet3 = LtlSetNew(size);
1519          LtlSetOR(tempSet3, tempSet, tempSet2);
1520          lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0);
1521        }
1522      }
1523      lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree);
1524      lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree);
1525      break;
1526    default:
1527      assert(0);
1528      break;
1529    }
1530  }
1531 
1532  return thisList;
1533}
1534
1535
1536/**Function********************************************************************
1537
1538  Synopsis    [Given a string, do the following replacement.]
1539 
1540  Description [
1541  =   =>   ==
1542  +   =>   ||
1543  *   =>   &&
1544  .   =>   _
1545  <   =>   _
1546  >   =>   _  ]
1547   
1548  SideEffects [The caller should free the result]
1549
1550******************************************************************************/
1551static char *
1552StringNormalize(
1553  char *inputString)
1554{
1555  char *normalString = ALLOC(char, strlen(inputString)*2);
1556  char *from = inputString;
1557  char *to = normalString;
1558 
1559  while( *from ) {
1560    switch(*from) {
1561    case '=':
1562      *(to++) = '=';
1563      *(to) = '=';
1564      break;
1565    case '+':
1566      *(to++) = '|';
1567      *(to) = '|';
1568      break;
1569    case '*':
1570      *(to++) = '&';
1571      *(to) = '&';
1572      break;
1573    case '.':
1574    case '<':
1575    case '>':
1576      *(to) = '_';
1577      break;
1578    default:
1579      *(to) = *from;
1580    }
1581    from++;
1582    to++;
1583  }
1584  *to = '\0';
1585 
1586  return normalString;
1587}
1588
1589/**Function********************************************************************
1590
1591  Synopsis    [Create the "label" signal in blif_mv format and print out.]
1592 
1593  Description [Assume that the label is a propositional formula with *, +, !.
1594  *
1595  * For Ctlsp_ID_c/Ctlsp_NOT_c:
1596  *   .table in1 n1_##_label$AUT
1597  *   !(RED) 1
1598  * For Ctlsp_AND_c:
1599  *   .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
1600  *   1 1  1
1601  * For Ctlsp_OR_c:
1602  *   .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
1603  *   1 -  1
1604  *   - 1  1
1605  ]
1606 
1607  SideEffects []
1608
1609******************************************************************************/
1610static void
1611AutomatonVtxLabelToBlifMv(
1612  FILE *fp,
1613  Ltl_Automaton_t *A,
1614  vertex_t *vtx)
1615{
1616    /* each 'compLabel' is a "propositional formulae" */
1617    LtlSet_t *compositeLabel = LtlAutomatonVertexGetLabels(vtx);
1618    int idx = Ltl_AutomatonVtxGetNodeIdx(vtx);
1619    int size = A->tableau->labelIndex;
1620    int i;
1621    st_table *CreatedSignals;
1622       
1623    if (LtlSetIsEmpty(compositeLabel)) {
1624        fprintf(fp, "\n.table n%d_label$AUT\n1\n", idx);
1625        return;
1626    }
1627   
1628    /* first, we should create the signals for each subformula */
1629    CreatedSignals = st_init_table(st_ptrcmp, st_ptrhash);
1630    for (i=0; i<size; i++) {
1631      if (LtlSetGetElt(compositeLabel, i))
1632        VtxLabelToBlifMv_Aux(fp, A, idx, i, CreatedSignals);
1633    }
1634    st_free_table(CreatedSignals);
1635   
1636    /* the label signal is the AND or all the conjuncts */
1637    fprintf(fp, "\n.table ");
1638    for (i=0; i<size; i++) {
1639      if (LtlSetGetElt(compositeLabel, i))
1640        fprintf(fp, "n%d_%d_label$AUT ", idx, i);
1641    }
1642    fprintf(fp, "  -> n%d_label$AUT\n.default 0\n", idx);
1643    for (i=0; i<size; i++) {
1644      if (LtlSetGetElt(compositeLabel, i))
1645        fprintf(fp, "1 ");
1646    }
1647    fprintf(fp, "1\n");
1648
1649}
1650
1651/**Function********************************************************************
1652
1653  Synopsis    [Create the "label" signal in blif_mv format and print out.]
1654 
1655  Description [Assume that "i" is the index in the label table]
1656 
1657  SideEffects []
1658
1659******************************************************************************/
1660static void
1661VtxLabelToBlifMv_Aux(
1662  FILE *fp,
1663  Ltl_Automaton_t *A,
1664  int node_idx,
1665  int index,
1666  st_table *CreatedSignals)
1667{
1668    Ctlsp_Formula_t *F = A->tableau->labelTable[index];
1669    Ctlsp_Formula_t *F_left, *F_right;
1670    int l_index, r_index;
1671
1672    if (st_is_member(CreatedSignals, F))
1673        return;
1674    else
1675        st_insert(CreatedSignals, F, (char *)0);
1676 
1677    switch(Ctlsp_FormulaReadType(F)) {
1678    case Ctlsp_ID_c:
1679        fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 0\n%s 1",
1680                (char *)Ctlsp_FormulaReadVariableName(F),
1681                node_idx, index,
1682                (char *)Ctlsp_FormulaReadValueName(F));
1683        break;
1684    case Ctlsp_NOT_c:
1685        F_left = Ctlsp_FormulaReadLeftChild(F);
1686        fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 1\n%s 0",
1687                (char *)Ctlsp_FormulaReadVariableName(F_left),
1688                node_idx, index,
1689                (char *)Ctlsp_FormulaReadValueName(F_left));
1690        break;
1691    case Ctlsp_AND_c:
1692        F_left = Ctlsp_FormulaReadLeftChild(F);
1693        F_right = Ctlsp_FormulaReadRightChild(F);
1694        l_index = Ctlsp_FormulaReadLabelIndex(F_left);
1695        r_index = Ctlsp_FormulaReadLabelIndex(F_right);
1696        VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
1697        VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
1698        fprintf(fp,"\n.table n%d_%d_label$AUT n%d_%d_label$AUT -> n%d_%d_label$AUT\n.default 0\n1 1 1",
1699                node_idx, l_index,
1700                node_idx, r_index,
1701                node_idx, index);
1702        break;
1703    case Ctlsp_OR_c:
1704        F_left = Ctlsp_FormulaReadLeftChild(F);
1705        F_right = Ctlsp_FormulaReadRightChild(F);
1706        l_index = Ctlsp_FormulaReadLabelIndex(F_left);
1707        r_index = Ctlsp_FormulaReadLabelIndex(F_right);
1708        VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
1709        VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
1710        fprintf(fp,
1711        "\n.table n%d_%d_label$AUT n%d_%d_label$AUT -> n%d_%d_label$AUT\n.default 0\n1 - 1\n- 1 1",
1712                node_idx, l_index,
1713                node_idx, r_index,
1714                node_idx, index);
1715        break;
1716    default:
1717        fail("unkown formula type");
1718    }
1719}
1720   
1721
1722
Note: See TracBrowser for help on using the repository browser.