#include "ltlInt.h"
Include dependency graph for ltlCompose.c:
Go to the source code of this file.
Functions | |
| static void | AutomatonGetInputNames (Ltl_Automaton_t *A, array_t *InputNames, array_t *Name2LabelIdx) |
| static int | AutomatonCountSelector (Ltl_Automaton_t *A) |
| static int | AutomatonComputeInitState (Ltl_Automaton_t *A) |
| static lsList | GetCubes_Aux (Ltl_Automaton_t *A, int index) |
| static char * | StringNormalize (char *inputString) |
| static void | AutomatonVtxLabelToBlifMv (FILE *fp, Ltl_Automaton_t *A, vertex_t *vtx) |
| static void | VtxLabelToBlifMv_Aux (FILE *fp, Ltl_Automaton_t *A, int node_idx, int index, st_table *CreatedSignals) |
| void | Ltl_AutomatonToDot (FILE *fp, Ltl_Automaton_t *aut, int level) |
| int | Ltl_AutomatonToBlifMv (FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A) |
| int | Ltl_AutomatonToVerilog (FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A) |
| int | Ltl_AutomatonToSmv (FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ltlCompose.c,v 1.30 2005/04/28 08:51:19 bli Exp $" |
Function Documentation
| static int AutomatonComputeInitState | ( | Ltl_Automaton_t * | A | ) | [static] |
Function********************************************************************
Synopsis [Determine if "Init" state is necessary.]
Description [If there exists such a state 'ns', "Init" is not necessary: (1) ns is in Aut->Init (2) there is a edge from ns to every state in Aut->Init (including itself) In another word, ns is equivalent to "Init". (3) there is no edge fron ns to states not in Aut->Init.
Return the index of the state 'ns' if exist, otherwise return -1. ]
SideEffects []
Definition at line 1286 of file ltlCompose.c.
{
int initIdx = -1;
vertex_t *vtx, *vtx2, *s;
edge_t *e;
st_generator *stgen, *stgen2;
lsGen lsgen;
st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
int isInit = 1;
/* first, compute the set of sucessors of 'vtx' */
lsList Img = g_get_out_edges(vtx);
st_table *uTable = st_init_table(st_ptrcmp, st_ptrhash);
lsForEachItem(Img, lsgen, e) {
s = g_e_dest(e);
st_insert(uTable, s, s);
}
/* then, test if it is equivalent to 'A->Init': No more, No less */
st_foreach_item(A->Init, stgen2, &vtx2, NIL(char *)) {
if (!st_is_member(uTable, vtx2)) {
isInit = 0;
st_free_gen(stgen2);
break;
}
}
if (isInit) {
st_foreach_item(uTable, stgen2, &vtx2, NIL(char *)) {
if (!st_is_member(A->Init, vtx2)) {
isInit = 0;
st_free_gen(stgen2);
break;
}
}
}
st_free_table(uTable);
if (isInit == 1) {
initIdx = ((Ltl_AutomatonNode_t *)vtx->user_data)->index;
st_free_gen(stgen);
break;
}
}
return initIdx;
}
Here is the caller graph for this function:
| static int AutomatonCountSelector | ( | Ltl_Automaton_t * | A | ) | [static] |
Function********************************************************************
Synopsis [Return the upper bound number of nondeterministic selectors.]
Description [The automaton is nondeterministic, but the blif_mv file should be deterministic. Selector (variable with random output) is used to make the .table determinstic. We need to know how many outputs the Selector should have. Here we take the maximum out-degree among all nodes as the upper bound estimation.]
SideEffects []
Definition at line 1252 of file ltlCompose.c.
{
int sel_num = st_count(A->Init);
int local_num;
lsGen lsgen;
vertex_t *vtx;
foreach_vertex(A->G, lsgen, vtx) {
local_num = lsLength(g_get_out_edges(vtx));
if (sel_num < local_num)
sel_num = local_num;
}
return sel_num;
}
Here is the caller graph for this function:
| static void AutomatonGetInputNames | ( | Ltl_Automaton_t * | A, |
| array_t * | InputNames, | ||
| array_t * | Name2LabelIdx | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Return a array of all the inputnames of the automaton.]
Description [InputNames and Name2LabelIdx are two "array_t" provided by the caller. InputNames will be filled by all the labels on the automaton nodes; Each item of Name2LabelIdx is a "st_table" from a label to all the related formulae in A->labelTable that contains the label.]
SideEffects []
Definition at line 1199 of file ltlCompose.c.
{
st_table *Visited = st_init_table(strcmp, st_strhash);
Ctlsp_Formula_t *F;
Ctlsp_FormulaType F_type;
long i, index, counter;
counter = 0;
for (i=0; i<array_n(A->labelTable); i++) {
/* get the positive formula string */
F = array_fetch(Ctlsp_Formula_t *, A->labelTable, i);
F_type = Ctlsp_FormulaReadType(F);
/* if it's not an AP (just a propositional formula), skip ... */
if (F_type != Ctlsp_NOT_c && F_type != Ctlsp_ID_c)
continue;
if (F_type == Ctlsp_NOT_c)
F = Ctlsp_FormulaReadLeftChild(F);
/* put into the InputNames array */
if (!st_lookup(Visited, Ctlsp_FormulaReadVariableName(F),&index)){
st_table *tmptbl = st_init_table(st_numcmp, st_numhash);
st_insert(tmptbl, (char *) i, (char *)i);
array_insert(st_table *, Name2LabelIdx, counter, tmptbl);
array_insert(char *, InputNames, counter,
Ctlsp_FormulaReadVariableName(F));
st_insert(Visited, Ctlsp_FormulaReadVariableName(F), (char *)counter++);
}else {
st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, index);
st_insert(tmptbl, (char *)i, (char *)i);
}
}
st_free_table(Visited);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void AutomatonVtxLabelToBlifMv | ( | FILE * | fp, |
| Ltl_Automaton_t * | A, | ||
| vertex_t * | vtx | ||
| ) | [static] |
Function********************************************************************
Synopsis [Create the "label" signal in blif_mv format and print out.]
Description [Assume that the label is a propositional formula with *, +, !.
For Ctlsp_ID_c/Ctlsp_NOT_c: .table in1 n1_##_label$AUT !(RED) 1 For Ctlsp_AND_c: .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT 1 1 1 For Ctlsp_OR_c: .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT 1 - 1
- 1 1 ]
SideEffects []
Definition at line 1611 of file ltlCompose.c.
{
/* each 'compLabel' is a "propositional formulae" */
LtlSet_t *compositeLabel = LtlAutomatonVertexGetLabels(vtx);
int idx = Ltl_AutomatonVtxGetNodeIdx(vtx);
int size = A->tableau->labelIndex;
int i;
st_table *CreatedSignals;
if (LtlSetIsEmpty(compositeLabel)) {
fprintf(fp, "\n.table n%d_label$AUT\n1\n", idx);
return;
}
/* first, we should create the signals for each subformula */
CreatedSignals = st_init_table(st_ptrcmp, st_ptrhash);
for (i=0; i<size; i++) {
if (LtlSetGetElt(compositeLabel, i))
VtxLabelToBlifMv_Aux(fp, A, idx, i, CreatedSignals);
}
st_free_table(CreatedSignals);
/* the label signal is the AND or all the conjuncts */
fprintf(fp, "\n.table ");
for (i=0; i<size; i++) {
if (LtlSetGetElt(compositeLabel, i))
fprintf(fp, "n%d_%d_label$AUT ", idx, i);
}
fprintf(fp, " -> n%d_label$AUT\n.default 0\n", idx);
for (i=0; i<size; i++) {
if (LtlSetGetElt(compositeLabel, i))
fprintf(fp, "1 ");
}
fprintf(fp, "1\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static lsList GetCubes_Aux | ( | Ltl_Automaton_t * | A, |
| int | index | ||
| ) | [static] |
Function********************************************************************
Synopsis [Given a composite label, return a list of label (each of which is a cube.]
Description [The composite label can any combination of !, + , *.]
SideEffects []Function********************************************************************
Synopsis [Given a index in A->tableau->labelTable, return a list of label (each of which is a cube.]
Description [The formula A->tableau->labelTable[index] can be any combination of !, + , *.]
SideEffects []
Definition at line 1479 of file ltlCompose.c.
{
Ctlsp_Formula_t *F = A->tableau->labelTable[index];
int size = A->tableau->labelIndex;
lsList leftList;
lsList rightList;
lsList thisList =(lsList)0;
lsGen lsgen, lsgen2;
LtlSet_t *tempSet, *tempSet2, *tempSet3;
if (Ctlsp_LtlFormulaIsAtomicPropositional(F)) {
thisList = lsCreate();
tempSet = LtlSetNew(size);
LtlSetSetElt(tempSet, Ctlsp_FormulaReadLabelIndex(F));
lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
}else {
Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
switch(Ctlsp_FormulaReadType(F)) {
case Ctlsp_OR_c:
leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
/* merge two list together */
thisList = leftList;
lsForEachItem(rightList, lsgen, tempSet) {
lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
}
lsDestroy(rightList, (void (*)(lsGeneric))0);
break;
case Ctlsp_AND_c:
leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
/* generate the cartesian product of the two lists */
thisList = lsCreate();
lsForEachItem(leftList, lsgen, tempSet) {
lsForEachItem(rightList, lsgen2, tempSet2) {
tempSet3 = LtlSetNew(size);
LtlSetOR(tempSet3, tempSet, tempSet2);
lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0);
}
}
lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree);
lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree);
break;
default:
assert(0);
break;
}
}
return thisList;
}
Here is the call graph for this function:
| int Ltl_AutomatonToBlifMv | ( | FILE * | fp, |
| Ntk_Network_t * | network, | ||
| Ltl_Automaton_t * | A | ||
| ) |
Function********************************************************************
Synopsis [Translate the automaton to a BlifMv file.]
Description [The Hrc_Manager may or may not be provided. If not, the blifmv file generated is not complete (all the inputs are assummed to be boolean).
Notice that the labels on each state are propositional subformulae, not necessarily atomic propositions.]
SideEffects []
SeeAlso []
Definition at line 175 of file ltlCompose.c.
{
Var_Variable_t *inputVar;
array_t *InputNames = array_alloc(char *, 0);
array_t *Name2LabelIdx = array_alloc(st_table *, 0);
Ntk_Node_t *ntknode;
char *inputName;
st_generator *stgen;
lsGen lsgen, lsgen2;
int i, j, is_enum, range;
int sel_num, sel_cnt;
edge_t *edge;
vertex_t *vtx, *vtx2;
st_table *FairSet, *tmptbl;
int InitIdx = AutomatonComputeInitState(A);
char InitStr[10];
int result = 1;
array_t *labelArray;
/* The initState of the automaton */
if (InitIdx == -1)
sprintf(InitStr, "Init");
else
sprintf(InitStr, "n%d", InitIdx);
if (network == NIL(Ntk_Network_t)) {
result = 0;
fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n");
}
/* Retrieve all the input names on the labels; For each input, create a
* hash table and add all the label subformulae contains that input;
* Finally, calculate the size of the "selector"
*/
AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
sel_num = AutomatonCountSelector(A);
fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name);
/*-------------------------------------------------------
* .model Buechi$AUT
* .root Buechi$AUT
*-------------------------------------------------------
*/
fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT");
/*-------------------------------------------------------
* .inputs in1 in2 in3 ... inN
*-------------------------------------------------------
*/
fprintf(fp, "\n.inputs ");
for (i=0; i<array_n(InputNames); i++) {
inputName = array_fetch(char *, InputNames, i);
fprintf(fp, "%s ", inputName);
}
/*-------------------------------------------------------
* .outputs fair1 fair2 fair3... fairN
*-------------------------------------------------------
*/
fprintf(fp, "\n.outputs ");
if ( lsLength(A->Fair) != 0) {
for (i=0; i<lsLength(A->Fair); i++) {
fprintf(fp, "fair%d$AUT ", i+1);
}
}else
fprintf(fp, "fair1$AUT");
/*-------------------------------------------------------
* .mv in1 3 RED GREEN YELLOW
*-------------------------------------------------------
*/
if (network != NIL(Ntk_Network_t)) {
for (i=0; i<array_n(InputNames); i++) {
inputName = array_fetch(char *, InputNames, i);
ntknode = Ntk_NetworkFindNodeByName(network, inputName);
assert(ntknode != NIL(Ntk_Node_t));
inputVar = Ntk_NodeReadVariable(ntknode);
is_enum = Var_VariableTestIsEnumerative(inputVar);
range = Var_VariableReadNumValues(inputVar);
if (is_enum) {
if (range != 2)
fprintf(fp, "\n.mv %s %d\n", inputName, range);
}else {
fprintf(fp, "\n.mv %s %d ", inputName, range);
for (j=0; j<range; j++) {
fprintf(fp, "%s ",
Var_VariableReadSymbolicValueFromIndex(inputVar,j));
}
}
}
}
/*-------------------------------------------------------
* .mv stateD$AUT N Init n1 n2 n3 ... nN
* .mv state$AUT N Init n1 n2 n3 ... nN
*-------------------------------------------------------
*/
if (InitIdx == -1)
fprintf(fp, "\n.mv stateD$AUT %d Init Trap ",
lsLength(g_get_vertices(A->G)) + 2);
else
fprintf(fp, "\n.mv stateD$AUT %d Trap ",
lsLength(g_get_vertices(A->G)) + 1);
foreach_vertex(A->G, lsgen, vtx) {
fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
if (InitIdx == -1)
fprintf(fp, "\n.mv state$AUT %d Init Trap ",
lsLength(g_get_vertices(A->G)) + 2);
else
fprintf(fp, "\n.mv state$AUT %d Trap ",
lsLength(g_get_vertices(A->G)) + 1);
foreach_vertex(A->G, lsgen, vtx) {
fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
/*-------------------------------------------------------
* .mv selector n
* .table selector
* -
*-------------------------------------------------------
*/
if (sel_num > 1)
fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num);
/*-------------------------------------------------------
* for each state label, create a signal n1_##_label$AUT (recursively)
*-------------------------------------------------------
*/
labelArray = array_alloc(vertex_t *, 0);
foreach_vertex(A->G, lsgen, vtx) {
AutomatonVtxLabelToBlifMv(fp, A, vtx);
array_insert_last(vertex_t *, labelArray, vtx);
}
/*-------------------------------------------------------
* .latch stateD$AUT state$AUT
* .reset state$AUT
* Init (or ns)
*-------------------------------------------------------
*/
fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s",
InitStr);
/*------------------------------------------------------
* .table selector$AUT state$AUT n1_label$AUT n2_label... -> stateD$AUT
* .default Trap
* 0 1 0 0 ... n1
* 1 0 1 n2
* ...
*------------------------------------------------------
*/
if (sel_num >1)
fprintf(fp, "\n.table selector$AUT state$AUT ");
else
fprintf(fp, "\n.table state$AUT ");
arrayForEachItem(vertex_t *, labelArray, i, vtx) {
fprintf(fp, "n%d_label$AUT ", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
fprintf(fp, " -> stateD$AUT\n.default Trap");
if (InitIdx == -1) {
sel_cnt = 0;
arrayForEachItem(vertex_t *, labelArray, i, vtx) {
if (!st_is_member(A->Init, vtx))
continue;
if (sel_num > 1) {
if (st_count(A->Init) == 1)
fprintf(fp, "\n- Init ");
else
fprintf(fp, "\n%d Init ", sel_cnt);
}else
fprintf(fp, "\nInit ");
for(j=0; j<array_n(labelArray); j++)
fprintf(fp, "%s ", ((i==j)?"1":"-"));
fprintf(fp, " n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
if (sel_num > 1)
sel_cnt++;
}
}
/* for each edge (n1, n2) with n2 labeled n2_label$AUT, add entry:
*-------------------------------------------------------
* selector 1 0 0 ... n1
* selector 0 1 0 ... n2
* ...
*-------------------------------------------------------
*/
foreach_vertex(A->G, lsgen, vtx) {
int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
int outDegree = lsLength(g_get_out_edges(vtx));
sel_cnt = 0;
foreach_out_edge(vtx, lsgen2, edge) {
int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
if (sel_num > 1) {
if (outDegree == 1)
fprintf(fp, "\n- n%d ", n1);
else
fprintf(fp, "\n%d n%d ", sel_cnt, n1);
}else {
fprintf(fp, "\nn%d ", n1);
}
arrayForEachItem(vertex_t *, labelArray, i, vtx2) {
fprintf(fp, "%s ", ((vtx2 == g_e_dest(edge))?"1":"-"));
}
fprintf(fp, " n%d", n2);
if (sel_num > 1)
sel_cnt++;
}
}
array_free(labelArray);
/*-------------------------------------------------------
* .table state -> fair1
* .default 0
* ------------------------------------------------------
*/
if (lsLength(A->Fair) != 0) {
i = 1;
lsForEachItem(A->Fair, lsgen, FairSet) {
int isFirst = 1;
fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++);
fprintf(fp, "\n.default 0\n(");
st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
if (isFirst)
isFirst = 0;
else
fprintf(fp, ",");
fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
fprintf(fp, ") 1");
}
}else {
fprintf(fp, "\n.table state$AUT -> fair1$AUT ");
if (InitIdx == -1)
fprintf(fp, "\n.default 0\n!(Trap,Init) 1");
else
fprintf(fp, "\n.default 0\n!(Trap) 1");
}
/*-------------------------------------------------------
* .end
* ------------------------------------------------------
*/
fprintf(fp, "\n.end\n");
/* free the name array
*/
array_free(InputNames);
arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
st_free_table(tmptbl);
}
array_free(Name2LabelIdx);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Ltl_AutomatonToDot | ( | FILE * | fp, |
| Ltl_Automaton_t * | aut, | ||
| int | level | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Translate the Automaton into Dot format.]
Description []
SideEffects []
SeeAlso []
Definition at line 74 of file ltlCompose.c.
{
edge_t *edge;
vertex_t *vtx1, *vtx2;
Ltl_AutomatonNode_t *node, *node2;
lsGen lsgen, lsgen2;
st_table *FairSet;
st_generator *stgen;
Ctlsp_Formula_t *F;
char *tmpString;
int fairindex, first, i, n;
/*-------------------------------------------------
* digraph "G(F(p=1))" {
* node [shape=ellipse];
* size = "7.5,10"
* center = true;
* "title" [label="G(F(p=1))", shape=plaintext];
*-------------------------------------------------
*/
if (aut->name)
tmpString = aut->name;
else
tmpString = "";
fprintf(fp, "\ndigraph \"%s\" {\nnode [shape=ellipse];\nsize = \"7.5,10\"\ncenter = true;\n\"title\" [label=\"%s\",shape=plaintext];", tmpString, tmpString);
/*-------------------------------------------------
* "n1" [label="n1\n{p=1}\n(1)"];
*-------------------------------------------------
*/
foreach_vertex( aut->G, lsgen, vtx1) {
node = (Ltl_AutomatonNode_t *)vtx1->user_data;
fprintf(fp,"\n\"n%d\" [label=\"n%d\\n{", node->index, node->index);
if (node->Labels) {
first = 1; n = array_n(aut->labelTable);
for (i=0; i<n; i++) {
if (LtlSetGetElt(node->Labels, i)) {
if (!first) fprintf(fp, ",");
else first = 0;
F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i);
Ctlsp_FormulaPrint(fp, F);
}
}
}
fprintf(fp, "}\\n(");
fairindex = 1;
lsForEachItem(aut->Fair, lsgen2, FairSet) {
if (st_is_member(FairSet, vtx1))
fprintf(fp, " %d ", fairindex);
fairindex++;
}
fprintf(fp, ")\"];");
}
/*-------------------------------------------------
* "init-n2" [style=invis]
* "init-n2" -> "n2";
*-------------------------------------------------
*/
st_foreach_item(aut->Init, stgen, &vtx1, NIL(char *)) {
node = (Ltl_AutomatonNode_t *) vtx1->user_data;
fprintf(fp, "\n\"init-n%d\" [style=invis]", node->index);
fprintf(fp, "\n\"init-n%d\" -> \"n%d\";", node->index, node->index);
}
/*-------------------------------------------------
* "n1" -> "n1";
*-------------------------------------------------
*/
foreach_edge(aut->G, lsgen, edge) {
vtx1 = g_e_source(edge);
vtx2 = g_e_dest(edge);
node = (Ltl_AutomatonNode_t *) vtx1->user_data;
node2 = (Ltl_AutomatonNode_t *) vtx2->user_data;
fprintf(fp, "\n\"n%d\" -> \"n%d\";", node->index, node2->index);
}
fprintf(fp, "\n}\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Ltl_AutomatonToSmv | ( | FILE * | fp, |
| Ntk_Network_t * | network, | ||
| Ltl_Automaton_t * | A | ||
| ) |
Function********************************************************************
Synopsis [Translate the automaton to SMV file.]
Description [The Hrc_Manager may or may not be provided. If not, the blifmv file generated is not complete (inputs are assummed to be boolean.]
SideEffects []
SeeAlso []
Definition at line 1173 of file ltlCompose.c.
{
return 1;
}
| int Ltl_AutomatonToVerilog | ( | FILE * | fp, |
| Ntk_Network_t * | network, | ||
| Ltl_Automaton_t * | A | ||
| ) |
Function********************************************************************
Synopsis [Translate the automaton to Verilog file.]
Description [The Hrc_Manager may or may not be provided. If not, the verilog file generated is not accurate (all the inputs are assummed to be boolean).]
SideEffects []
SeeAlso []
Definition at line 808 of file ltlCompose.c.
{
Var_Variable_t *inputVar;
array_t *InputNames = array_alloc(char *, 0);
array_t *Name2LabelIdx = array_alloc(st_table *, 0);
Ntk_Node_t *ntknode;
char *inputName, *formulaString, *normalString;
st_generator *stgen;
lsGen lsgen, lsgen2;
int i, j, is_enum, range, isFirst;
int sel_num, sel_cnt;
edge_t *edge;
vertex_t *vtx;
st_table *FairSet;
int InitIdx = AutomatonComputeInitState(A);
char InitStr[10];
int result = 1;
/* The initState of the automaton */
if (InitIdx == -1)
sprintf(InitStr, "Init");
else
sprintf(InitStr, "n%d", InitIdx);
if (network == NIL(Ntk_Network_t)) {
result = 0;
fprintf(vis_stderr, "Warning: the Verilog output is incomplete. (The current node is empty. Read in design.)\n");
}
/* Retrieve all the input names of the automaton into 'InputNames', And for
* each name, put into a hash table all the subformulae contains it
*/
AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
sel_num = AutomatonCountSelector(A);
fprintf(fp, "\n// Buechi automaton: %s", A->name);
/*-------------------------------------------------------
* typedef enum {Init, trap, n1, n2, ... nN} states;
* typedef enum {READ, GREEN, YELLOW} type_in1;
*-------------------------------------------------------
*/
if (InitIdx == -1)
fprintf(fp, "\ntypedef enum {Init,Trap");
else
fprintf(fp, "\ntypedef enum {Trap");
foreach_vertex(A->G, lsgen, vtx) {
fprintf(fp, ",n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
fprintf(fp, "} type_states;");
if (network != NIL(Ntk_Network_t)) {
arrayForEachItem(char *, InputNames, i, inputName) {
/* replace illegal characters in the input name string */
normalString = StringNormalize(inputName);
fprintf(fp, "\n//Input name mapping:\t %s => %s;", inputName,
normalString);
ntknode = Ntk_NetworkFindNodeByName(network, inputName);
assert(ntknode != NIL(Ntk_Node_t));
inputVar = Ntk_NodeReadVariable(ntknode);
is_enum = Var_VariableTestIsEnumerative(inputVar);
range = Var_VariableReadNumValues(inputVar);
if (is_enum) {
if (range>2)
fprintf(fp, "\ntypedef enum {0-%d} type_%s;",
range-1, normalString);
}else {
fprintf(fp, "\ntypedef enum {");
isFirst = 1;
for (j=0; j<range; j++) {
char *vstr =
Var_VariableReadSymbolicValueFromIndex(inputVar,j);
if (isFirst) {
fprintf(fp, "%s ", vstr);
isFirst = 0;
} else
fprintf(fp, ",%s ", vstr);
}
fprintf(fp, "} type_%s;", normalString);
}
FREE(normalString);
}
}
/*-------------------------------------------------------
* module Buechi (clock, in1, in2 ... inN, fair1, ...);
*-------------------------------------------------------
*/
fprintf(fp, "\n//Buechi Buechi (clock");
for (i=0; i<array_n(InputNames); i++) {
inputName = array_fetch(char *, InputNames, i);
fprintf(fp, ",%s", inputName);
}
for (i=0; i<lsLength(A->Fair); i++) {
fprintf(fp, ",fair%d", i+1);
}
fprintf(fp, ");");
fprintf(fp, "\nmodule Buechi (clock");
for (i=0; i<array_n(InputNames); i++) {
inputName = array_fetch(char *, InputNames, i);
normalString = StringNormalize(inputName);
fprintf(fp, ",%s", normalString);
FREE(normalString);
}
for (i=0; i<lsLength(A->Fair); i++) {
fprintf(fp, ",fair%d", i+1);
}
fprintf(fp, ");");
/*-------------------------------------------------------
* input clock, in1, in2 ... inN ;
* output fair1, fair2 ... fairN ;
*-------------------------------------------------------
*/
fprintf(fp, "\n\tinput clock");
for (i=0; i<array_n(InputNames); i++) {
inputName = array_fetch(char *, InputNames, i);
normalString = StringNormalize(inputName);
fprintf(fp, ", %s", normalString);
FREE(normalString);
}
if (lsLength(A->Fair)>0) {
fprintf(fp, ";\n\toutput ");
isFirst = 1;
for (i=0; i<lsLength(A->Fair); i++) {
if (isFirst) {
fprintf(fp, "fair%d", i+1);
isFirst = 0;
} else {
fprintf(fp, ",fair%d", i+1);
}
}
}
fprintf(fp, ";");
/*-------------------------------------------------------
* type_in1 wire in1;
* type_in2 wire in2;
* ...
* type_states reg state;
* wire[0:logN] sel;
*-------------------------------------------------------
*/
if (network != NIL(Ntk_Network_t)) {
arrayForEachItem(char *, InputNames, i, inputName) {
normalString = StringNormalize(inputName);
ntknode = Ntk_NetworkFindNodeByName(network, inputName);
assert(ntknode != NIL(Ntk_Node_t));
inputVar = Ntk_NodeReadVariable(ntknode);
is_enum = Var_VariableTestIsEnumerative(inputVar);
range = Var_VariableReadNumValues(inputVar);
if (!is_enum || range > 2)
fprintf(fp, "\n\ttype_%s wire %s;", normalString,normalString);
FREE(normalString);
}
}
fprintf(fp, "\n\ttype_states reg state;");
if (sel_num >1) {
if (sel_num == 2)
fprintf(fp, "\n\twire sel;");
else
fprintf(fp, "\n\twire [0:%d] sel;", (int)(ceil(log(sel_num)))-1);
}
/*-------------------------------------------------------
* assign sel = $ND( {0-N} );
* assign fair = (state==n1 || state==n2 || ... );
*-------------------------------------------------------
*/
fprintf(fp, "\n\tassign sel = $ND( {0-%d} );", sel_num-1 );
i = 1;
lsForEachItem(A->Fair, lsgen, FairSet) {
int isFirst = 1;
fprintf(fp, "\n\tassign fair%d = (state==", i++);
st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
if (isFirst)
isFirst = 0;
else
fprintf(fp, "|| state==");
fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
}
fprintf(fp, ");");
}
/*-------------------------------------------------------
* initial state = Init;
*-------------------------------------------------------
*/
fprintf(fp, "\n\tinitial state = %s;", InitStr);
/*-------------------------------------------------------
* always @ (posedge clock) begin
* case (state)
*-------------------------------------------------------
*/
fprintf(fp, "\n\talways @ (posedge clock) begin");
fprintf(fp, "\n\t\tcase (state)");
/* for each initial state n2 with label "in1=p !in3=q...", add entry:
*-------------------------------------------------------
* Init:
* if( sel==0 && in1==p && !in3=q ... )
* state = n2;
* else if( sel==1 && ...)
* state = n3;
* else
* state = Trap;
*------------------------------------------------------
*/
if (InitIdx == -1) {
fprintf(fp, "\n\t\tInit:");
sel_cnt = 0;
st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx);
LtlSet_t *label = LtlAutomatonVertexGetLabels(vtx);
/* universal label (no label) on n2 */
if (LtlSetIsEmpty(label)) {
if (st_count(A->Init) == 1 || sel_num == 0)
fprintf(fp,"\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
else if (sel_cnt == 0)
fprintf(fp,"\n\t\t\tif(sel==%d)\n\t\t\t\tstate = n%d;",
sel_cnt++, n2);
else
fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
sel_cnt++, n2);
}else {
/* there is at least one label on n2 */
if (st_count(A->Init) == 1 || sel_num == 0)
fprintf(fp, "\n\t\t\tif(");
else if (sel_cnt==0)
fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
else
fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
isFirst = 1;
for (i=0; i<array_n(A->labelTable); i++) {
if (LtlSetGetElt(label, i)) {
Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
A->labelTable, i);
formulaString = Ctlsp_FormulaConvertToString(F);
normalString = StringNormalize(formulaString);
FREE(formulaString);
if (isFirst)
isFirst = 0;
else
fprintf(fp, " && ");
fprintf(fp, "%s", normalString);
FREE(normalString);
}
}
fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
}
}
fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
}
/* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry:
*-------------------------------------------------------
* n1:
* if( sel==0 && in1==p && !in3=q ... )
* state = n2;
* else if( sel==1 && ...)
* state = n3;
* else
* state = Trap;
*-------------------------------------------------------
*/
foreach_vertex(A->G, lsgen, vtx) {
int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
int outDegree = lsLength(g_get_out_edges(vtx));
fprintf(fp, "\n\t\tn%d:", n1);
sel_cnt = 0;
foreach_out_edge(vtx, lsgen2, edge) {
int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
LtlSet_t *label = LtlAutomatonVertexGetLabels(g_e_dest(edge));
/* universal label (no label) on n2 */
if (LtlSetIsEmpty(label)) {
if (outDegree == 1 || sel_num == 0)
fprintf(fp, "\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
else if (sel_cnt == 0)
fprintf(fp, "\n\t\t\tif(sel==%d) \n\t\t\t\tstate = n%d;",
sel_cnt++, n2);
else
fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
sel_cnt++, n2);
}else {
/* at least 1 label on n2 */
if (outDegree == 1 || sel_num == 0)
fprintf(fp, "\n\t\t\tif(");
else if (sel_cnt==0)
fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
else
fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
isFirst = 1;
for (i=0; i<array_n(A->labelTableNegate); i++) {
if (LtlSetGetElt(label, i)) {
Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
A->labelTable, i);
formulaString = Ctlsp_FormulaConvertToString(F);
normalString = StringNormalize(formulaString);
FREE(formulaString);
if (isFirst) isFirst = 0;
else fprintf(fp, " && ");
fprintf(fp, "%s", normalString);
FREE(normalString);
}
}
fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
}
}
fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
}
/*-------------------------------------------------------
* default: state = Trap;
* endcase
* end
* endmodule
*-------------------------------------------------------
*/
fprintf(fp, "\n\t\tdefault: state = Trap;\n\t\tendcase\n\tend\nendmodule\n");
/* free the name array */
array_free(InputNames);
for(i=0; i<array_n(Name2LabelIdx); i++) {
st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, i);
st_free_table(tmptbl);
}
array_free(Name2LabelIdx);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static char * StringNormalize | ( | char * | inputString | ) | [static] |
Function********************************************************************
Synopsis [Given a string, do the following replacement.]
Description [ = => == + => || => && . => _ < => _ > => _ ]
SideEffects [The caller should free the result]
Definition at line 1552 of file ltlCompose.c.
{
char *normalString = ALLOC(char, strlen(inputString)*2);
char *from = inputString;
char *to = normalString;
while( *from ) {
switch(*from) {
case '=':
*(to++) = '=';
*(to) = '=';
break;
case '+':
*(to++) = '|';
*(to) = '|';
break;
case '*':
*(to++) = '&';
*(to) = '&';
break;
case '.':
case '<':
case '>':
*(to) = '_';
break;
default:
*(to) = *from;
}
from++;
to++;
}
*to = '\0';
return normalString;
}
Here is the caller graph for this function:
| static void VtxLabelToBlifMv_Aux | ( | FILE * | fp, |
| Ltl_Automaton_t * | A, | ||
| int | node_idx, | ||
| int | index, | ||
| st_table * | CreatedSignals | ||
| ) | [static] |
Function********************************************************************
Synopsis [Create the "label" signal in blif_mv format and print out.]
Description [Assume that "i" is the index in the label table]
SideEffects []
Definition at line 1661 of file ltlCompose.c.
{
Ctlsp_Formula_t *F = A->tableau->labelTable[index];
Ctlsp_Formula_t *F_left, *F_right;
int l_index, r_index;
if (st_is_member(CreatedSignals, F))
return;
else
st_insert(CreatedSignals, F, (char *)0);
switch(Ctlsp_FormulaReadType(F)) {
case Ctlsp_ID_c:
fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 0\n%s 1",
(char *)Ctlsp_FormulaReadVariableName(F),
node_idx, index,
(char *)Ctlsp_FormulaReadValueName(F));
break;
case Ctlsp_NOT_c:
F_left = Ctlsp_FormulaReadLeftChild(F);
fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 1\n%s 0",
(char *)Ctlsp_FormulaReadVariableName(F_left),
node_idx, index,
(char *)Ctlsp_FormulaReadValueName(F_left));
break;
case Ctlsp_AND_c:
F_left = Ctlsp_FormulaReadLeftChild(F);
F_right = Ctlsp_FormulaReadRightChild(F);
l_index = Ctlsp_FormulaReadLabelIndex(F_left);
r_index = Ctlsp_FormulaReadLabelIndex(F_right);
VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
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",
node_idx, l_index,
node_idx, r_index,
node_idx, index);
break;
case Ctlsp_OR_c:
F_left = Ctlsp_FormulaReadLeftChild(F);
F_right = Ctlsp_FormulaReadRightChild(F);
l_index = Ctlsp_FormulaReadLabelIndex(F_left);
r_index = Ctlsp_FormulaReadLabelIndex(F_right);
VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
fprintf(fp,
"\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",
node_idx, l_index,
node_idx, r_index,
node_idx, index);
break;
default:
fail("unkown formula type");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ltlCompose.c,v 1.30 2005/04/28 08:51:19 bli Exp $" [static] |
CFile***********************************************************************
FileName [ltlCompose.c]
PackageName [ltl]
Synopsis [Write the Buechi automaton into a file.]
Author [Chao Wang<chao.wang@colorado.EDU>]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 19 of file ltlCompose.c.
