/**CFile***********************************************************************

  FileName    [bmcAutSat.c]

  PackageName [bmc]
 
  Synopsis    [Automaton for BMC]

  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.]
******************************************************************************/

#include "bmc.h"
#include "bmcInt.h"

static char rcsid[] UNUSED = "$Id: bmcAutSat.c,v 1.10 2005/04/16 18:02:25 awedh Exp $";

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

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


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


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


/**AutomaticStart*************************************************************/

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


/**AutomaticEnd***************************************************************/


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


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

 Synopsis [Verify the general LTL formula passes by applying the
   termination criteria that are described in the paper "Proving More
   Properties with Bounded Model Checking"]

  Description [Check for the termination on the composition of the
  automaton that describes the negation of the LTL formula and the
  model.  We apply the termination criteria as described in the paper
  "Proving More Properties with Bounded Model Checking".]

  Return value:
        -1 error in running BMC
	 0 no action
	 1 (m+n-1) <= options->maxK.  If no counterexample of length up to (m+n-1),
	                              the property passes
	 2 (m+n-1) >  options->maxK   The property is undecided if no counterexample
	                              of length <= options->maxK.
	 3 Pass by early termination
  
  SideEffects []

  SeeAlso     []

******************************************************************************/
int
BmcAutLtlCheckForTermination(
  Ntk_Network_t            *network,
  array_t                  *constraintArray,
  BmcCheckForTermination_t *terminationStatus,
  st_table                 *nodeToMvfAigTable,
  st_table                 *CoiTable,
  BmcOption_t              *options)
{
  
  BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
  FILE            *cnfFile;
  array_t         *result = NIL(array_t);
  array_t         *unitClause = array_alloc(int, 0);
  array_t         *orClause;

  long            startTime, endTime;
  int             k = terminationStatus->k;
  int             returnStatus = 0;
  Ltl_Automaton_t *automaton = terminationStatus->automaton;

  /*
    If checkLevel == 0 -->  check for beta' only and if UNSAT, m=k and chekLevel =1
    If checkLevel == 1 -->  check for beta  only and if UNSAT, checkLevel = 2.
    If checkLevel == 2 -->  check for alpha only and if UNSAT, n=k and checkLevel = 3.
    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
    checkLevel = 4 if (m+n-1) > maxK;
   */ 
  startTime = util_cpu_ctime();
 
  /* ===========================
     Early termination condition
     =========================== */
  if (options->earlyTermination) {
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
    }
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();

    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
		    "** bmc error: Cannot create CNF output file %s\n",
		    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
						cnfClauses, nodeToMvfAigTable, CoiTable);
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    BmcCnfClausesFree(cnfClauses);
	  
    result = BmcCheckSAT(options);
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      (void) fprintf(vis_stdout, "# BMC: by early ermination\n");
      return 3;
    }
  } /* Early termination */
   if((!automaton->fairSets) &&
     (terminationStatus->checkLevel == 0)) {
    /*
      All the automaton states are fair states. So, beta' and beta are always UNSAT.
    */
    terminationStatus->m = 0;
     (void) fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
    terminationStatus->checkLevel = 2;
  }
  /*
    beta''(k) 
  */
  if(terminationStatus->checkLevel == 0){ 
    int i;
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta'' \n");
    }
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
		    "** bmc error: Cannot create CNF output file %s\n",
		    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
						cnfClauses, nodeToMvfAigTable, CoiTable);
    for(i=1; i<=k+1; i++){
      if(constraintArray != NIL(array_t)){
	Ctlsp_Formula_t *formula;
	int              j;
	
	arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	  array_insert(int, unitClause, 0,
		       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
		       );
	  BmcCnfInsertClause(cnfClauses, unitClause);
	}
      }
      array_insert(int, unitClause, 0,
		   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
		   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
       if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	array_insert_last(int, orClause,
			  BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
			  );
      }
      array_insert_last(int, orClause, 
			BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
			);
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else {
      array_insert(int, unitClause, 0, 
		   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, 0, 0, cnfClauses, NIL(st_table))
		   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->m = k;
      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check for Beta' */
  
  /*
    beta'(k) 
  */
  if(terminationStatus->checkLevel == 0){
    int i;
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta' \n");
    }
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
		    "** bmc error: Cannot create CNF output file %s\n",
		    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
						cnfClauses, nodeToMvfAigTable, CoiTable);
    for(i=0; i<=k; i++){
      if(constraintArray != NIL(array_t)){
	Ctlsp_Formula_t *formula;
	int              j;
	
	arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	  array_insert(int, unitClause, 0,
		       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
		       );
	  BmcCnfInsertClause(cnfClauses, unitClause);
	}
      }
      array_insert(int, unitClause, 0,
		   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
		   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	array_insert_last(int, orClause,
			  BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
			  );
      }
      array_insert_last(int, orClause, 
			BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
			);
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else {
      array_insert(int, unitClause, 0, 
		   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
		   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->m = k;
      (void)fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check for Beta' */
  
  /*
    Check for Beta.
  */
  if(terminationStatus->checkLevel == 1){
    cnfClauses = BmcCnfClausesAlloc();
    {/* To print a witness */
      /*  lsGen               lsGen;
      vertex_t            *vtx;
      Ltl_AutomatonNode_t *state;
      int i;
      
      foreach_vertex(automaton->G, lsGen, vtx) {
	state = (Ltl_AutomatonNode_t *) vtx->user_data;
	state->cnfIndex = ALLOC(int, k+2);
	for(i=0; i<=k+1; i++){
	  state->cnfIndex[i] = BmcAutGenerateCnfForBddOffSet(state->Encode, i,
							     i, cnfClauses, NIL(st_table));
	}
	} */
    }/* To print a witness */
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
    }
    
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
		    "** bmc error: Cannot create CNF output file %s\n",
		    options->satInFile);
      return -1;
    }
    /*
      Generate a simple path of length k+1.
    */
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
						cnfClauses, nodeToMvfAigTable,
						   CoiTable);

    if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	array_insert(int, unitClause, 0,
		     - BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
		     );
	BmcCnfInsertClause(cnfClauses, unitClause);
      }
    }
    
    array_insert(int, unitClause, 0, 
		 - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
		 );
    BmcCnfInsertClause(cnfClauses, unitClause);

   if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	array_insert_last(int, orClause,
			  BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
			  );
      }
      array_insert_last(int, orClause, 
			BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
			);
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else { 
      array_insert(int, unitClause, 0, 
		   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
		   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->checkLevel = 2;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check Beta*/
  
  if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
    }
    
    cnfClauses = BmcCnfClausesAlloc();
      
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
		    "** bmc error: Cannot create CNF output file %s\n",
		    options->satInFile);
      return -1;
    }
    
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
						cnfClauses, nodeToMvfAigTable, CoiTable);
    if(automaton->fairSets){

      if(constraintArray != NIL(array_t)){
	Ctlsp_Formula_t *formula;
	int              j;
	
	orClause   = array_alloc(int, 0);
	
	arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
	  array_insert_last(int, orClause,
			    BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
			    );
	}
	array_insert_last(int, orClause, 
			  BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
			  );
	BmcCnfInsertClause(cnfClauses, orClause);
	array_free(orClause);
      } else {
	
	array_insert(int, unitClause, 0,  
		     BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
		     );
	BmcCnfInsertClause(cnfClauses, unitClause);
      }
    }
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    BmcCnfClausesFree(cnfClauses);
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->n = k;
      terminationStatus->checkLevel = 3;
      (void)fprintf(vis_stderr,"m=%d  n=%d\n",terminationStatus->m,terminationStatus->n);
      if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
	terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
	if(k==0){
	  /*
	    By induction, the property passes.
	  */
	  terminationStatus->k = 0;
	}
	returnStatus = 1;
      } else {
	terminationStatus->checkLevel = 4;
	returnStatus = 2;
      }
    }
  }/* Chek for Alpha */
  
  array_free(unitClause);

  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
	    (double)(endTime - startTime) / 1000.0);
  }

  return returnStatus;
 
} /* BmcAutLtlCheckForTermination */


