#include "ltlInt.h"
Include dependency graph for ltlSet.c:
Go to the source code of this file.
Functions | |
| LtlSet_t * | LtlSetNew (int size) |
| void | LtlSetFree (LtlSet_t *set) |
| LtlSet_t * | LtlSetCopy (LtlSet_t *from) |
| void | LtlSetAssign (LtlSet_t *to, LtlSet_t *from) |
| int | LtlSetEqual (LtlSet_t *s1, LtlSet_t *s2) |
| int | LtlSetCardinality (LtlSet_t *set) |
| int | LtlSetCompareCardinality (const void *p1, const void *p2) |
| int | LtlSetIsContradictory (LtlSet_t *set, array_t *Negate) |
| int | LtlSetInclude (LtlSet_t *large, LtlSet_t *small) |
| void | LtlSetOR (LtlSet_t *to, LtlSet_t *from1, LtlSet_t *from2) |
| void | LtlSetClear (LtlSet_t *set) |
| void | LtlSetSetElt (LtlSet_t *set, int index) |
| void | LtlSetClearElt (LtlSet_t *set, int index) |
| int | LtlSetGetElt (LtlSet_t *set, int index) |
| int | LtlSetIsEmpty (LtlSet_t *set) |
| LtlSet_t * | LtlSetIsInList (LtlSet_t *set, lsList list) |
| LtlSet_t * | LtlSetToLabelSet (LtlTableau_t *tableau, LtlSet_t *set) |
| void | LtlSetPrint (LtlTableau_t *tableau, LtlSet_t *set) |
| void | LtlSetPrintIndex (int length, LtlSet_t *set) |
| LtlPair_t * | LtlPairNew (char *First, char *Second) |
| void | LtlPairFree (LtlPair_t *pair) |
| int | LtlPairHash (char *key, int modulus) |
| int | LtlPairCompare (const char *key1, const char *key2) |
| void | LtlPairPrint (LtlPair_t *pair) |
| void | LtlCoverPrintIndex (int length, lsList cover) |
| lsList | LtlCoverCompleteSum (lsList Cover, array_t *Negate) |
| LtlSet_t * | LtlSetConsensus (LtlSet_t *first, LtlSet_t *second, array_t *Negate) |
| lsList | LtlCoverCofactor (lsList Cover, LtlSet_t *c, array_t *Negate) |
| int | LtlCoverIsTautology (lsList Cover, array_t *Negate) |
| int | LtlCoverIsImpliedBy (lsList Cover, LtlSet_t *term, array_t *Negate) |
| lsList | LtlCoverPrimeAndIrredundant (LtlTableau_t *tableau, lsList Cover, array_t *Negate) |
| LtlSet_t * | LtlCoverGetSuperCube (lsList Cover, array_t *Negate) |
| mdd_t * | LtlSetModelCheckFormulae (LtlSet_t *set, array_t *labelTable, Fsm_Fsm_t *fsm) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ltlSet.c,v 1.25 2005/04/28 08:45:27 bli Exp $" |
Function Documentation
| lsList LtlCoverCofactor | ( | lsList | Cover, |
| LtlSet_t * | c, | ||
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return the cofactor of the cover with respect to the set.]
Description [We need the Negate method for each item in the set.]
SideEffects [The result need to be freed by the caller. The input is left unchanged.]
Definition at line 824 of file ltlSet.c.
{
lsList cofactor = lsCopy(Cover, (lsGeneric (*)(lsGeneric))LtlSetCopy);
lsList list;
lsGen lsgen;
st_table *removed = st_init_table(st_ptrcmp, st_ptrhash);
int literal, complement;
LtlSet_t *term;
for (literal=0; literal<array_n(Negate); literal++) {
if (!LtlSetGetElt(c, literal)) continue;
complement = array_fetch(int, Negate, literal);
lsForEachItem(cofactor, lsgen, term) {
if (st_is_member(removed, term)) continue;
if (LtlSetGetElt(term, complement))
st_insert(removed, term, term);
else if (LtlSetGetElt(term, literal))
LtlSetClearElt(term, literal);
}
}
list = cofactor;
cofactor = lsCreate();
lsForEachItem(list, lsgen, term) {
if (st_is_member(removed, term))
LtlSetFree(term);
else
lsNewEnd(cofactor, (lsGeneric) term, (lsHandle *) 0);
}
lsDestroy(list, (void (*)(lsGeneric))0);
st_free_table(removed);
return cofactor;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| lsList LtlCoverCompleteSum | ( | lsList | Cover, |
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return the 'Complete Sum' of the cover by iterated consensus.]
Description [The cover is represented by a list of sets (product terms).]
SideEffects [The result should be freed by the caller. The given cover is NOT changed.]
Definition at line 628 of file ltlSet.c.
{
lsList cs = lsCreate();
lsGen lsgen;
array_t *products = array_alloc(LtlSet_t *, 0);
LtlSet_t *term, *term1, *term2, *consensus;
long i, j, k, flag;
st_table *removed, *consList; /* removed, and consensus generated */
/* Check and remove contraditory terms -- containing both F and !F */
lsForEachItem(Cover, lsgen, term) {
if (!LtlSetIsContradictory(term, Negate))
array_insert_last(LtlSet_t *, products, term);
}
/* Sort terms by increasing number of literals */
array_sort(products, LtlSetCompareCardinality);
/* Check tautologous term */
term = array_fetch(LtlSet_t *, products, 0);
if (LtlSetCardinality(term) == 0) {
lsNewEnd(cs, (lsGeneric) LtlSetCopy(term), (lsHandle *)0);
array_free(products);
return cs;
}
/* In the following, we won't change 'products'. Instead, if a term need to
* be removed, we will store it (its index number) in the hash table
*/
removed = st_init_table(st_ptrcmp, st_ptrhash);
/* In the following, we might generate some new consensus terms, and we will
* store them (LtlSet_t) in the list
*/
consList = st_init_table(st_ptrcmp, st_ptrhash);
/* Check terms for single-cube containment. Rely on ordering for efficiency.
* A term can only be contained by another term with fewer literals
*/
for (i=array_n(products)-1; i>0; i--) {
term = array_fetch(LtlSet_t *, products, i);
for (j=0; j<i; j++) {
term1 = array_fetch(LtlSet_t *, products, j);
if (LtlSetCardinality(term1) == LtlSetCardinality(term)) break;
if (LtlSetInclude(term, term1)) {
/* remember the removed term */
st_insert(removed, (char *)i, (char *)i);
break;
}
}
}
/* Now do iterated consensus */
for (i=1; i<array_n(products); i++) {
if (st_is_member(removed, (char *)i)) continue;
term = array_fetch(LtlSet_t *, products, i);
for (j=0; j<i; j++) {
if (st_is_member(removed, (char *)j)) continue;
term1 = array_fetch(LtlSet_t *, products, j);
consensus = LtlSetConsensus(term, term1, Negate);
if (consensus) {
/* should store consensus ? */
flag = 1;
for(k=0; k<array_n(products); k++) {
if (st_is_member(removed, (char *)k)) continue;
term2 = array_fetch(LtlSet_t *, products, k);
if (LtlSetInclude(consensus, term2)) {
/* redudant new term */
flag = 0;
break;
}
if (LtlSetInclude(term2, consensus)) {
/* remember the removed term2 (k) */
st_insert(removed, (char *)k, (char *)k);
}
}
if (flag) {
array_insert_last(LtlSet_t *, products, consensus);
st_insert(consList, consensus, (char *)0);
}else
LtlSetFree(consensus);
}
}
}
#if 0
if (0) {
fprintf(vis_stdout, "\nLtlCompleteSum: products = { ");
for(i=0; i<array_n(products); i++) {
term = array_fetch(LtlSet_t *, products, i);
LtlSetPrintIndex(array_n(Negate), term);
}
fprintf(vis_stdout, "}\nLtlCompleteSum: removed = { ");
st_foreach_item(removed, stgen, &i, NIL(char *)) {
term = array_fetch(LtlSet_t *, products, i);
LtlSetPrintIndex(array_n(Negate), term);
}
fprintf(vis_stdout, "}\nLtlCompleteSum: consList = { ");
st_foreach_item(consList, stgen, &term, NIL(char *)) {
LtlSetPrintIndex(array_n(Negate), term);
}
fprintf(vis_stdout, "}\n");
fflush(vis_stdout);
}
#endif
arrayForEachItem(LtlSet_t *, products, i, term) {
if (!st_is_member(removed, (char *)i)) {
/* put it into the complete sum list */
if (!st_is_member(consList, term))
term1 = LtlSetCopy(term);
else
term1 = term;
lsNewEnd(cs, (lsGeneric) term1, NIL(lsHandle));
}else {
/* it has been removed. If it was allocated locally, free it */
if (st_is_member(consList, term))
LtlSetFree(term);
}
}
array_free(products);
st_free_table(removed);
st_free_table(consList);
return cs;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| LtlSet_t* LtlCoverGetSuperCube | ( | lsList | Cover, |
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return the supercube of a cover.]
Description []
SideEffects [The result should be freed by the caller.]
Definition at line 972 of file ltlSet.c.
{
LtlSet_t *unate = LtlSetNew(array_n(Negate));
LtlSet_t *binate = LtlSetNew(array_n(Negate));
lsGen lsgen;
LtlSet_t *term;
int literal, neg;
lsForEachItem( Cover, lsgen, term ) {
for (literal=0; literal<array_n(Negate); literal++) {
if (!LtlSetGetElt(term, literal)) continue;
if (LtlSetGetElt(binate, literal) || LtlSetGetElt(unate, literal))
continue;
neg = array_fetch(int, Negate, literal);
if (LtlSetGetElt(unate, neg)) {
LtlSetClearElt(unate, neg);
LtlSetSetElt(binate, literal);
LtlSetSetElt(binate, neg);
}else
LtlSetSetElt(unate, literal);
}
}
LtlSetFree(binate);
return unate;
}
Here is the call graph for this function:
| int LtlCoverIsImpliedBy | ( | lsList | Cover, |
| LtlSet_t * | term, | ||
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return 1 if the given cover is implied BY the set.]
Description []
SideEffects []
Definition at line 903 of file ltlSet.c.
{
lsList cofactor = LtlCoverCofactor(Cover, term, Negate);
int result = LtlCoverIsTautology(Cover, Negate);
lsDestroy(cofactor, (void (*)(lsGeneric))LtlSetFree);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int LtlCoverIsTautology | ( | lsList | Cover, |
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return 1 if the given cover is tautology.]
Description [The test is not fast: the compute sum of the cover should be computed.]
SideEffects []
Definition at line 874 of file ltlSet.c.
{
lsList complete = LtlCoverCompleteSum(Cover, Negate);
LtlSet_t *term;
int result;
if (lsLength(complete) !=1)
result = 0;
else {
lsFirstItem(complete, &term, (lsHandle *)0);
result = (LtlSetCardinality(term) == 0);
}
lsDestroy(complete, (void (*)(lsGeneric))LtlSetFree);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| lsList LtlCoverPrimeAndIrredundant | ( | LtlTableau_t * | tableau, |
| lsList | Cover, | ||
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Boolean minimization of the given cover.]
Description [First, compute a prime and irredundant version of the Cover; Then try to drop each item iff it is implied by the remaining items.
Notice: there might be a bug in the algorithm. Need to be fixed. Need to talke to Fabio/Roderick ]
SideEffects []
Definition at line 931 of file ltlSet.c.
{
lsList pai = LtlCoverCompleteSum(Cover, Negate);
int totalnum; /* total num of terms in current lsList pai */
int procnum; /* how many are already processed so far ? */
LtlSet_t *term;
totalnum = lsLength(pai);
procnum = 0;
/* Try to drop each term in turn */
while(lsDelBegin(pai, &term) != LS_NOMORE) {
if ( (lsLength(pai) != 0) &&
/* !LtlAutomatonSetIsFair(tableau, term) && */
LtlCoverIsImpliedBy(pai, term, Negate) ) {
LtlSetFree(term);
totalnum--;
}else
lsNewEnd(pai, (lsGeneric) term, (lsHandle *)0);
procnum++;
if (procnum >= totalnum)
break;
}
return pai;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void LtlCoverPrintIndex | ( | int | length, |
| lsList | cover | ||
| ) |
Function********************************************************************
Synopsis [Print the cover as a set of index.]
Description []
SideEffects []
Definition at line 599 of file ltlSet.c.
{
int first = 1;
lsGen gen;
LtlSet_t *set;
fprintf(vis_stdout, "{ ");
lsForEachItem(cover, gen, set) {
if (first) first = 0;
else fprintf(vis_stdout, " + ");
LtlSetPrintIndex(length, set);
}
fprintf(vis_stdout, " }");
}
Here is the call graph for this function:
| int LtlPairCompare | ( | const char * | key1, |
| const char * | key2 | ||
| ) |
Function********************************************************************
Synopsis [Return -1/0/+1 when the key1 is greater/equal/less than key2.]
Description [For two keys with the same content, they are equal.]
SideEffects []
Definition at line 550 of file ltlSet.c.
{
LtlPair_t *pair1 = (LtlPair_t *) key1;
LtlPair_t *pair2 = (LtlPair_t *) key2;
assert(key1 != NIL(char));
assert(key2 != NIL(char));
if ((pair1->First == pair2->First) && (pair1->Second == pair2->Second))
return 0;
else if (pair1->First >= pair2->First && pair1->Second >= pair2->Second)
return 1;
else
return -1;
}
Here is the caller graph for this function:
| void LtlPairFree | ( | LtlPair_t * | pair | ) |
| int LtlPairHash | ( | char * | key, |
| int | modulus | ||
| ) |
Function********************************************************************
Synopsis [Return a hash key for the given pair.]
Description [The key is based on the content. Thus two pair with the same content (not necessarily the same pointer) have the same hash key.]
SideEffects []
Definition at line 530 of file ltlSet.c.
{
LtlPair_t *pair = (LtlPair_t *) key;
return (int) ((((unsigned long) pair->First >>2) +
((unsigned long) pair->Second>>4)) % modulus);
}
Here is the caller graph for this function:
| LtlPair_t* LtlPairNew | ( | char * | First, |
| char * | Second | ||
| ) |
| void LtlPairPrint | ( | LtlPair_t * | pair | ) |
Function********************************************************************
Synopsis [Print the pair as index pair.]
Description []
SideEffects []
Definition at line 578 of file ltlSet.c.
{
vertex_t *first = (vertex_t *) pair->First;
vertex_t *second= (vertex_t *) pair->Second;
Ltl_AutomatonNode_t *node1 = (Ltl_AutomatonNode_t *) first->user_data;
Ltl_AutomatonNode_t *node2 = (Ltl_AutomatonNode_t *) second->user_data;
fprintf(vis_stdout, " (n%d, n%d) ", node1->index, node2->index);
}
| void LtlSetAssign | ( | LtlSet_t * | to, |
| LtlSet_t * | from | ||
| ) |
Function********************************************************************
Synopsis [Assign the content of 'from' to set 'to'.]
Description []
SideEffects [set 'to' is changed.]
Definition at line 135 of file ltlSet.c.
{
var_set_assign(to->e, from->e);
}
Here is the caller graph for this function:
| int LtlSetCardinality | ( | LtlSet_t * | set | ) |
| void LtlSetClear | ( | LtlSet_t * | set | ) |
| void LtlSetClearElt | ( | LtlSet_t * | set, |
| int | index | ||
| ) |
| int LtlSetCompareCardinality | ( | const void * | p1, |
| const void * | p2 | ||
| ) |
Function********************************************************************
Synopsis [Return -1/0/+1 when 's1' has more/equal/less cardinality than 's2'.]
Description []
SideEffects []
Definition at line 187 of file ltlSet.c.
{
LtlSet_t **s1 = (LtlSet_t **) p1;
LtlSet_t **s2 = (LtlSet_t **) p2;
int c1;
int c2;
c1 = LtlSetCardinality(*s1);
c2 = LtlSetCardinality(*s2);
if (c1 < c2)
return -1;
else if (c1 == c2)
return 0;
else
return +1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| LtlSet_t* LtlSetConsensus | ( | LtlSet_t * | first, |
| LtlSet_t * | second, | ||
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return the consensus of two given set (product terms).]
Description [If the consesus does not exist, return a null pointer.]
SideEffects [The result should be freed by the caller.]
Definition at line 773 of file ltlSet.c.
{
LtlSet_t *consensus = LtlSetNew(array_n(Negate));
int pivot = -1;
int literal, complement;
for (literal=0; literal<array_n(Negate); literal++) {
if (LtlSetGetElt(first, literal)) {
complement = array_fetch(int, Negate, literal);
if (LtlSetGetElt(second, complement)) {
if (pivot != -1) {
LtlSetFree(consensus);
return NIL(LtlSet_t);
}else {
pivot = complement;
}
}else {
LtlSetSetElt(consensus, literal);
}
}
}
/* if pivot has never been defined, return NIL */
if (pivot == -1) {
LtlSetFree(consensus);
return NIL(LtlSet_t);
}
for (literal=0; literal<array_n(Negate); literal++) {
if (LtlSetGetElt(second, literal)) {
if (literal != pivot)
LtlSetSetElt(consensus, literal);
}
}
return consensus;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| LtlSet_t* LtlSetCopy | ( | LtlSet_t * | from | ) |
Function********************************************************************
Synopsis [Allocate the new set and copy the content of the given set.]
Description []
SideEffects [The result should be freed by the caller.]
Definition at line 115 of file ltlSet.c.
{
LtlSet_t *set = ALLOC(LtlSet_t, 1);
set->e = var_set_copy(from->e);
return set;
}
Here is the caller graph for this function:
| int LtlSetEqual | ( | LtlSet_t * | s1, |
| LtlSet_t * | s2 | ||
| ) |
| void LtlSetFree | ( | LtlSet_t * | set | ) |
| int LtlSetGetElt | ( | LtlSet_t * | set, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Return the value of the bit indicated by 'index'.]
Description []
SideEffects [The set is changed.]
Definition at line 336 of file ltlSet.c.
{
return var_set_get_elt(set->e,index);
}
Here is the caller graph for this function:
| int LtlSetInclude | ( | LtlSet_t * | large, |
| LtlSet_t * | small | ||
| ) |
Function********************************************************************
Synopsis [Return 1 iff 'large' includes 'small'.]
Description []
SideEffects []
Definition at line 247 of file ltlSet.c.
{
var_set_t *neg_large = var_set_not(var_set_copy(large->e),large->e);
int result = ! var_set_intersect(small->e, neg_large);
var_set_free(neg_large);
return result;
}
Here is the caller graph for this function:
| int LtlSetIsContradictory | ( | LtlSet_t * | set, |
| array_t * | Negate | ||
| ) |
Function********************************************************************
Synopsis [Return 1 iff the set contains both 'F' and '!F'.]
Description []
SideEffects []
Definition at line 217 of file ltlSet.c.
{
int i, negi;
int flag = 0;
for (i=0; i<array_n(Negate); i++) {
if (LtlSetGetElt(set, i)) {
negi = array_fetch(int, Negate, i);
if (LtlSetGetElt(set, negi)) {
flag = 1;
break;
}
}
}
return flag;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int LtlSetIsEmpty | ( | LtlSet_t * | set | ) |
| LtlSet_t* LtlSetIsInList | ( | LtlSet_t * | set, |
| lsList | list | ||
| ) |
Function********************************************************************
Synopsis [Return the set in the list that matches the given set.]
Description [Null will be return if there does not exist a match set.]
SideEffects []
Definition at line 369 of file ltlSet.c.
{
lsGen gen;
lsGeneric data;
LtlSet_t *s = NIL(LtlSet_t);
int flag = 0;
lsForEachItem(list, gen, data) {
s = (LtlSet_t *) data;
if ( var_set_equal(s->e, set->e) ) {
flag = 1;
lsFinish(gen);
break;
}
}
return flag? s: NIL(LtlSet_t);
}
Here is the caller graph for this function:
| mdd_t* LtlSetModelCheckFormulae | ( | LtlSet_t * | set, |
| array_t * | labelTable, | ||
| Fsm_Fsm_t * | fsm | ||
| ) |
Function********************************************************************
Synopsis [Return the supercube of a cover.]
Description []
SideEffects [The result should be freed by the caller.]
Definition at line 1014 of file ltlSet.c.
{
mdd_t *minterm, *mdd1, *mdd2;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
mdd_t *mddOne = mdd_one(mddManager);
array_t *careStatesArray = array_alloc(mdd_t *, 0);
int i;
array_insert(mdd_t *, careStatesArray, 0, mddOne);
minterm = mdd_dup(mddOne);
for (i=0; i<array_n(labelTable); i++) {
if (LtlSetGetElt(set, i)) {
Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, labelTable, i);
Ctlp_Formula_t *ctlF = Ctlsp_PropositionalFormulaToCTL(F);
mdd1 = Mc_FsmEvaluateFormula(fsm, ctlF, mddOne,
NIL(Fsm_Fairness_t),
careStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(Fsm_HintsArray_t), Mc_None_c,
McVerbosityNone_c, McDcLevelNone_c, 0,
McGSH_EL_c);
mdd2 = minterm;
minterm = mdd_and(minterm, mdd1, 1, 1);
mdd_free(mdd2);
mdd_free(mdd1);
Ctlp_FormulaFree(ctlF);
}
}
mdd_array_free(careStatesArray);
return minterm;
}
Here is the call graph for this function:
| LtlSet_t* LtlSetNew | ( | int | size | ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Allocate the set data structure.]
Description []
SideEffects [The result should be freed by the caller.]
Definition at line 78 of file ltlSet.c.
{
LtlSet_t *set = ALLOC(LtlSet_t, 1);
set->e = var_set_new(size);
return set;
}
Here is the caller graph for this function:
| void LtlSetOR | ( | LtlSet_t * | to, |
| LtlSet_t * | from1, | ||
| LtlSet_t * | from2 | ||
| ) |
Function********************************************************************
Synopsis [Union the two sets 'from1' and 'from2', and assign to set 'to'.]
Description []
SideEffects [set 'to' is changed.]
Definition at line 268 of file ltlSet.c.
{
var_set_or(to->e, from1->e, from2->e);
}
Here is the caller graph for this function:
| void LtlSetPrint | ( | LtlTableau_t * | tableau, |
| LtlSet_t * | set | ||
| ) |
Function********************************************************************
Synopsis [Print all the 'elementary formulae' contained in the set.]
Description [Assume the set is based on the index table 'tableau->abTable'.]
SideEffects []
Definition at line 440 of file ltlSet.c.
{
int i;
fprintf(vis_stdout, "{ ");
for (i=0; i<tableau->abIndex; i++) {
if (LtlSetGetElt(set, i)) {
Ctlsp_FormulaPrint(vis_stdout, tableau->abTable[i].F);
fprintf(vis_stdout, "; ");
}
}
fprintf(vis_stdout, " }");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void LtlSetPrintIndex | ( | int | length, |
| LtlSet_t * | set | ||
| ) |
Function********************************************************************
Synopsis [Print all index that are set in the set.]
Description [The length of the set should be provided.]
SideEffects []
Definition at line 466 of file ltlSet.c.
{
int i;
fprintf(vis_stdout, "{ ");
for (i=0; i<length; i++) {
if (LtlSetGetElt(set, i)) {
fprintf(vis_stdout, " %d ", i);
}
}
fprintf(vis_stdout, " }\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void LtlSetSetElt | ( | LtlSet_t * | set, |
| int | index | ||
| ) |
| LtlSet_t* LtlSetToLabelSet | ( | LtlTableau_t * | tableau, |
| LtlSet_t * | set | ||
| ) |
Function********************************************************************
Synopsis [Transform the given set to the label set and return it.]
Description [The given set may contain all the 'elementary formulae'. Its table and negation are 'tableau->abTable' and 'tableau->abTableNegate'.
The label set contain only the propositional formulae and their negations. Its table and negation array are 'labelTable' and 'labelNegate'.
The above two table could have been the same, but we choose to implement them differently: Since labelTable might be smaller than abTable, it will make the boolean minimization based on it faster.]
SideEffects [The result should be freed by the caller.]
Definition at line 408 of file ltlSet.c.
{
int i;
LtlSet_t *vset = LtlSetNew(tableau->labelIndex);
Ctlsp_Formula_t *F;
for (i=0; i<tableau->abIndex; i++) {
if (var_set_get_elt(set->e, i)) {
F = tableau->abTable[i].F;
if (Ctlsp_LtlFormulaIsPropositional(F)&&
Ctlsp_FormulaReadType(F) != Ctlsp_TRUE_c &&
Ctlsp_FormulaReadType(F) != Ctlsp_FALSE_c)
var_set_set_elt(vset->e,
Ctlsp_FormulaReadLabelIndex(tableau->abTable[i].F));
}
}
return vset;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ltlSet.c,v 1.25 2005/04/28 08:45:27 bli Exp $" [static] |
CFile***********************************************************************
FileName [ltlSet.c]
PackageName [ltl]
Synopsis [Set/Pair/Cover Manipulation functions used in the ltl package.]
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.]
