#include "bmc.h"#include "bmcInt.h"
Include dependency graph for bmcAutUtil.c:
Go to the source code of this file.
Functions | |
| static st_table * | AutomatonVertexGetImg (graph_t *G, vertex_t *vtx) |
| static st_table * | AutomatonVertexGetPreImg (graph_t *G, vertex_t *vtx) |
| static int | stIntersect (st_table *tbl1, st_table *tbl2) |
| static int | NoOfBitEncode (int n) |
| static bdd_t * | encodeOfInteger (mdd_manager *manager, array_t *varArray, int val) |
| void | BmcAutEncodeAutomatonStates (Ntk_Network_t *network, Ltl_Automaton_t *automaton) |
| void | BmcAutEncodeAutomatonStates2 (Ntk_Network_t *network, Ltl_Automaton_t *automaton) |
| void | BmcAutEncodeAutomatonStates3 (Ntk_Network_t *network, Ltl_Automaton_t *automaton) |
| void | BmcAutBuildTransitionRelation (Ntk_Network_t *network, Ltl_Automaton_t *automaton) |
| mdd_t * | BmcAutBuildMddForPropositionalFormula (Ntk_Network_t *network, Ltl_Automaton_t *automaton, Ctlsp_Formula_t *formula) |
| int | BmcAutGenerateCnfForBddOffSet (bdd_t *function, int current, int next, BmcCnfClauses_t *cnfClauses, st_table *nsPsTable) |
| BmcCheckForTermination_t * | BmcAutTerminationAlloc (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray) |
| Ltl_Automaton_t * | BmcAutLtlToAutomaton (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula) |
| void | BmcAutTerminationFree (BmcCheckForTermination_t *result) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcAutUtil.c,v 1.18 2005/05/18 18:11:52 jinh Exp $" |
Function Documentation
| static st_table * AutomatonVertexGetImg | ( | graph_t * | G, |
| vertex_t * | vtx | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Return the image of the given vertex in the hash table.]
SideEffects [Result should be freed by the caller.]
Definition at line 798 of file bmcAutUtil.c.
{
lsList Img;
lsGen lsgen;
edge_t *e;
vertex_t *s;
st_table *uTable;
Img = g_get_out_edges(vtx);
uTable = st_init_table(st_ptrcmp, st_ptrhash);
lsForEachItem(Img, lsgen, e) {
s = g_e_dest(e);
st_insert(uTable, (char *) s, (char *) s);
}
return uTable;
}
Here is the caller graph for this function:
| static st_table * AutomatonVertexGetPreImg | ( | graph_t * | G, |
| vertex_t * | vtx | ||
| ) | [static] |
Function********************************************************************
Synopsis [Return the pre-image of the given vertex in the hash table.]
SideEffects [Result should be freed by the caller.]
Definition at line 827 of file bmcAutUtil.c.
{
lsList preImg;
lsGen lsgen;
edge_t *e;
vertex_t *s;
st_table *uTable;
preImg = g_get_in_edges(vtx);
uTable = st_init_table(st_ptrcmp, st_ptrhash);
lsForEachItem(preImg, lsgen, e) {
s = g_e_source(e);
st_insert(uTable, (char *) s, (char *) s);
}
return uTable;
}
Here is the caller graph for this function:
| mdd_t* BmcAutBuildMddForPropositionalFormula | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton, | ||
| Ctlsp_Formula_t * | formula | ||
| ) |
Function********************************************************************
Synopsis [Build MDD for a propositional formula.]
Description [Build MDD for a propositional formula. Returns NIL if the conversion fails. The calling application is responsible for freeing the returned MDD.]
SideEffects []
SeeAlso []
Definition at line 472 of file bmcAutUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(network);
mdd_t *left, *right, *result;
if (formula == NIL(Ctlsp_Formula_t)) {
return NIL(mdd_t);
}
if (formula->type == Ctlsp_TRUE_c){
return bdd_one(manager);
}
if (formula->type == Ctlsp_FALSE_c){
return mdd_zero(manager);
}
if (!Ctlsp_isPropositionalFormula(formula)) {
(void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
fprintf(vis_stdout, "\nFormula: ");
Ctlsp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
return NIL(mdd_t);
}
/*
Atomic proposition.
*/
if (formula->type == Ctlsp_ID_c){
int is_complemented;
bdd_node *funcNode;
result = BmcModelCheckAtomicFormula(Fsm_NetworkReadOrCreateFsm(network), formula);
funcNode = bdd_get_node(result, &is_complemented);
if(is_complemented){
funcNode = bdd_not_bdd_node(funcNode);
}
return result;
}
/*
right can be NIL(mdd_t) for unery operators, but left can't be NIL(mdd_t)
*/
left = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->left);
if (left == NIL(mdd_t)){
return NIL(mdd_t);
}
right = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->right);
/*assert(right != NIL(mdd_t)); */
switch(formula->type) {
case Ctlsp_NOT_c:
result = mdd_not(left);
break;
case Ctlsp_OR_c:
result = mdd_or(left, right, 1, 1);
break;
case Ctlsp_AND_c:
result = mdd_and(left, right, 1, 1);
break;
case Ctlsp_THEN_c:
result = mdd_or(left, right, 0, 1);
break;
case Ctlsp_EQ_c:
result = mdd_xnor(left, right);
break;
case Ctlsp_XOR_c:
result = mdd_xor(left, right);
break;
default:
/*
return NIL(mdd_t) if the type is not supported
*/
fail("Unexpected type");
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcAutBuildTransitionRelation | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton | ||
| ) |
Function********************************************************************
Synopsis [Build BDD of the transition relation of the Automaton.]
Description []
SideEffects []
SeeAlso []
Definition at line 341 of file bmcAutUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(network);
lsGen lsGen;
st_generator *stGen;
vertex_t *vtx, *vtx1;
Ltl_AutomatonNode_t *state, *nextState;
bdd_t *nextStateBdd, *transitionRelation;
bdd_t *initialState, *fairSet, *fairState;
int i;
bdd_t *bddVar;
st_table *nextStates;
var_set_t *psSupport, *nsSupport;
st_table *FairSet = 0;
array_t *fairSetArray;
/*
psNsTable (Bdd Id, bdd_t*)
*/
st_table *psNsTable = st_init_table(st_numcmp, st_numhash);
/*
nsPsTable (BDD Id, BDD Id)
*/
st_table *nsPsTable = st_init_table(st_numcmp, st_numhash);
boolean isComplemented;
int nodeIndex;
/*
Initialization
*/
transitionRelation = bdd_zero(manager);
/*
Build the transition relation
*/
foreach_vertex(automaton->G, lsGen, vtx) {
state = (Ltl_AutomatonNode_t *) vtx->user_data;
/*
support is the set of the bddId of the bdd node in the support of the bdd function.
*/
psSupport = bdd_get_support(state->Encode);
for(i=0; i<psSupport->n_elts; i++) {
if (var_set_get_elt(psSupport, i) == 1) {
/*
i is the bdd Id of the variable in the support of the function.
*/
if (!st_lookup(psNsTable, (char *)(long) i, NULL)){
bddVar = bdd_create_variable(manager);
nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
st_insert(psNsTable, (char *) (long) i, (char *) bddVar);
st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
}
}
}
/*
Get the next states.
*/
nextStates = AutomatonVertexGetImg(automaton->G, vtx);
st_foreach_item(nextStates, stGen, &vtx1, NULL) {
nextState = (Ltl_AutomatonNode_t *) vtx1->user_data;
nextStateBdd = bdd_dup(nextState->Encode);
nsSupport = bdd_get_support(nextStateBdd);
for(i=0; i<nsSupport->n_elts; i++) {
if (var_set_get_elt(nsSupport, i) == 1) {
bdd_t *tmp;
if (!st_lookup(psNsTable, (char *)(long)i, &bddVar)){
bddVar = bdd_create_variable(manager);
nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
st_insert(psNsTable, (char *) (long) i, (char *) bddVar);
st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
}
tmp = nextStateBdd;
nextStateBdd = bdd_compose(nextStateBdd, bdd_get_variable(manager, i), bddVar);
bdd_free(tmp);
}
}
transitionRelation = bdd_or(transitionRelation, bdd_and(state->Encode, nextStateBdd,1 ,1) ,1 ,1);
} /* for each next states*/
} /* for each present state */
fairSetArray = array_alloc(bdd_t*, 0);
fairSet = 0;
if (lsLength(automaton->Fair) != 0) {
fairSet = bdd_zero(manager);
lsForEachItem(automaton->Fair, lsGen, FairSet) {
fairState = bdd_zero(manager);
st_foreach_item(FairSet, stGen, &vtx, NULL) {
state = (Ltl_AutomatonNode_t *) vtx->user_data;
fairState = bdd_or(fairState, state->Encode,1,1);
}
array_insert_last(bdd_t*, fairSetArray, fairState);
fairSet = bdd_or(fairSet, fairState,1,1);
}
}
initialState = bdd_zero(manager);
st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
state = (Ltl_AutomatonNode_t *) vtx->user_data;
initialState = bdd_or(initialState, state->Encode, 1, 1);
}
automaton->transitionRelation = transitionRelation;
automaton->initialStates = initialState;
automaton->fairSets = fairSet;
automaton->psNsTable = psNsTable;
automaton->nsPsTable = nsPsTable;
automaton->fairSetArray = fairSetArray;
} /* BmcAutBuildTransitionRelation() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcAutEncodeAutomatonStates | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Encode the states of the Automaton.]
Description []
SideEffects []
SeeAlso []
Definition at line 77 of file bmcAutUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(network);
lsGen lsGen, lsGen1;
vertex_t *vtx;
Ltl_AutomatonNode_t *node, *node1;
Ctlsp_Formula_t *F;
mdd_t *label;
int i;
/*
Build the mdd of the labels of each automaton node
*/
foreach_vertex(automaton->G, lsGen, vtx) {
node = (Ltl_AutomatonNode_t *) vtx->user_data;
if (node->Labels) {
label = mdd_one(manager);
for (i=0; i<array_n(automaton->labelTable); i++) {
if (LtlSetGetElt(node->Labels, i)) {
F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i);
label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
}
}
node->Encode = label;
}
}
/*
Encode automaton labels
*/
foreach_vertex(automaton->G, lsGen, vtx) {
bdd_t *newVar = NULL;
node = (Ltl_AutomatonNode_t *) vtx->user_data;
foreach_vertex(automaton->G, lsGen1, vtx) {
node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
if(node != node1){
if(newVar == NULL){
newVar = bdd_create_variable(manager);
node->Encode = bdd_and(node->Encode, newVar, 1, 1);
}
node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
}
}
}
} /* BmcAutEncodeAutomatonStates() */
Here is the call graph for this function:
| void BmcAutEncodeAutomatonStates2 | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton | ||
| ) |
Function********************************************************************
Synopsis [Encode the states of the Automaton.]
Description [The labels of each node in the automaton are propositional and are asserted by state variables in the original model. So, we uses these labels as part of the state encoding of the automaton. If two nodes cannot be uniquely specified, then we use new variables]
SideEffects []
SeeAlso []
Definition at line 143 of file bmcAutUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(network);
lsGen lsGen, lsGen1;
vertex_t *vtx;
Ltl_AutomatonNode_t *node, *node1;
Ctlsp_Formula_t *F;
mdd_t *label;
int i;
/*
Build the mdd for the labels of each automaton node.
*/
foreach_vertex(automaton->G, lsGen, vtx) {
node = (Ltl_AutomatonNode_t *) vtx->user_data;
if (node->Labels) {
label = mdd_one(manager);
for (i=0; i<array_n(automaton->labelTable); i++) {
if (LtlSetGetElt(node->Labels, i)) {
F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i);
label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
}
}
node->Encode = label;
}
}
/*
Three cases:
1- node and node1 are both = 1
2- node1 = 1
3- neither node nor nod1 equal to 1
*/
foreach_vertex(automaton->G, lsGen, vtx) {
bdd_t *newVar = NULL;
st_table *preState, *preState1;
node = (Ltl_AutomatonNode_t *) vtx->user_data;
preState = AutomatonVertexGetPreImg(automaton->G, vtx);
foreach_vertex(automaton->G, lsGen1, vtx) {
node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
if(node != node1){
if (!mdd_is_tautology(mdd_and(node->Encode, node1->Encode, 1,1),0)){
preState1 = AutomatonVertexGetPreImg(automaton->G, vtx);
if (stIntersect(preState, preState1)){
if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
node->Encode = bdd_not(node1->Encode);
} else
if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
node1->Encode = bdd_not(node->Encode);
} else {
if(newVar == NULL){
newVar = bdd_create_variable(manager);
}
node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
node->Encode = bdd_and(node->Encode, bdd_not(node1->Encode), 1, 1);
}
} else {
if(newVar == NULL){
newVar = bdd_create_variable(manager);
node->Encode = bdd_and(node->Encode, newVar, 1, 1);
}
node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
}
}
}
}
}
#if 0
/*
Encode the automaton labels
*/
foreach_vertex(automaton->G, lsGen, vtx) {
bdd_t *newVar = NULL;
st_table *nextStates;
Ltl_AutomatonNode_t *nextState;
st_generator *stGen;
node = (Ltl_AutomatonNode_t *) vtx->user_data;
nextStates = AutomatonVertexGetImg(automaton->G, vtx);
st_foreach_item(nextStates, stGen, (char **)&vtx, NIL(char *)) {
nextState = (Ltl_AutomatonNode_t *) vtx->user_data;
if(node != nextState){
if (!mdd_is_tautology(mdd_and(node->Encode, nextState->Encode, 1,1),0)){
printf("n%d intersects n%d\n", node->index, nextState->index);
if(newVar == NULL){
newVar = bdd_create_variable(manager);
/*node->Encode = bdd_and(node->Encode, newVar, 1, 1);*/
}
nextState->Encode = bdd_and(nextState->Encode, bdd_not(newVar), 1, 1);
node->Encode = bdd_and(node->Encode, bdd_not(nextState->Encode), 1, 1);
}
}
}
}
#endif
} /* BmcAutEncodeAutomatonStates2() */
Here is the call graph for this function:
| void BmcAutEncodeAutomatonStates3 | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton | ||
| ) |
Function********************************************************************
Synopsis [Encode the states of the Automaton.]
Description [The labels of each node in the automaton are propositional and are asserted by state variables in the original model. So, we uses these labels as part of the state encoding of the automaton. If two nodes cannot be uniquely specified, then we use new variables]
SideEffects []
SeeAlso []
Definition at line 264 of file bmcAutUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(network);
lsGen lsGen;
st_generator *stGen, *stGen1;
vertex_t *vtx, *vtx1;
Ltl_AutomatonNode_t *node, *node1;
Ctlsp_Formula_t *F;
bdd_t *label;
int i;
int noOfStates=0;
int noOfBits;
array_t *varArray = array_alloc(bdd_t*,0);
/*
Build the bdd for the labels of each automaton node.
*/
foreach_vertex(automaton->G, lsGen, vtx) {
node = (Ltl_AutomatonNode_t *) vtx->user_data;
if (node->Labels) {
noOfStates++;
label = bdd_one(manager);
for (i=0; i<array_n(automaton->labelTable); i++) {
if (LtlSetGetElt(node->Labels, i)) {
F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i);
label = bdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
}
}
node->Encode = label;
}
}
st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
node = (Ltl_AutomatonNode_t *) vtx->user_data;
st_foreach_item(automaton->Init, stGen1, &vtx1, NULL) {
node1 = (Ltl_AutomatonNode_t *) vtx1->user_data;
if(node != node1){
if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
node->Encode = bdd_not(node1->Encode);
} else
if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
node1->Encode = bdd_not(node->Encode);
}
}
}
}
noOfBits = NoOfBitEncode(noOfStates);
for(i=0; i< noOfBits; i++){
array_insert_last(bdd_t*, varArray, bdd_create_variable(manager));
}
i=0;
foreach_vertex(automaton->G, lsGen, vtx) {
node = (Ltl_AutomatonNode_t *) vtx->user_data;
if (node->Labels) {
node->Encode = bdd_and(node->Encode, encodeOfInteger(manager, varArray, i), 1, 1);
i++;
}
}
} /* BmcAutEncodeAutomatonStates3() */
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcAutGenerateCnfForBddOffSet | ( | bdd_t * | function, |
| int | current, | ||
| int | next, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nsPsTable | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF for a given BDD function.]
Description [Generate CNF for a BDD function. This function first negates the BDD function, and then generates the CNF corresponding to the OFF-set of the negated function. If the BDD node is a next state variable, we use the BDD index of the present state variable corresponding to this variable. We could do this by searching the nsPSTable. If trans ==1, this function generates a CNF for a transition from current state to next state, otherwise it generates CNF for NO transition.
The function calling this function must add a unit clause to set the returned value to positive (for function to be true) or negative (for function to be false).
]
SideEffects []
SeeAlso []
Definition at line 574 of file bmcAutUtil.c.
{
bdd_manager *bddManager = bdd_get_manager(function);
bdd_node *node, *funcNode;
int is_complemented;
bdd_gen *gen;
int varIndex;
array_t *tmpClause;
array_t *cube;
int i, value;
int state = current;
bdd_t *bddFunction;
bdd_t *newVar;
int total=0, ndc=0;
float per;
if (function == NULL){
return 0;
}
funcNode = bdd_get_node(function, &is_complemented);
if (bdd_is_constant(funcNode)){
if (is_complemented){
/* add an empty clause to indicate FALSE (un-satisfiable)*/
BmcAddEmptyClause(cnfClauses);
}
/*bdd_free(bddFunction);
bdd_free(newVar);*/
return 0;
}
newVar = bdd_create_variable(bddManager);
bddFunction = bdd_xnor(newVar, function);
bddFunction = bdd_not(bddFunction);
foreach_bdd_cube(bddFunction, gen, cube){
tmpClause = array_alloc(int,0);
arrayForEachItem(int, cube, i, value) {
total++;
if (value != 2){
int j;
ndc++;
/*
If the BDD varaible is a next state varaible, we use the corresponding
current state varaible but with next state index.
*/
if (nsPsTable && st_lookup_int(nsPsTable, (char *)(long)i, &j)){
node = bdd_bdd_ith_var(bddManager, j);
state = next;
} else {
node = bdd_bdd_ith_var(bddManager, i);
state = current;
}
varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), state, cnfClauses);
if (value == 1){
varIndex = -varIndex;
}
array_insert_last(int, tmpClause, varIndex);
}
}
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
}/* foreach_bdd_cube() */
varIndex = BmcGetCnfVarIndexForBddNode(bddManager,
bdd_regular(bdd_get_node(newVar, &is_complemented)),
current, cnfClauses);
per = ((float) ((float)ndc/(float)total))*100;
return (varIndex);
} /* BmcAutGenerateCnfForBddOffSet() */
Here is the call graph for this function:
Here is the caller graph for this function:
| Ltl_Automaton_t* BmcAutLtlToAutomaton | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula | ||
| ) |
Function********************************************************************
Synopsis [Convert LTL to Automaton]
Description [] SideEffects []
SeeAlso []
Definition at line 734 of file bmcAutUtil.c.
{
Ltl_Automaton_t *automaton;
LtlMcOption_t *ltlOptions = LtlMcOptionAlloc();
/*
Build the Buechi Automaton for the negation of the LTL formula.
*/
ltlOptions->algorithm = Ltl2Aut_WRING_c;
ltlOptions->rewriting = TRUE;
ltlOptions->prunefair = TRUE;
ltlOptions->iocompatible = TRUE;
ltlOptions->directsim = TRUE;
ltlOptions->reversesim = TRUE;
ltlOptions->verbosity = McVerbosityNone_c;
ltlOptions->noStrengthReduction = 1;
automaton = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
assert(automaton != NIL(Ltl_Automaton_t));
return automaton;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| BmcCheckForTermination_t* BmcAutTerminationAlloc | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| array_t * | constraintArray | ||
| ) |
Function********************************************************************
Synopsis [Alloc Memory for BmcCheckForTermination_t]
SideEffects []
SeeAlso []
Definition at line 663 of file bmcAutUtil.c.
{
BmcCheckForTermination_t *result = ALLOC(BmcCheckForTermination_t, 1);
Ltl_Automaton_t *automaton;
LtlMcOption_t *ltlOptions = LtlMcOptionAlloc();
if (!result){
return result;
}
/*
Build the Buechi Automaton for the negation of the LTL formula.
*/
ltlOptions->algorithm = Ltl2Aut_WRING_c;
ltlOptions->rewriting = TRUE;
ltlOptions->prunefair = TRUE;
ltlOptions->iocompatible = TRUE;
ltlOptions->directsim = TRUE;
ltlOptions->reversesim = TRUE;
ltlOptions->verbosity = McVerbosityNone_c;
ltlOptions->noStrengthReduction = 1;
automaton = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
assert(automaton != NIL(Ltl_Automaton_t));
/*BmcAutEncodeAutomatonStates(network, automaton); */
/*mcAutEncodeAutomatonStates2(network, automaton);*/
BmcAutEncodeAutomatonStates3(network, automaton);
BmcAutBuildTransitionRelation(network, automaton);
LtlMcOptionFree(ltlOptions);
result->k = 0;
result->m = -1;
result->n = -1;
result->checkLevel = 0;
result->action = 0;
result->automaton = automaton;
result->externalConstraints = NIL(Ctlsp_Formula_t);
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula1, *formula2;
int j;
formula1 = NIL(Ctlsp_Formula_t);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula2) {
formula2 = Ctlsp_FormulaDup(formula2);
if(formula1 == NIL(Ctlsp_Formula_t)) {
formula1 = formula2;
} else {
formula1 = Ctlsp_FormulaCreate(Ctlsp_OR_c, formula1, formula2);
}
}
result->externalConstraints = formula1;
}
result->internalConstraints = automaton->fairSets;
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcAutTerminationFree | ( | BmcCheckForTermination_t * | result | ) |
Function********************************************************************
Synopsis [Free BmcCheckForTermination_t.]
SideEffects []
SeeAlso []
Definition at line 769 of file bmcAutUtil.c.
{
LtlTableau_t *tableau;
Ltl_Automaton_t *automaton = result->automaton;
tableau = automaton->tableau;
Ltl_AutomatonFree((gGeneric) automaton);
LtlTableauFree(tableau);
if(result->externalConstraints != NIL(Ctlsp_Formula_t)){
Ctlsp_FormulaFree(result->externalConstraints);
}
FREE(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * encodeOfInteger | ( | mdd_manager * | manager, |
| array_t * | varArray, | ||
| int | val | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns no. of Bit encoding needed for n]
Description []
SideEffects []
SeeAlso []
Definition at line 911 of file bmcAutUtil.c.
{
int i;
bdd_t *returnValue = mdd_one(manager);
int tmp = val;
bdd_t *var;
for(i=0; i< array_n(varArray); i++){
var = array_fetch(bdd_t*, varArray, i);
if(tmp%2 == 0){
returnValue = bdd_and(returnValue, var, 1, 0);
} else {
returnValue = bdd_and(returnValue, var, 1, 1);
}
tmp = tmp / 2;
}
return returnValue;
}
Here is the caller graph for this function:
| static int NoOfBitEncode | ( | int | n | ) | [static] |
Function********************************************************************
Synopsis [Returns no. of Bit encoding needed for n]
Description []
SideEffects []
SeeAlso []
Definition at line 884 of file bmcAutUtil.c.
{
int i = 0;
int j = 1;
if (n < 2) return 1; /* Takes care of value <= 1 */
while (j < n) {
j = j * 2;
i++;
}
return i;
}
Here is the caller graph for this function:
| static int stIntersect | ( | st_table * | tbl1, |
| st_table * | tbl2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Return 1 if tbl1 and tbl2 two intersects.]
SideEffects []
Definition at line 856 of file bmcAutUtil.c.
{
st_generator *stgen;
vertex_t *vtx;
st_foreach_item(tbl1, stgen, &vtx, NULL) {
if (st_is_member(tbl2,(char *)vtx)) {
st_free_gen(stgen);
return 1;
}
}
return 0;
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcAutUtil.c,v 1.18 2005/05/18 18:11:52 jinh Exp $" [static] |
CFile***********************************************************************
FileName [bmcAutUtil.c]
PackageName [bmc]
Synopsis [Utility file for BMC_Automaton]
Author [Mohammad Awedh]
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 20 of file bmcAutUtil.c.