/**Function********************************************************************

  Synopsis [Generate CNF clauses that describe a path in the automaton.] 

  Description [Generate CNF clauses for a path in the automaton
  starting from "fromState" and ending at "toState". If "initialState"
  = BMC_INITIAL_STATES, the the path starts from an initial state.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcAutCnfGenerateClausesForPath(
  Ltl_Automaton_t *automaton,
  int             fromState,
  int             toState,
  int             initialState,
  BmcCnfClauses_t *cnfClauses)
{
  int          k;
  array_t      *unitClause = array_alloc(int, 1);

  if(initialState){
    array_insert(int, unitClause, 0, 
		 BmcAutGenerateCnfForBddOffSet(automaton->initialStates, 0, 0, cnfClauses, automaton->nsPsTable)
		 );
    BmcCnfInsertClause(cnfClauses, unitClause);
  }
  for(k=fromState; k<toState; k++){
    array_insert(int, unitClause, 0,  
    BmcAutGenerateCnfForBddOffSet(automaton->transitionRelation, k, k+1, cnfClauses, automaton->nsPsTable)
		      );
    BmcCnfInsertClause(cnfClauses, unitClause);
  }
  array_free(unitClause);
  
} /* BmcAutCnfGenerateClausesForPath() */


/**Function********************************************************************

  Synopsis [Generate CNF clauses for a simple path in the composite
  model]

  Description [This function generates CNF clauses for a simple path
  from state "fromState" to state "toState" in the composition of
  network and automaton.  A simple path is a path along which every
  state in the path is distinct.  If Si and Sj in the path then Si !=
  Sj.

  If the value of "initialState" is BMC_INITIAL_STATES, then the path
  is an initialized path.  Otherwise "initialState" is
  BMC_NO_INITIAL_STATES.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcAutCnfGenerateClausesForSimpleCompositePath(
   Ntk_Network_t   *network,
   Ltl_Automaton_t *automaton,
   int             fromState,
   int             toState,
   int             initialState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  int state;
  
  /*
    Generate clauses for a path from fromState to toState in the original model.
  */
  BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
  /*
    Generate clauses for a path from fromState to toState in the Automaton.
  */
  BmcAutCnfGenerateClausesForPath(automaton, fromState, toState, initialState, cnfClauses);
  
  /*
    Restrict the above path to be simpe path.
  */
  for(state= fromState + 1; state < toState; state++){
    BmcCnfNoLoopToAnyPreviouseCompositeStates(network, automaton, fromState, state,
					      cnfClauses, nodeToMvfAigTable, CoiTable);
  }

  return;
} /* BmcAutCnfGenerateClausesForSimpleCompositePath */


