src/ltl/ltlSet.c

Go to the documentation of this file.

#include "ltlInt.h"

static char rcsid[] UNUSED = "$Id: ltlSet.c,v 1.25 2005/04/28 08:45:27 bli Exp $";

/* Set manipulation functions.
 *  
 * Set is a term -- the conjunction of literals. In the Ltl->Aut process, a
 * literal can be an propositional formula, a X-formula and its negation.
 * In order to interpret a Set, we need to corresponding arrays: Table and
 * Negate. An '1' in the i-th position of the Set means "Table[i] is contained
 * in the Set", and the negation of "Table[i]" is "Negate[i]".
 * 
 * Cover is a lsList of terms -- the "union" of all the items (product terms).
 *
 * Pair is a data structure to hold a 'ordered pair of items': (First, Second).
 */

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

LtlSet_t *
LtlSetNew(
  int size)
{
  LtlSet_t *set = ALLOC(LtlSet_t, 1);
    
  set->e = var_set_new(size);

  return set;
}

void
LtlSetFree(
  LtlSet_t *set)
{
  var_set_free(set->e);
  FREE(set);
}

LtlSet_t *
LtlSetCopy(
  LtlSet_t *from)
{
  LtlSet_t *set = ALLOC(LtlSet_t, 1);
  
  set->e = var_set_copy(from->e);
  
  return set;
}

void
LtlSetAssign(
  LtlSet_t *to,
  LtlSet_t *from)
{
  var_set_assign(to->e, from->e);
}

int
LtlSetEqual(
  LtlSet_t *s1,
  LtlSet_t *s2)
{
  return var_set_equal(s1->e, s2->e);
}


int
LtlSetCardinality(
  LtlSet_t *set)
{
  return (var_set_n_elts(set->e));
}

int
LtlSetCompareCardinality(
  const void *p1,
  const void *p2)
{
  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;
}

int
LtlSetIsContradictory(
  LtlSet_t *set,
  array_t *Negate)
{
  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;
}

int
LtlSetInclude(
  LtlSet_t *large,
  LtlSet_t *small)
{
  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;
}

void
LtlSetOR(
  LtlSet_t *to,
  LtlSet_t *from1,
  LtlSet_t *from2)
{
  var_set_or(to->e, from1->e, from2->e);
}

void
LtlSetClear(
  LtlSet_t *set)
{
  var_set_clear(set->e);
}

void
LtlSetSetElt(
  LtlSet_t *set,
  int index)
{
  var_set_set_elt(set->e, index);
}

void
LtlSetClearElt(
  LtlSet_t *set,
  int index)
{
  var_set_clear_elt(set->e, index);
}

int
LtlSetGetElt(
  LtlSet_t *set,
  int index)
{
  return var_set_get_elt(set->e,index);
}

int
LtlSetIsEmpty(
  LtlSet_t *set)
{
  return var_set_is_empty(set->e);
}

LtlSet_t *
LtlSetIsInList(
  LtlSet_t *set,
  lsList list)
{
  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);
}
    
LtlSet_t *
LtlSetToLabelSet(
  LtlTableau_t *tableau,
  LtlSet_t *set)
{
  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;
}

void
LtlSetPrint(
  LtlTableau_t *tableau,
  LtlSet_t *set)
{
  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, " }");
}

void
LtlSetPrintIndex(
  int length,
  LtlSet_t *set)
{
  int i;
  
  fprintf(vis_stdout, "{ ");
  for (i=0; i<length; i++) {
    if (LtlSetGetElt(set, i)) {
      fprintf(vis_stdout, " %d ", i);
    }
  }
  fprintf(vis_stdout, " }\n");
}


LtlPair_t *
LtlPairNew(
  char *First,
  char *Second)
{
  LtlPair_t *pair = ALLOC(LtlPair_t, 1);

  pair->First = First;
  pair->Second= Second;
  return pair;
}

void
LtlPairFree(
  LtlPair_t *pair)
{
  FREE(pair);
}

int
LtlPairHash(
  char *key,
  int modulus)
{
  LtlPair_t *pair = (LtlPair_t *) key;
  
  return (int) ((((unsigned long) pair->First >>2) +
                 ((unsigned long) pair->Second>>4)) % modulus);
}

int 
LtlPairCompare(
  const char *key1,
  const char *key2)
{
  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;
}

void
LtlPairPrint(
  LtlPair_t *pair)
{
  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
LtlCoverPrintIndex(
  int length,
  lsList cover)
{
  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, " }");
}


lsList 
LtlCoverCompleteSum(
  lsList Cover,
  array_t *Negate)
{
  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;
}


LtlSet_t *
LtlSetConsensus(
  LtlSet_t *first,
  LtlSet_t *second,
  array_t *Negate)
{
  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;
}

lsList
LtlCoverCofactor(
  lsList Cover,
  LtlSet_t *c,
  array_t *Negate)
{
  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;
}
      
int
LtlCoverIsTautology(
  lsList Cover,
  array_t *Negate)
{
  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;
}

int
LtlCoverIsImpliedBy(
  lsList Cover,
  LtlSet_t *term,
  array_t *Negate)
{
  lsList cofactor = LtlCoverCofactor(Cover, term, Negate);
  int result = LtlCoverIsTautology(Cover, Negate);
  lsDestroy(cofactor, (void (*)(lsGeneric))LtlSetFree);
  
  return result;
}
    

lsList
LtlCoverPrimeAndIrredundant(
  LtlTableau_t *tableau,
  lsList Cover,
  array_t *Negate)
{
  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;
}


LtlSet_t *
LtlCoverGetSuperCube(
  lsList Cover,
  array_t *Negate)
{
  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;
}



mdd_t *
LtlSetModelCheckFormulae(
  LtlSet_t *set,
  array_t *labelTable,
  Fsm_Fsm_t *fsm)
{
  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;
}