- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00017 #include "ltlInt.h" 00018 00019 static char rcsid[] UNUSED = "$Id: ltlCompose.c,v 1.30 2005/04/28 08:51:19 bli Exp $"; 00020 00021 /*---------------------------------------------------------------------------*/ 00022 /* Constant declarations */ 00023 /*---------------------------------------------------------------------------*/ 00024 00025 /*---------------------------------------------------------------------------*/ 00026 /* Structure declarations */ 00027 /*---------------------------------------------------------------------------*/ 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Type declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 /*---------------------------------------------------------------------------*/ 00034 /* Variable declarations */ 00035 /*---------------------------------------------------------------------------*/ 00036 00037 /*---------------------------------------------------------------------------*/ 00038 /* Macro declarations */ 00039 /*---------------------------------------------------------------------------*/ 00040 00043 /*---------------------------------------------------------------------------*/ 00044 /* Static function prototypes */ 00045 /*---------------------------------------------------------------------------*/ 00046 00047 static void AutomatonGetInputNames(Ltl_Automaton_t *A, array_t *InputNames, array_t *Name2LabelIdx); 00048 static int AutomatonCountSelector(Ltl_Automaton_t *A); 00049 static int AutomatonComputeInitState(Ltl_Automaton_t *A); 00050 /*static lsList AutomatonLabelGetCubes(Ltl_Automaton_t *A, LtlSet_t *compositeLabel, Ntk_Network_t *network);*/ 00051 static lsList GetCubes_Aux(Ltl_Automaton_t *A, int index); 00052 static char * StringNormalize(char *inputString); 00053 static void AutomatonVtxLabelToBlifMv(FILE *fp, Ltl_Automaton_t *A, vertex_t *vtx); 00054 static void VtxLabelToBlifMv_Aux(FILE *fp, Ltl_Automaton_t *A, int node_idx, int index, st_table *CreatedSignals); 00055 00058 /*---------------------------------------------------------------------------*/ 00059 /* Definition of exported functions */ 00060 /*---------------------------------------------------------------------------*/ 00061 00073 void 00074 Ltl_AutomatonToDot( 00075 FILE *fp, 00076 Ltl_Automaton_t *aut, 00077 int level) 00078 { 00079 edge_t *edge; 00080 vertex_t *vtx1, *vtx2; 00081 Ltl_AutomatonNode_t *node, *node2; 00082 lsGen lsgen, lsgen2; 00083 st_table *FairSet; 00084 st_generator *stgen; 00085 Ctlsp_Formula_t *F; 00086 char *tmpString; 00087 int fairindex, first, i, n; 00088 00089 /*------------------------------------------------- 00090 * digraph "G(F(p=1))" { 00091 * node [shape=ellipse]; 00092 * size = "7.5,10" 00093 * center = true; 00094 * "title" [label="G(F(p=1))", shape=plaintext]; 00095 *------------------------------------------------- 00096 */ 00097 if (aut->name) 00098 tmpString = aut->name; 00099 else 00100 tmpString = ""; 00101 00102 fprintf(fp, "\ndigraph \"%s\" {\nnode [shape=ellipse];\nsize = \"7.5,10\"\ncenter = true;\n\"title\" [label=\"%s\",shape=plaintext];", tmpString, tmpString); 00103 00104 /*------------------------------------------------- 00105 * "n1" [label="n1\n{p=1}\n(1)"]; 00106 *------------------------------------------------- 00107 */ 00108 foreach_vertex( aut->G, lsgen, vtx1) { 00109 node = (Ltl_AutomatonNode_t *)vtx1->user_data; 00110 fprintf(fp,"\n\"n%d\" [label=\"n%d\\n{", node->index, node->index); 00111 if (node->Labels) { 00112 first = 1; n = array_n(aut->labelTable); 00113 for (i=0; i<n; i++) { 00114 if (LtlSetGetElt(node->Labels, i)) { 00115 if (!first) fprintf(fp, ","); 00116 else first = 0; 00117 F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i); 00118 Ctlsp_FormulaPrint(fp, F); 00119 } 00120 } 00121 } 00122 fprintf(fp, "}\\n("); 00123 fairindex = 1; 00124 lsForEachItem(aut->Fair, lsgen2, FairSet) { 00125 if (st_is_member(FairSet, vtx1)) 00126 fprintf(fp, " %d ", fairindex); 00127 fairindex++; 00128 } 00129 fprintf(fp, ")\"];"); 00130 } 00131 00132 /*------------------------------------------------- 00133 * "init-n2" [style=invis] 00134 * "init-n2" -> "n2"; 00135 *------------------------------------------------- 00136 */ 00137 st_foreach_item(aut->Init, stgen, &vtx1, NIL(char *)) { 00138 node = (Ltl_AutomatonNode_t *) vtx1->user_data; 00139 fprintf(fp, "\n\"init-n%d\" [style=invis]", node->index); 00140 fprintf(fp, "\n\"init-n%d\" -> \"n%d\";", node->index, node->index); 00141 } 00142 00143 00144 /*------------------------------------------------- 00145 * "n1" -> "n1"; 00146 *------------------------------------------------- 00147 */ 00148 foreach_edge(aut->G, lsgen, edge) { 00149 vtx1 = g_e_source(edge); 00150 vtx2 = g_e_dest(edge); 00151 node = (Ltl_AutomatonNode_t *) vtx1->user_data; 00152 node2 = (Ltl_AutomatonNode_t *) vtx2->user_data; 00153 fprintf(fp, "\n\"n%d\" -> \"n%d\";", node->index, node2->index); 00154 } 00155 fprintf(fp, "\n}\n"); 00156 } 00157 00158 00174 int 00175 Ltl_AutomatonToBlifMv( 00176 FILE *fp, 00177 Ntk_Network_t *network, 00178 Ltl_Automaton_t *A) 00179 { 00180 Var_Variable_t *inputVar; 00181 array_t *InputNames = array_alloc(char *, 0); 00182 array_t *Name2LabelIdx = array_alloc(st_table *, 0); 00183 Ntk_Node_t *ntknode; 00184 char *inputName; 00185 st_generator *stgen; 00186 lsGen lsgen, lsgen2; 00187 int i, j, is_enum, range; 00188 int sel_num, sel_cnt; 00189 edge_t *edge; 00190 vertex_t *vtx, *vtx2; 00191 st_table *FairSet, *tmptbl; 00192 int InitIdx = AutomatonComputeInitState(A); 00193 char InitStr[10]; 00194 int result = 1; 00195 array_t *labelArray; 00196 00197 /* The initState of the automaton */ 00198 if (InitIdx == -1) 00199 sprintf(InitStr, "Init"); 00200 else 00201 sprintf(InitStr, "n%d", InitIdx); 00202 00203 if (network == NIL(Ntk_Network_t)) { 00204 result = 0; 00205 fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n"); 00206 } 00207 00208 /* Retrieve all the input names on the labels; For each input, create a 00209 * hash table and add all the label subformulae contains that input; 00210 * Finally, calculate the size of the "selector" 00211 */ 00212 AutomatonGetInputNames(A, InputNames, Name2LabelIdx); 00213 sel_num = AutomatonCountSelector(A); 00214 fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name); 00215 00216 /*------------------------------------------------------- 00217 * .model Buechi$AUT 00218 * .root Buechi$AUT 00219 *------------------------------------------------------- 00220 */ 00221 fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT"); 00222 00223 /*------------------------------------------------------- 00224 * .inputs in1 in2 in3 ... inN 00225 *------------------------------------------------------- 00226 */ 00227 fprintf(fp, "\n.inputs "); 00228 for (i=0; i<array_n(InputNames); i++) { 00229 inputName = array_fetch(char *, InputNames, i); 00230 fprintf(fp, "%s ", inputName); 00231 } 00232 00233 /*------------------------------------------------------- 00234 * .outputs fair1 fair2 fair3... fairN 00235 *------------------------------------------------------- 00236 */ 00237 fprintf(fp, "\n.outputs "); 00238 if ( lsLength(A->Fair) != 0) { 00239 for (i=0; i<lsLength(A->Fair); i++) { 00240 fprintf(fp, "fair%d$AUT ", i+1); 00241 } 00242 }else 00243 fprintf(fp, "fair1$AUT"); 00244 00245 /*------------------------------------------------------- 00246 * .mv in1 3 RED GREEN YELLOW 00247 *------------------------------------------------------- 00248 */ 00249 if (network != NIL(Ntk_Network_t)) { 00250 for (i=0; i<array_n(InputNames); i++) { 00251 inputName = array_fetch(char *, InputNames, i); 00252 ntknode = Ntk_NetworkFindNodeByName(network, inputName); 00253 assert(ntknode != NIL(Ntk_Node_t)); 00254 inputVar = Ntk_NodeReadVariable(ntknode); 00255 is_enum = Var_VariableTestIsEnumerative(inputVar); 00256 range = Var_VariableReadNumValues(inputVar); 00257 if (is_enum) { 00258 if (range != 2) 00259 fprintf(fp, "\n.mv %s %d\n", inputName, range); 00260 }else { 00261 fprintf(fp, "\n.mv %s %d ", inputName, range); 00262 for (j=0; j<range; j++) { 00263 fprintf(fp, "%s ", 00264 Var_VariableReadSymbolicValueFromIndex(inputVar,j)); 00265 } 00266 } 00267 } 00268 } 00269 00270 /*------------------------------------------------------- 00271 * .mv stateD$AUT N Init n1 n2 n3 ... nN 00272 * .mv state$AUT N Init n1 n2 n3 ... nN 00273 *------------------------------------------------------- 00274 */ 00275 if (InitIdx == -1) 00276 fprintf(fp, "\n.mv stateD$AUT %d Init Trap ", 00277 lsLength(g_get_vertices(A->G)) + 2); 00278 else 00279 fprintf(fp, "\n.mv stateD$AUT %d Trap ", 00280 lsLength(g_get_vertices(A->G)) + 1); 00281 foreach_vertex(A->G, lsgen, vtx) { 00282 fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00283 } 00284 if (InitIdx == -1) 00285 fprintf(fp, "\n.mv state$AUT %d Init Trap ", 00286 lsLength(g_get_vertices(A->G)) + 2); 00287 else 00288 fprintf(fp, "\n.mv state$AUT %d Trap ", 00289 lsLength(g_get_vertices(A->G)) + 1); 00290 foreach_vertex(A->G, lsgen, vtx) { 00291 fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00292 } 00293 00294 /*------------------------------------------------------- 00295 * .mv selector n 00296 * .table selector 00297 * - 00298 *------------------------------------------------------- 00299 */ 00300 if (sel_num > 1) 00301 fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num); 00302 00303 /*------------------------------------------------------- 00304 * for each state label, create a signal n1_##_label$AUT (recursively) 00305 *------------------------------------------------------- 00306 */ 00307 labelArray = array_alloc(vertex_t *, 0); 00308 foreach_vertex(A->G, lsgen, vtx) { 00309 AutomatonVtxLabelToBlifMv(fp, A, vtx); 00310 array_insert_last(vertex_t *, labelArray, vtx); 00311 } 00312 00313 /*------------------------------------------------------- 00314 * .latch stateD$AUT state$AUT 00315 * .reset state$AUT 00316 * Init (or ns) 00317 *------------------------------------------------------- 00318 */ 00319 fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s", 00320 InitStr); 00321 00322 00323 /*------------------------------------------------------ 00324 * .table selector$AUT state$AUT n1_label$AUT n2_label... -> stateD$AUT 00325 * .default Trap 00326 * 0 1 0 0 ... n1 00327 * 1 0 1 n2 00328 * ... 00329 *------------------------------------------------------ 00330 */ 00331 if (sel_num >1) 00332 fprintf(fp, "\n.table selector$AUT state$AUT "); 00333 else 00334 fprintf(fp, "\n.table state$AUT "); 00335 00336 arrayForEachItem(vertex_t *, labelArray, i, vtx) { 00337 fprintf(fp, "n%d_label$AUT ", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00338 } 00339 fprintf(fp, " -> stateD$AUT\n.default Trap"); 00340 00341 if (InitIdx == -1) { 00342 sel_cnt = 0; 00343 arrayForEachItem(vertex_t *, labelArray, i, vtx) { 00344 if (!st_is_member(A->Init, vtx)) 00345 continue; 00346 if (sel_num > 1) { 00347 if (st_count(A->Init) == 1) 00348 fprintf(fp, "\n- Init "); 00349 else 00350 fprintf(fp, "\n%d Init ", sel_cnt); 00351 }else 00352 fprintf(fp, "\nInit "); 00353 00354 for(j=0; j<array_n(labelArray); j++) 00355 fprintf(fp, "%s ", ((i==j)?"1":"-")); 00356 00357 fprintf(fp, " n%d", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00358 00359 if (sel_num > 1) 00360 sel_cnt++; 00361 } 00362 } 00363 00364 /* for each edge (n1, n2) with n2 labeled n2_label$AUT, add entry: 00365 *------------------------------------------------------- 00366 * selector 1 0 0 ... n1 00367 * selector 0 1 0 ... n2 00368 * ... 00369 *------------------------------------------------------- 00370 */ 00371 foreach_vertex(A->G, lsgen, vtx) { 00372 int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx); 00373 int outDegree = lsLength(g_get_out_edges(vtx)); 00374 sel_cnt = 0; 00375 foreach_out_edge(vtx, lsgen2, edge) { 00376 int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge)); 00377 00378 if (sel_num > 1) { 00379 if (outDegree == 1) 00380 fprintf(fp, "\n- n%d ", n1); 00381 else 00382 fprintf(fp, "\n%d n%d ", sel_cnt, n1); 00383 }else { 00384 fprintf(fp, "\nn%d ", n1); 00385 } 00386 00387 arrayForEachItem(vertex_t *, labelArray, i, vtx2) { 00388 fprintf(fp, "%s ", ((vtx2 == g_e_dest(edge))?"1":"-")); 00389 } 00390 fprintf(fp, " n%d", n2); 00391 00392 if (sel_num > 1) 00393 sel_cnt++; 00394 } 00395 } 00396 array_free(labelArray); 00397 00398 /*------------------------------------------------------- 00399 * .table state -> fair1 00400 * .default 0 00401 * ------------------------------------------------------ 00402 */ 00403 if (lsLength(A->Fair) != 0) { 00404 i = 1; 00405 lsForEachItem(A->Fair, lsgen, FairSet) { 00406 int isFirst = 1; 00407 fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++); 00408 fprintf(fp, "\n.default 0\n("); 00409 st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) { 00410 if (isFirst) 00411 isFirst = 0; 00412 else 00413 fprintf(fp, ","); 00414 fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00415 } 00416 fprintf(fp, ") 1"); 00417 } 00418 }else { 00419 fprintf(fp, "\n.table state$AUT -> fair1$AUT "); 00420 if (InitIdx == -1) 00421 fprintf(fp, "\n.default 0\n!(Trap,Init) 1"); 00422 else 00423 fprintf(fp, "\n.default 0\n!(Trap) 1"); 00424 } 00425 00426 /*------------------------------------------------------- 00427 * .end 00428 * ------------------------------------------------------ 00429 */ 00430 fprintf(fp, "\n.end\n"); 00431 00432 /* free the name array 00433 */ 00434 array_free(InputNames); 00435 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) { 00436 st_free_table(tmptbl); 00437 } 00438 array_free(Name2LabelIdx); 00439 00440 return result; 00441 } 00442 00443 #if 0 00444 int 00445 Ltl_AutomatonToBlifMv_Old( 00446 FILE *fp, 00447 Ntk_Network_t *network, 00448 Ltl_Automaton_t *A) 00449 { 00450 Var_Variable_t *inputVar; 00451 array_t *InputNames = array_alloc(char *, 0); 00452 array_t *Name2LabelIdx = array_alloc(st_table *, 0); 00453 Ntk_Node_t *ntknode; 00454 char *inputName; 00455 st_generator *stgen, *stgen2; 00456 lsGen lsgen, lsgen2, lsgen3; 00457 int i, j, is_enum, range; 00458 long index; 00459 int sel_num, sel_cnt; 00460 edge_t *edge; 00461 vertex_t *vtx; 00462 st_table *FairSet, *tmptbl; 00463 LtlSet_t *label; 00464 int InitIdx = AutomatonComputeInitState(A); 00465 char InitStr[10]; 00466 int result = 1; 00467 00468 /* The initState of the automaton */ 00469 if (InitIdx == -1) 00470 sprintf(InitStr, "Init"); 00471 else 00472 sprintf(InitStr, "n%d", InitIdx); 00473 00474 if (network == NIL(Ntk_Network_t)) { 00475 result = 0; 00476 fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n"); 00477 } 00478 00479 /* Retrieve all the input names on the labels; For each input, create a 00480 * hash table and add all the label subformulae contains that input; 00481 * Finally, calculate the size of the "selector" 00482 */ 00483 AutomatonGetInputNames(A, InputNames, Name2LabelIdx); 00484 sel_num = AutomatonCountSelector(A); 00485 fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name); 00486 00487 /*------------------------------------------------------- 00488 * .model Buechi$AUT 00489 * .root Buechi$AUT 00490 *------------------------------------------------------- 00491 */ 00492 fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT"); 00493 00494 /*------------------------------------------------------- 00495 * .inputs in1 in2 in3 ... inN 00496 *------------------------------------------------------- 00497 */ 00498 fprintf(fp, "\n.inputs "); 00499 for (i=0; i<array_n(InputNames); i++) { 00500 inputName = array_fetch(char *, InputNames, i); 00501 fprintf(fp, "%s ", inputName); 00502 } 00503 00504 /*------------------------------------------------------- 00505 * .outputs fair1 fair2 fair3... fairN 00506 *------------------------------------------------------- 00507 */ 00508 fprintf(fp, "\n.outputs "); 00509 if ( lsLength(A->Fair) != 0) { 00510 for (i=0; i<lsLength(A->Fair); i++) { 00511 fprintf(fp, "fair%d$AUT ", i+1); 00512 } 00513 }else 00514 fprintf(fp, "fair1$AUT"); 00515 00516 /*------------------------------------------------------- 00517 * .mv in1 3 RED GREEN YELLOW 00518 *------------------------------------------------------- 00519 */ 00520 if (network != NIL(Ntk_Network_t)) { 00521 for (i=0; i<array_n(InputNames); i++) { 00522 inputName = array_fetch(char *, InputNames, i); 00523 ntknode = Ntk_NetworkFindNodeByName(network, inputName); 00524 assert(ntknode != NIL(Ntk_Node_t)); 00525 inputVar = Ntk_NodeReadVariable(ntknode); 00526 is_enum = Var_VariableTestIsEnumerative(inputVar); 00527 range = Var_VariableReadNumValues(inputVar); 00528 if (is_enum) { 00529 if (range != 2) 00530 fprintf(fp, "\n.mv %s %d\n", inputName, range); 00531 }else { 00532 fprintf(fp, "\n.mv %s %d ", inputName, range); 00533 for (j=0; j<range; j++) { 00534 fprintf(fp, "%s ", 00535 Var_VariableReadSymbolicValueFromIndex(inputVar,j)); 00536 } 00537 } 00538 } 00539 } 00540 00541 /*------------------------------------------------------- 00542 * .mv stateD$AUT N Init n1 n2 n3 ... nN 00543 * .mv state$AUT N Init n1 n2 n3 ... nN 00544 *------------------------------------------------------- 00545 */ 00546 if (InitIdx == -1) 00547 fprintf(fp, "\n.mv stateD$AUT %d Init Trap ", 00548 lsLength(g_get_vertices(A->G)) + 2); 00549 else 00550 fprintf(fp, "\n.mv stateD$AUT %d Trap ", 00551 lsLength(g_get_vertices(A->G)) + 1); 00552 foreach_vertex(A->G, lsgen, vtx) { 00553 fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00554 } 00555 if (InitIdx == -1) 00556 fprintf(fp, "\n.mv state$AUT %d Init Trap ", 00557 lsLength(g_get_vertices(A->G)) + 2); 00558 else 00559 fprintf(fp, "\n.mv state$AUT %d Trap ", 00560 lsLength(g_get_vertices(A->G)) + 1); 00561 foreach_vertex(A->G, lsgen, vtx) { 00562 fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00563 } 00564 00565 /*------------------------------------------------------- 00566 * .mv selector n 00567 * .table selector 00568 * - 00569 *------------------------------------------------------- 00570 */ 00571 if (sel_num > 1) 00572 fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num); 00573 00574 /*------------------------------------------------------- 00575 * .latch stateD$AUT state$AUT 00576 * .reset state$AUT 00577 * Init (or ns) 00578 *------------------------------------------------------- 00579 */ 00580 fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s", 00581 InitStr); 00582 00583 /*------------------------------------------------------ 00584 * .table selector$AUT state$AUT in1 in2 ... inN -> stateD$AUT 00585 * .default Trap 00586 *------------------------------------------------------ 00587 */ 00588 if (sel_num >1) 00589 fprintf(fp, "\n.table selector$AUT state$AUT "); 00590 else 00591 fprintf(fp, "\n.table state$AUT "); 00592 00593 for (i=0; i<array_n(InputNames); i++) { 00594 inputName = array_fetch(char *, InputNames, i); 00595 fprintf(fp, "%s ", inputName); 00596 } 00597 fprintf(fp, " -> stateD$AUT\n.default Trap"); 00598 00599 00600 /* for each initial state n2 with label "in1=p !in3=q...", add entry: 00601 *------------------------------------------------------- 00602 * selector Init (p) - (!(q)) .. n2 00603 *------------------------------------------------------- 00604 */ 00605 if (InitIdx == -1) { 00606 sel_cnt = 0; 00607 st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) { 00608 int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx); 00609 /* each 'compLabel' is a set of "propositional formulae" */ 00610 LtlSet_t *compLabel = LtlAutomatonVertexGetLabels(vtx); 00611 /* each item in labelList is a set of "atomic proposition" */ 00612 lsList labelList = AutomatonLabelGetCubes(A, compLabel, network); 00613 lsForEachItem(labelList, lsgen, label) { 00614 if (sel_num > 1) { 00615 if (st_count(A->Init) == 1) 00616 fprintf(fp, "\n- Init "); 00617 else 00618 fprintf(fp, "\n%d Init ", sel_cnt); 00619 }else 00620 fprintf(fp, "\nInit "); 00621 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) { 00622 int isFirst = 1; 00623 int is_universe = 1; 00624 /* The value is the universe '-' iff it is not in the label */ 00625 if (!LtlSetIsEmpty(label)) { 00626 st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) { 00627 if (LtlSetGetElt(label, (int) index)) { 00628 is_universe = 0; 00629 st_free_gen(stgen2); 00630 break; 00631 } 00632 } 00633 } 00634 if (is_universe) { 00635 fprintf(fp, "- "); 00636 continue; 00637 } 00638 /* Otherwise, write the value. Note that the value should be 00639 * the conjunction of the values of the atomic propositions. 00640 * A * B * C = !(!A + !B +!C) 00641 */ 00642 fprintf(fp, "!("); 00643 st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) { 00644 if (LtlSetGetElt(label, (int) index)) { 00645 Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, 00646 A->labelTable, 00647 (int) index); 00648 if (isFirst) 00649 isFirst = 0; 00650 else 00651 fprintf(fp, ","); 00652 if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c) { 00653 F = Ctlsp_FormulaReadLeftChild(F); 00654 }else { 00655 fprintf(fp, "!"); 00656 } 00657 00658 fprintf(fp, "(%s)", Ctlsp_FormulaReadValueName(F)); 00659 } 00660 } 00661 fprintf(fp, ") "); 00662 } 00663 fprintf(fp, " n%d", n2); 00664 } 00665 lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree); 00666 00667 if (sel_num > 1) 00668 sel_cnt++; 00669 } 00670 } 00671 00672 /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry: 00673 *------------------------------------------------------- 00674 * selector n1 (p) - (!(q)) ... n2 00675 *------------------------------------------------------- 00676 */ 00677 foreach_vertex(A->G, lsgen, vtx) { 00678 int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx); 00679 int outDegree = lsLength(g_get_out_edges(vtx)); 00680 sel_cnt = 0; 00681 foreach_out_edge(vtx, lsgen2, edge) { 00682 int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge)); 00683 /* 'compLabel' contains a set of "propositional formulae" */ 00684 LtlSet_t *compLabel = LtlAutomatonVertexGetLabels(g_e_dest(edge)); 00685 /* each item in 'labelList' is a set of "atomic propositions" */ 00686 lsList labelList = AutomatonLabelGetCubes(A, compLabel, network); 00687 lsForEachItem(labelList, lsgen3, label) { 00688 if (sel_num > 1) { 00689 if (outDegree == 1) 00690 fprintf(fp, "\n- n%d ", n1); 00691 else 00692 fprintf(fp, "\n%d n%d ", sel_cnt, n1); 00693 }else { 00694 fprintf(fp, "\nn%d ", n1); 00695 } 00696 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) { 00697 int isFirst = 1; 00698 int is_universe = 1; 00699 /* the value is universe '-' iff it is not in the label */ 00700 if (!LtlSetIsEmpty(label)) { 00701 st_foreach_item(tmptbl,stgen2,&index, NIL(char *)){ 00702 if (LtlSetGetElt(label, (int) index)) { 00703 is_universe = 0; 00704 st_free_gen(stgen2); 00705 break; 00706 } 00707 } 00708 } 00709 if (is_universe) { 00710 fprintf(fp, "- "); 00711 continue; 00712 } 00713 /* write the value as the conjunction of the values in the 00714 * atomic proposition. for example, if the state is labeled 00715 * 'in1={R,G,B}' and 'in1={G}', we should write as 00716 * !( !(R,G,B), !(G) ) 00717 * Note that it's the same as {R,G,B}^{G}={G} 00718 */ 00719 fprintf(fp, "!("); 00720 st_foreach_item(tmptbl, stgen, &index, NIL(char *)) { 00721 if (LtlSetGetElt(label, (int) index)) { 00722 Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, 00723 A->labelTable, 00724 (int) index); 00725 if (isFirst) 00726 isFirst = 0; 00727 else 00728 fprintf(fp, ","); 00729 if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c) 00730 F = Ctlsp_FormulaReadLeftChild(F); 00731 else 00732 fprintf(fp, "!"); 00733 fprintf(fp, "(%s)", Ctlsp_FormulaReadValueName(F)); 00734 } 00735 } 00736 fprintf(fp, ") "); 00737 } 00738 fprintf(fp, " n%d", n2); 00739 } 00740 lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree); 00741 00742 if (sel_num > 1) 00743 sel_cnt++; 00744 } 00745 } 00746 00747 00748 /*------------------------------------------------------- 00749 * .table state -> fair1 00750 * .default 0 00751 * ------------------------------------------------------ 00752 */ 00753 if (lsLength(A->Fair) != 0) { 00754 i = 1; 00755 lsForEachItem(A->Fair, lsgen, FairSet) { 00756 int isFirst = 1; 00757 fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++); 00758 fprintf(fp, "\n.default 0\n("); 00759 st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) { 00760 if (isFirst) 00761 isFirst = 0; 00762 else 00763 fprintf(fp, ","); 00764 fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00765 } 00766 fprintf(fp, ") 1"); 00767 } 00768 }else { 00769 fprintf(fp, "\n.table state$AUT -> fair1$AUT "); 00770 if (InitIdx == -1) 00771 fprintf(fp, "\n.default 0\n!(Trap,Init) 1"); 00772 else 00773 fprintf(fp, "\n.default 0\n!(Trap) 1"); 00774 } 00775 00776 /*------------------------------------------------------- 00777 * .end 00778 * ------------------------------------------------------ 00779 */ 00780 fprintf(fp, "\n.end\n"); 00781 00782 /* free the name array 00783 */ 00784 array_free(InputNames); 00785 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) { 00786 st_free_table(tmptbl); 00787 } 00788 array_free(Name2LabelIdx); 00789 00790 return result; 00791 } 00792 #endif 00793 00794 00807 int 00808 Ltl_AutomatonToVerilog( 00809 FILE *fp, 00810 Ntk_Network_t *network, 00811 Ltl_Automaton_t *A) 00812 { 00813 Var_Variable_t *inputVar; 00814 array_t *InputNames = array_alloc(char *, 0); 00815 array_t *Name2LabelIdx = array_alloc(st_table *, 0); 00816 Ntk_Node_t *ntknode; 00817 char *inputName, *formulaString, *normalString; 00818 st_generator *stgen; 00819 lsGen lsgen, lsgen2; 00820 int i, j, is_enum, range, isFirst; 00821 int sel_num, sel_cnt; 00822 edge_t *edge; 00823 vertex_t *vtx; 00824 st_table *FairSet; 00825 int InitIdx = AutomatonComputeInitState(A); 00826 char InitStr[10]; 00827 int result = 1; 00828 00829 /* The initState of the automaton */ 00830 if (InitIdx == -1) 00831 sprintf(InitStr, "Init"); 00832 else 00833 sprintf(InitStr, "n%d", InitIdx); 00834 00835 if (network == NIL(Ntk_Network_t)) { 00836 result = 0; 00837 fprintf(vis_stderr, "Warning: the Verilog output is incomplete. (The current node is empty. Read in design.)\n"); 00838 } 00839 00840 /* Retrieve all the input names of the automaton into 'InputNames', And for 00841 * each name, put into a hash table all the subformulae contains it 00842 */ 00843 AutomatonGetInputNames(A, InputNames, Name2LabelIdx); 00844 sel_num = AutomatonCountSelector(A); 00845 fprintf(fp, "\n// Buechi automaton: %s", A->name); 00846 00847 /*------------------------------------------------------- 00848 * typedef enum {Init, trap, n1, n2, ... nN} states; 00849 * typedef enum {READ, GREEN, YELLOW} type_in1; 00850 *------------------------------------------------------- 00851 */ 00852 if (InitIdx == -1) 00853 fprintf(fp, "\ntypedef enum {Init,Trap"); 00854 else 00855 fprintf(fp, "\ntypedef enum {Trap"); 00856 foreach_vertex(A->G, lsgen, vtx) { 00857 fprintf(fp, ",n%d", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00858 } 00859 fprintf(fp, "} type_states;"); 00860 00861 if (network != NIL(Ntk_Network_t)) { 00862 arrayForEachItem(char *, InputNames, i, inputName) { 00863 /* replace illegal characters in the input name string */ 00864 normalString = StringNormalize(inputName); 00865 fprintf(fp, "\n//Input name mapping:\t %s => %s;", inputName, 00866 normalString); 00867 00868 ntknode = Ntk_NetworkFindNodeByName(network, inputName); 00869 assert(ntknode != NIL(Ntk_Node_t)); 00870 inputVar = Ntk_NodeReadVariable(ntknode); 00871 00872 is_enum = Var_VariableTestIsEnumerative(inputVar); 00873 range = Var_VariableReadNumValues(inputVar); 00874 if (is_enum) { 00875 if (range>2) 00876 fprintf(fp, "\ntypedef enum {0-%d} type_%s;", 00877 range-1, normalString); 00878 }else { 00879 fprintf(fp, "\ntypedef enum {"); 00880 isFirst = 1; 00881 for (j=0; j<range; j++) { 00882 char *vstr = 00883 Var_VariableReadSymbolicValueFromIndex(inputVar,j); 00884 if (isFirst) { 00885 fprintf(fp, "%s ", vstr); 00886 isFirst = 0; 00887 } else 00888 fprintf(fp, ",%s ", vstr); 00889 } 00890 fprintf(fp, "} type_%s;", normalString); 00891 } 00892 00893 FREE(normalString); 00894 } 00895 } 00896 00897 /*------------------------------------------------------- 00898 * module Buechi (clock, in1, in2 ... inN, fair1, ...); 00899 *------------------------------------------------------- 00900 */ 00901 fprintf(fp, "\n//Buechi Buechi (clock"); 00902 for (i=0; i<array_n(InputNames); i++) { 00903 inputName = array_fetch(char *, InputNames, i); 00904 fprintf(fp, ",%s", inputName); 00905 } 00906 for (i=0; i<lsLength(A->Fair); i++) { 00907 fprintf(fp, ",fair%d", i+1); 00908 } 00909 fprintf(fp, ");"); 00910 00911 fprintf(fp, "\nmodule Buechi (clock"); 00912 for (i=0; i<array_n(InputNames); i++) { 00913 inputName = array_fetch(char *, InputNames, i); 00914 normalString = StringNormalize(inputName); 00915 fprintf(fp, ",%s", normalString); 00916 FREE(normalString); 00917 } 00918 for (i=0; i<lsLength(A->Fair); i++) { 00919 fprintf(fp, ",fair%d", i+1); 00920 } 00921 fprintf(fp, ");"); 00922 00923 00924 /*------------------------------------------------------- 00925 * input clock, in1, in2 ... inN ; 00926 * output fair1, fair2 ... fairN ; 00927 *------------------------------------------------------- 00928 */ 00929 fprintf(fp, "\n\tinput clock"); 00930 for (i=0; i<array_n(InputNames); i++) { 00931 inputName = array_fetch(char *, InputNames, i); 00932 normalString = StringNormalize(inputName); 00933 fprintf(fp, ", %s", normalString); 00934 FREE(normalString); 00935 } 00936 if (lsLength(A->Fair)>0) { 00937 fprintf(fp, ";\n\toutput "); 00938 isFirst = 1; 00939 for (i=0; i<lsLength(A->Fair); i++) { 00940 if (isFirst) { 00941 fprintf(fp, "fair%d", i+1); 00942 isFirst = 0; 00943 } else { 00944 fprintf(fp, ",fair%d", i+1); 00945 } 00946 } 00947 } 00948 fprintf(fp, ";"); 00949 00950 00951 /*------------------------------------------------------- 00952 * type_in1 wire in1; 00953 * type_in2 wire in2; 00954 * ... 00955 * type_states reg state; 00956 * wire[0:logN] sel; 00957 *------------------------------------------------------- 00958 */ 00959 if (network != NIL(Ntk_Network_t)) { 00960 arrayForEachItem(char *, InputNames, i, inputName) { 00961 normalString = StringNormalize(inputName); 00962 00963 ntknode = Ntk_NetworkFindNodeByName(network, inputName); 00964 assert(ntknode != NIL(Ntk_Node_t)); 00965 inputVar = Ntk_NodeReadVariable(ntknode); 00966 00967 is_enum = Var_VariableTestIsEnumerative(inputVar); 00968 range = Var_VariableReadNumValues(inputVar); 00969 00970 if (!is_enum || range > 2) 00971 fprintf(fp, "\n\ttype_%s wire %s;", normalString,normalString); 00972 FREE(normalString); 00973 } 00974 } 00975 fprintf(fp, "\n\ttype_states reg state;"); 00976 if (sel_num >1) { 00977 if (sel_num == 2) 00978 fprintf(fp, "\n\twire sel;"); 00979 else 00980 fprintf(fp, "\n\twire [0:%d] sel;", (int)(ceil(log(sel_num)))-1); 00981 } 00982 00983 /*------------------------------------------------------- 00984 * assign sel = $ND( {0-N} ); 00985 * assign fair = (state==n1 || state==n2 || ... ); 00986 *------------------------------------------------------- 00987 */ 00988 fprintf(fp, "\n\tassign sel = $ND( {0-%d} );", sel_num-1 ); 00989 i = 1; 00990 lsForEachItem(A->Fair, lsgen, FairSet) { 00991 int isFirst = 1; 00992 fprintf(fp, "\n\tassign fair%d = (state==", i++); 00993 st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) { 00994 if (isFirst) 00995 isFirst = 0; 00996 else 00997 fprintf(fp, "|| state=="); 00998 fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx)); 00999 } 01000 fprintf(fp, ");"); 01001 } 01002 01003 /*------------------------------------------------------- 01004 * initial state = Init; 01005 *------------------------------------------------------- 01006 */ 01007 fprintf(fp, "\n\tinitial state = %s;", InitStr); 01008 01009 /*------------------------------------------------------- 01010 * always @ (posedge clock) begin 01011 * case (state) 01012 *------------------------------------------------------- 01013 */ 01014 fprintf(fp, "\n\talways @ (posedge clock) begin"); 01015 fprintf(fp, "\n\t\tcase (state)"); 01016 01017 /* for each initial state n2 with label "in1=p !in3=q...", add entry: 01018 *------------------------------------------------------- 01019 * Init: 01020 * if( sel==0 && in1==p && !in3=q ... ) 01021 * state = n2; 01022 * else if( sel==1 && ...) 01023 * state = n3; 01024 * else 01025 * state = Trap; 01026 *------------------------------------------------------ 01027 */ 01028 if (InitIdx == -1) { 01029 fprintf(fp, "\n\t\tInit:"); 01030 sel_cnt = 0; 01031 st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) { 01032 int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx); 01033 LtlSet_t *label = LtlAutomatonVertexGetLabels(vtx); 01034 01035 /* universal label (no label) on n2 */ 01036 if (LtlSetIsEmpty(label)) { 01037 if (st_count(A->Init) == 1 || sel_num == 0) 01038 fprintf(fp,"\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2); 01039 else if (sel_cnt == 0) 01040 fprintf(fp,"\n\t\t\tif(sel==%d)\n\t\t\t\tstate = n%d;", 01041 sel_cnt++, n2); 01042 else 01043 fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;", 01044 sel_cnt++, n2); 01045 }else { 01046 /* there is at least one label on n2 */ 01047 if (st_count(A->Init) == 1 || sel_num == 0) 01048 fprintf(fp, "\n\t\t\tif("); 01049 else if (sel_cnt==0) 01050 fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++); 01051 else 01052 fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++); 01053 01054 isFirst = 1; 01055 for (i=0; i<array_n(A->labelTable); i++) { 01056 if (LtlSetGetElt(label, i)) { 01057 Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, 01058 A->labelTable, i); 01059 formulaString = Ctlsp_FormulaConvertToString(F); 01060 normalString = StringNormalize(formulaString); 01061 FREE(formulaString); 01062 01063 if (isFirst) 01064 isFirst = 0; 01065 else 01066 fprintf(fp, " && "); 01067 01068 fprintf(fp, "%s", normalString); 01069 FREE(normalString); 01070 } 01071 } 01072 fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2); 01073 } 01074 } 01075 fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;"); 01076 } 01077 01078 /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry: 01079 *------------------------------------------------------- 01080 * n1: 01081 * if( sel==0 && in1==p && !in3=q ... ) 01082 * state = n2; 01083 * else if( sel==1 && ...) 01084 * state = n3; 01085 * else 01086 * state = Trap; 01087 *------------------------------------------------------- 01088 */ 01089 foreach_vertex(A->G, lsgen, vtx) { 01090 int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx); 01091 int outDegree = lsLength(g_get_out_edges(vtx)); 01092 fprintf(fp, "\n\t\tn%d:", n1); 01093 sel_cnt = 0; 01094 foreach_out_edge(vtx, lsgen2, edge) { 01095 int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge)); 01096 LtlSet_t *label = LtlAutomatonVertexGetLabels(g_e_dest(edge)); 01097 01098 /* universal label (no label) on n2 */ 01099 if (LtlSetIsEmpty(label)) { 01100 if (outDegree == 1 || sel_num == 0) 01101 fprintf(fp, "\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2); 01102 else if (sel_cnt == 0) 01103 fprintf(fp, "\n\t\t\tif(sel==%d) \n\t\t\t\tstate = n%d;", 01104 sel_cnt++, n2); 01105 else 01106 fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;", 01107 sel_cnt++, n2); 01108 }else { 01109 /* at least 1 label on n2 */ 01110 if (outDegree == 1 || sel_num == 0) 01111 fprintf(fp, "\n\t\t\tif("); 01112 else if (sel_cnt==0) 01113 fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++); 01114 else 01115 fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++); 01116 01117 isFirst = 1; 01118 for (i=0; i<array_n(A->labelTableNegate); i++) { 01119 if (LtlSetGetElt(label, i)) { 01120 Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, 01121 A->labelTable, i); 01122 formulaString = Ctlsp_FormulaConvertToString(F); 01123 normalString = StringNormalize(formulaString); 01124 FREE(formulaString); 01125 01126 if (isFirst) isFirst = 0; 01127 else fprintf(fp, " && "); 01128 01129 fprintf(fp, "%s", normalString); 01130 FREE(normalString); 01131 } 01132 } 01133 fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2); 01134 } 01135 } 01136 fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;"); 01137 } 01138 01139 /*------------------------------------------------------- 01140 * default: state = Trap; 01141 * endcase 01142 * end 01143 * endmodule 01144 *------------------------------------------------------- 01145 */ 01146 fprintf(fp, "\n\t\tdefault: state = Trap;\n\t\tendcase\n\tend\nendmodule\n"); 01147 01148 /* free the name array */ 01149 array_free(InputNames); 01150 for(i=0; i<array_n(Name2LabelIdx); i++) { 01151 st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, i); 01152 st_free_table(tmptbl); 01153 } 01154 array_free(Name2LabelIdx); 01155 01156 return result; 01157 } 01158 01159 01172 int 01173 Ltl_AutomatonToSmv( 01174 FILE *fp, 01175 Ntk_Network_t *network, 01176 Ltl_Automaton_t *A) 01177 { 01178 return 1; 01179 } 01180 01181 /*---------------------------------------------------------------------------*/ 01182 /* Definition of static functions */ 01183 /*---------------------------------------------------------------------------*/ 01184 01185 01198 static void 01199 AutomatonGetInputNames( 01200 Ltl_Automaton_t *A, 01201 array_t *InputNames, 01202 array_t *Name2LabelIdx) 01203 { 01204 st_table *Visited = st_init_table(strcmp, st_strhash); 01205 Ctlsp_Formula_t *F; 01206 Ctlsp_FormulaType F_type; 01207 long i, index, counter; 01208 01209 counter = 0; 01210 for (i=0; i<array_n(A->labelTable); i++) { 01211 /* get the positive formula string */ 01212 F = array_fetch(Ctlsp_Formula_t *, A->labelTable, i); 01213 F_type = Ctlsp_FormulaReadType(F); 01214 /* if it's not an AP (just a propositional formula), skip ... */ 01215 if (F_type != Ctlsp_NOT_c && F_type != Ctlsp_ID_c) 01216 continue; 01217 if (F_type == Ctlsp_NOT_c) 01218 F = Ctlsp_FormulaReadLeftChild(F); 01219 /* put into the InputNames array */ 01220 if (!st_lookup(Visited, Ctlsp_FormulaReadVariableName(F),&index)){ 01221 st_table *tmptbl = st_init_table(st_numcmp, st_numhash); 01222 st_insert(tmptbl, (char *) i, (char *)i); 01223 01224 array_insert(st_table *, Name2LabelIdx, counter, tmptbl); 01225 array_insert(char *, InputNames, counter, 01226 Ctlsp_FormulaReadVariableName(F)); 01227 01228 st_insert(Visited, Ctlsp_FormulaReadVariableName(F), (char *)counter++); 01229 }else { 01230 st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, index); 01231 st_insert(tmptbl, (char *)i, (char *)i); 01232 } 01233 } 01234 01235 st_free_table(Visited); 01236 } 01237 01251 static int 01252 AutomatonCountSelector( 01253 Ltl_Automaton_t *A) 01254 { 01255 int sel_num = st_count(A->Init); 01256 int local_num; 01257 lsGen lsgen; 01258 vertex_t *vtx; 01259 01260 foreach_vertex(A->G, lsgen, vtx) { 01261 local_num = lsLength(g_get_out_edges(vtx)); 01262 if (sel_num < local_num) 01263 sel_num = local_num; 01264 } 01265 01266 return sel_num; 01267 } 01268 01269 01285 static int 01286 AutomatonComputeInitState( 01287 Ltl_Automaton_t *A) 01288 { 01289 int initIdx = -1; 01290 vertex_t *vtx, *vtx2, *s; 01291 edge_t *e; 01292 st_generator *stgen, *stgen2; 01293 lsGen lsgen; 01294 01295 st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) { 01296 int isInit = 1; 01297 /* first, compute the set of sucessors of 'vtx' */ 01298 lsList Img = g_get_out_edges(vtx); 01299 st_table *uTable = st_init_table(st_ptrcmp, st_ptrhash); 01300 lsForEachItem(Img, lsgen, e) { 01301 s = g_e_dest(e); 01302 st_insert(uTable, s, s); 01303 } 01304 /* then, test if it is equivalent to 'A->Init': No more, No less */ 01305 st_foreach_item(A->Init, stgen2, &vtx2, NIL(char *)) { 01306 if (!st_is_member(uTable, vtx2)) { 01307 isInit = 0; 01308 st_free_gen(stgen2); 01309 break; 01310 } 01311 } 01312 if (isInit) { 01313 st_foreach_item(uTable, stgen2, &vtx2, NIL(char *)) { 01314 if (!st_is_member(A->Init, vtx2)) { 01315 isInit = 0; 01316 st_free_gen(stgen2); 01317 break; 01318 } 01319 } 01320 } 01321 st_free_table(uTable); 01322 01323 if (isInit == 1) { 01324 initIdx = ((Ltl_AutomatonNode_t *)vtx->user_data)->index; 01325 st_free_gen(stgen); 01326 break; 01327 } 01328 } 01329 01330 return initIdx; 01331 } 01332 01343 /*static lsList 01344 AutomatonLabelGetCubes( 01345 Ltl_Automaton_t *A, 01346 LtlSet_t *compositeLabel, 01347 Ntk_Network_t *network) 01348 { 01349 LtlTableau_t *tableau = A->tableau; 01350 int size = tableau->labelIndex; 01351 LtlSet_t *tempSet, *tempSet2, *tempSet3; 01352 lsList conjunctList; 01353 lsList disjunctList; 01354 lsList tempList, tempList2, tempList3; 01355 lsGen lsgen, lsgen2; 01356 int i; 01357 01358 if (LtlSetIsEmpty(compositeLabel)) { 01359 tempList = lsCreate(); 01360 lsNewEnd(tempList, (lsGeneric)LtlSetNew(size), (lsHandle *)0); 01361 return tempList; 01362 } 01363 01364 first, get a list of disjunctLists (which should be conjoin together 01365 to form a cartesian product 01366 01367 conjunctList = lsCreate(); 01368 tempSet = LtlSetNew(size); 01369 for (i=0; i<size; i++) { 01370 if (LtlSetGetElt(compositeLabel, i)) { 01371 if (Ctlsp_LtlFormulaIsAtomicPropositional(tableau->labelTable[i])) 01372 LtlSetSetElt(tempSet, i); 01373 else { 01374 disjunctList = GetCubes_Aux(A, i); 01375 lsNewEnd(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0); 01376 } 01377 } 01378 } 01379 if (LtlSetIsEmpty(tempSet)) 01380 LtlSetFree(tempSet); 01381 else { 01382 disjunctList = lsCreate(); 01383 lsNewEnd(disjunctList, (lsGeneric)tempSet, (lsHandle *)0); 01384 lsNewBegin(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0); 01385 } 01386 01387 01388 compute the cartesian product of the conjuncts 01389 while(lsLength(conjunctList)>1) { 01390 lsList thisList; 01391 lsList leftList; 01392 lsList rightList; 01393 01394 lsDelBegin(conjunctList, (lsGeneric *)&leftList); 01395 lsDelBegin(conjunctList, (lsGeneric *)&rightList); 01396 form the cartesian product of the two lists 01397 thisList = lsCreate(); 01398 lsForEachItem(leftList, lsgen, tempSet) { 01399 lsForEachItem(rightList, lsgen2, tempSet2) { 01400 tempSet3 = LtlSetNew(size); 01401 LtlSetOR(tempSet3, tempSet, tempSet2); 01402 01403 if (0) 01404 fprintf(vis_stdout, 01405 "tempSet = %d tempSet2 = %d tempSet3 = %d\n", 01406 LtlSetIsEmpty(tempSet), 01407 LtlSetIsEmpty(tempSet2), 01408 LtlSetIsEmpty(tempSet3)); 01409 01410 if no contradictory, retain it 01411 if (LtlSetIsContradictory(tempSet3,tableau->labelTableNegate)) 01412 LtlSetFree(tempSet3); 01413 else 01414 lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0); 01415 } 01416 } 01417 lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree); 01418 lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree); 01419 01420 lsNewBegin(conjunctList, (lsGeneric)thisList, (lsHandle *)0); 01421 } 01422 01423 lsDelBegin(conjunctList, (lsGeneric *)&tempList); 01424 lsDestroy(conjunctList, (void(*)(lsGeneric))0); 01425 01426 remove redundant minterms from 'tempList' 01427 tempList3 = lsCreate(); 01428 tempList2 = lsCopy(tempList, (lsGeneric(*)(lsGeneric))0); 01429 lsForEachItem(tempList, lsgen, tempSet) { 01430 If tempSet is a superset of other cubes, discard it 01431 int flag = 1; 01432 lsForEachItem(tempList2, lsgen2, tempSet2) { 01433 if (tempSet != tempSet2 && LtlSetInclude(tempSet, tempSet2)) { 01434 flag = 0; 01435 lsFinish(lsgen2); 01436 break; 01437 } 01438 } 01439 if (!flag) continue; 01440 If tempSet is an "emptyset" (for example, comtains both 01441 signal=0 and signal=1, where signal has only these two 01442 values), discard it 01443 01444 flag = 1; 01445 if (network != NIL(Ntk_Network_t)) { 01446 Fsm_Fsm_t *fsm = Fsm_NetworkReadOrCreateFsm(network); 01447 if (fsm != NIL(Fsm_Fsm_t)) { 01448 mdd_t *minterm = LtlSetModelCheckFormulae(tempSet, 01449 A->labelTable, 01450 fsm); 01451 flag = !(mdd_is_tautology(minterm, 0)); 01452 mdd_free(minterm); 01453 } 01454 } 01455 if (!flag) continue; 01456 otherwise, save a copy into tempList3 01457 lsNewBegin(tempList3, (lsGeneric)LtlSetCopy(tempSet), (lsHandle *)0); 01458 } 01459 lsDestroy(tempList2, (void(*)(lsGeneric))0); 01460 lsDestroy(tempList, (void (*)(lsGeneric))LtlSetFree); 01461 tempList = tempList3; 01462 01463 return tempList; 01464 } 01465 */ 01466 01478 static lsList 01479 GetCubes_Aux( 01480 Ltl_Automaton_t *A, 01481 int index) 01482 { 01483 Ctlsp_Formula_t *F = A->tableau->labelTable[index]; 01484 int size = A->tableau->labelIndex; 01485 lsList leftList; 01486 lsList rightList; 01487 lsList thisList =(lsList)0; 01488 lsGen lsgen, lsgen2; 01489 LtlSet_t *tempSet, *tempSet2, *tempSet3; 01490 01491 if (Ctlsp_LtlFormulaIsAtomicPropositional(F)) { 01492 thisList = lsCreate(); 01493 tempSet = LtlSetNew(size); 01494 LtlSetSetElt(tempSet, Ctlsp_FormulaReadLabelIndex(F)); 01495 lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0); 01496 }else { 01497 Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F); 01498 Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F); 01499 01500 switch(Ctlsp_FormulaReadType(F)) { 01501 case Ctlsp_OR_c: 01502 leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left)); 01503 rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right)); 01504 /* merge two list together */ 01505 thisList = leftList; 01506 lsForEachItem(rightList, lsgen, tempSet) { 01507 lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0); 01508 } 01509 lsDestroy(rightList, (void (*)(lsGeneric))0); 01510 break; 01511 case Ctlsp_AND_c: 01512 leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left)); 01513 rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right)); 01514 /* generate the cartesian product of the two lists */ 01515 thisList = lsCreate(); 01516 lsForEachItem(leftList, lsgen, tempSet) { 01517 lsForEachItem(rightList, lsgen2, tempSet2) { 01518 tempSet3 = LtlSetNew(size); 01519 LtlSetOR(tempSet3, tempSet, tempSet2); 01520 lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0); 01521 } 01522 } 01523 lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree); 01524 lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree); 01525 break; 01526 default: 01527 assert(0); 01528 break; 01529 } 01530 } 01531 01532 return thisList; 01533 } 01534 01535 01551 static char * 01552 StringNormalize( 01553 char *inputString) 01554 { 01555 char *normalString = ALLOC(char, strlen(inputString)*2); 01556 char *from = inputString; 01557 char *to = normalString; 01558 01559 while( *from ) { 01560 switch(*from) { 01561 case '=': 01562 *(to++) = '='; 01563 *(to) = '='; 01564 break; 01565 case '+': 01566 *(to++) = '|'; 01567 *(to) = '|'; 01568 break; 01569 case '*': 01570 *(to++) = '&'; 01571 *(to) = '&'; 01572 break; 01573 case '.': 01574 case '<': 01575 case '>': 01576 *(to) = '_'; 01577 break; 01578 default: 01579 *(to) = *from; 01580 } 01581 from++; 01582 to++; 01583 } 01584 *to = '\0'; 01585 01586 return normalString; 01587 } 01588 01610 static void 01611 AutomatonVtxLabelToBlifMv( 01612 FILE *fp, 01613 Ltl_Automaton_t *A, 01614 vertex_t *vtx) 01615 { 01616 /* each 'compLabel' is a "propositional formulae" */ 01617 LtlSet_t *compositeLabel = LtlAutomatonVertexGetLabels(vtx); 01618 int idx = Ltl_AutomatonVtxGetNodeIdx(vtx); 01619 int size = A->tableau->labelIndex; 01620 int i; 01621 st_table *CreatedSignals; 01622 01623 if (LtlSetIsEmpty(compositeLabel)) { 01624 fprintf(fp, "\n.table n%d_label$AUT\n1\n", idx); 01625 return; 01626 } 01627 01628 /* first, we should create the signals for each subformula */ 01629 CreatedSignals = st_init_table(st_ptrcmp, st_ptrhash); 01630 for (i=0; i<size; i++) { 01631 if (LtlSetGetElt(compositeLabel, i)) 01632 VtxLabelToBlifMv_Aux(fp, A, idx, i, CreatedSignals); 01633 } 01634 st_free_table(CreatedSignals); 01635 01636 /* the label signal is the AND or all the conjuncts */ 01637 fprintf(fp, "\n.table "); 01638 for (i=0; i<size; i++) { 01639 if (LtlSetGetElt(compositeLabel, i)) 01640 fprintf(fp, "n%d_%d_label$AUT ", idx, i); 01641 } 01642 fprintf(fp, " -> n%d_label$AUT\n.default 0\n", idx); 01643 for (i=0; i<size; i++) { 01644 if (LtlSetGetElt(compositeLabel, i)) 01645 fprintf(fp, "1 "); 01646 } 01647 fprintf(fp, "1\n"); 01648 01649 } 01650 01660 static void 01661 VtxLabelToBlifMv_Aux( 01662 FILE *fp, 01663 Ltl_Automaton_t *A, 01664 int node_idx, 01665 int index, 01666 st_table *CreatedSignals) 01667 { 01668 Ctlsp_Formula_t *F = A->tableau->labelTable[index]; 01669 Ctlsp_Formula_t *F_left, *F_right; 01670 int l_index, r_index; 01671 01672 if (st_is_member(CreatedSignals, F)) 01673 return; 01674 else 01675 st_insert(CreatedSignals, F, (char *)0); 01676 01677 switch(Ctlsp_FormulaReadType(F)) { 01678 case Ctlsp_ID_c: 01679 fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 0\n%s 1", 01680 (char *)Ctlsp_FormulaReadVariableName(F), 01681 node_idx, index, 01682 (char *)Ctlsp_FormulaReadValueName(F)); 01683 break; 01684 case Ctlsp_NOT_c: 01685 F_left = Ctlsp_FormulaReadLeftChild(F); 01686 fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 1\n%s 0", 01687 (char *)Ctlsp_FormulaReadVariableName(F_left), 01688 node_idx, index, 01689 (char *)Ctlsp_FormulaReadValueName(F_left)); 01690 break; 01691 case Ctlsp_AND_c: 01692 F_left = Ctlsp_FormulaReadLeftChild(F); 01693 F_right = Ctlsp_FormulaReadRightChild(F); 01694 l_index = Ctlsp_FormulaReadLabelIndex(F_left); 01695 r_index = Ctlsp_FormulaReadLabelIndex(F_right); 01696 VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals); 01697 VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals); 01698 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", 01699 node_idx, l_index, 01700 node_idx, r_index, 01701 node_idx, index); 01702 break; 01703 case Ctlsp_OR_c: 01704 F_left = Ctlsp_FormulaReadLeftChild(F); 01705 F_right = Ctlsp_FormulaReadRightChild(F); 01706 l_index = Ctlsp_FormulaReadLabelIndex(F_left); 01707 r_index = Ctlsp_FormulaReadLabelIndex(F_right); 01708 VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals); 01709 VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals); 01710 fprintf(fp, 01711 "\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", 01712 node_idx, l_index, 01713 node_idx, r_index, 01714 node_idx, index); 01715 break; 01716 default: 01717 fail("unkown formula type"); 01718 } 01719 } 01720 01721 01722
1.7.3