/**Function********************************************************************

  Synopsis [Generate CNF clauses for no loop from last state to any of
  the previouse states of the path]

  Description [Generate CNF clauses for no loop from last state
  "toState" to any of the previous states starting from
  "fromState". It generates the CNF clauses such that the last state
  of the path is not equal to any previous states.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfNoLoopToAnyPreviouseCompositeStates(
   Ntk_Network_t   *network,
   Ltl_Automaton_t *automaton,
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t     *manager   = Ntk_NetworkReadMAigManager(network);
  bdd_manager        *bddManager = bdd_get_manager(automaton->transitionRelation);
  
  Ntk_Node_t         *latch;
  MvfAig_Function_t  *latchMvfAig;
  bAigEdge_t         *latchBAig;
  array_t            *orClause;
  int                currentIndex, nextIndex, andIndex1, andIndex2;  
  int                i, k, mvfSize, bddID;
    
  st_generator       *stGen;

  /*
    Generates CNF clauses to constrain that the toState is not equal
    to any previouse states starting from fromState.
    
    Assume there are two state varaibles a and b. To check if Si !=
    Sj, we must generate clauses for the formula ( ai != aj + bi !=
    bj).
  */
  for(k=fromState; k < toState; k++){
    orClause = array_alloc(int,0);
    st_foreach_item(CoiTable, stGen, &latch, NULL) {
      
  
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
	array_free(latchMvfAig);
	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      } 
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
	latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
      }

      for (i=0; i< mvfSize; i++){
	currentIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
	nextIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);	 
	andIndex1 = cnfClauses->cnfGlobalIndex++;
	BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
	andIndex2 = cnfClauses->cnfGlobalIndex++;
	BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);

	array_insert_last(int, orClause, andIndex1);
	array_insert_last(int, orClause, andIndex2);
      }
      FREE(latchBAig);
    }/* For each latch loop*/
    st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
      currentIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
						 k, cnfClauses);
      nextIndex    = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
						 toState, cnfClauses);
      						 
      andIndex1 = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
      andIndex2 = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
      
      array_insert_last(int, orClause, andIndex1);
      array_insert_last(int, orClause, andIndex2);
    }
    BmcCnfInsertClause(cnfClauses, orClause);
    array_free(orClause);
  } /* foreach k*/
  return;
} /* BmcCnfNoLoopToAnyPreviouseCompositeStates */