#include "amcInt.h"
#include "mcInt.h"

Include dependency graph for amcBlock.c:

Data Structures
struct	BlockInfoStruct
struct	BlockSubsystemInfoStruct
Typedefs
typedef struct BlockInfoStruct	BlockInfo_t
typedef struct BlockSubsystemInfoStruct	BlockSubsystemInfo_t
Functions
static BlockInfo_t *	AmcObtainOptimalSystemUpperBound (Amc_Info_t amcInfo, Ctlp_Formula_t formula, BlockInfo_t *BlockInfo, int verbosity)
static BlockInfo_t *	AmcObtainOptimalSystemLowerBound (Amc_Info_t amcInfo, Ctlp_Formula_t formula, BlockInfo_t *BlockInfo, int verbosity)
static void	AmcInitializeDependency (array_t *subSystemArray, int isMBM)
static void	AmcInitializeSchedule (Amc_Info_t *amcInfo)
static int	AmcIsEverySubsystemRescheduled (Amc_Info_t *amcInfo)
static void	AmcPrintScheduleInformation (Amc_Info_t *amcInfo)
static array_t *	AmcInitializeQuantifyVars (Amc_SubsystemInfo_t *subSystem)
static int	AmcBlockSubsystemReadScheduledForRefinement (BlockSubsystemInfo_t *system)
static void	AmcBlockSubsystemSetScheduledForRefinement (BlockSubsystemInfo_t *system, int data)
static void	AmcBlockSetOptimalSystem (BlockInfo_t system, Amc_SubsystemInfo_t data)
static void	AmcBlockSetBestSystem (BlockInfo_t *system, int data)
int	AmcBlockTearingProc (Amc_Info_t amcInfo, Ctlp_Formula_t formula, int verbosity)
void	AmcFreeBlock (Amc_Info_t *amcInfo)
Variables
static char rcsid[]	UNUSED = "$Id: amcBlock.c,v 1.35 2005/04/25 20:24:53 fabio Exp $"

Typedef Documentation

typedef struct BlockInfoStruct BlockInfo_t

Definition at line 50 of file amcBlock.c.

typedef struct BlockSubsystemInfoStruct BlockSubsystemInfo_t

Definition at line 51 of file amcBlock.c.

Function Documentation

static void AmcBlockSetBestSystem	(	BlockInfo_t *	system,
		int	data
	)		`[static]`

Function********************************************************************

Synopsis [Set best system.]

SideEffects []

Definition at line 1306 of file amcBlock.c.

{
  system->bestSystem = data;
}

Here is the caller graph for this function:

static void AmcBlockSetOptimalSystem	(	BlockInfo_t *	system,
		Amc_SubsystemInfo_t *	data
	)		`[static]`

Function********************************************************************

Synopsis [Set optimal system.]

SideEffects []

Definition at line 1275 of file amcBlock.c.

{
  system->optimalSystem = data;
}

Here is the caller graph for this function:

static int AmcBlockSubsystemReadScheduledForRefinement ( BlockSubsystemInfo_t * system ) [static]

Function********************************************************************

Synopsis [Read scheduling information.]

SideEffects []

Definition at line 1229 of file amcBlock.c.

{
  return system->scheduledForRefinement;
}

Here is the caller graph for this function:

static void AmcBlockSubsystemSetScheduledForRefinement	(	BlockSubsystemInfo_t *	system,
		int	data
	)		`[static]`

Function********************************************************************

Synopsis [Set scheduling information.]

SideEffects []

Definition at line 1243 of file amcBlock.c.

{
  system->scheduledForRefinement = data;
}

Here is the caller graph for this function:

int AmcBlockTearingProc	(	Amc_Info_t *	amcInfo,
		Ctlp_Formula_t *	formula,
		int	verbosity
	)

AutomaticEnd Function********************************************************************

Synopsis [A block-tearing procedure.]

Description [From an array of subsystems, the routine picks a subsystem that produces best result. When proving true positive, a subsystem that produces smallest cardinality of the error state is chosen as the best subsystem. Error states are defined as; (Initial States) - (Subset of states satisfying given formula). An over-approximation of the transition relation produces a subset of states satisfying the original ACTL formula. Whenever the subset of states satisfying given formula contains the initial states, we conclude that the system models the specification. The routine treats initial states as a monotonically decreasing(cardinality wise) set. This is because when we identify the set of subsets of states satisfying given ACTL formula cover the initial states, we can conclude that the initial states are entirely contained in the exact set of states satisfying given ACTL formula. Hence, once we identify an error states, the routine updates the error states as new initial states.

When proving true negative of given ACTL formula, the best subsystem is that produces smallest cardinality of the superset of states satisfying ACTL formula in consideration. An under-approximation of the transition relation of the original system produces a superset of states satisfying the ACTL formulas. Whenever we find an initial state(s) that are not contained in the superset of states satisfying given ACTL formula, we conclude that the system does not model the specification. An initial state(s) that is not contained in the superset of states satisfying an ACTL formula is used to produce a debug trace.

When "machine by machine" switch is ON, refinement of either subsets or the supersets of states satisfying given formula is performed. This process is done until the refinements cannot be made. (Note; "machine by machine" refinement is not yet supported. 2/12/97)

]

SideEffects []

Definition at line 149 of file amcBlock.c.

{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem;
  BlockInfo_t           BlockInfo;


  /*
   * Update fan-in subsystems and fan-out subsystems when machine by machine 
   * method is ON.
   * Update initial states in BlockInfo.
   * Reschedule every subsystem to be evaluated.
   */

  if( amcInfo->optimalSystem == NIL(Amc_SubsystemInfo_t) ) {
    AmcInitializeDependency(subSystemArray, amcInfo->isMBM);
  }

  AmcInitializeSchedule(amcInfo);

  /* BlockInfo is a temporary storage. optimal system is not freed */
  BlockInfo.optimalSystem = NIL(Amc_SubsystemInfo_t);
    

  /*
   * Outer loop until there's no scheduled subsystem.
   */
  while(AmcIsEverySubsystemRescheduled(amcInfo)) {

    if(verbosity == Amc_VerbosityNone_c)
      AmcPrintScheduleInformation(amcInfo);


    if( !amcInfo->lowerBound ) {
        AmcObtainOptimalSystemUpperBound(amcInfo, formula, &BlockInfo, 
                                         verbosity);
        /* AmcObtainOptimalSystemUpperBoundWithDI(amcInfo, formula, &BlockInfo,
                                                  verbosity); */
    }
    else {
        AmcObtainOptimalSystemLowerBound(amcInfo, formula, &BlockInfo, 
                                         verbosity);
        /* AmcObtainOptimalSystemLowerBoundWithMBM(amcInfo, formula, &BlockInfo,
                                                   verbosity); */
    }

    if(amcInfo->isVerified) {

        int best = BlockInfo.bestSystem;
        subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray,
                                best);
        subSystem->takenIntoOptimal = 1;

      return 1;
    }

    if(!amcInfo->isMBM)
      break;

  } /* End of while() */

  if(verbosity == Amc_VerbosityNone_c)
    AmcPrintScheduleInformation(amcInfo);


  /* Update the subsystem that had been included in optimal system */
  {
    int best = BlockInfo.bestSystem;
    subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 
                            best);
    subSystem->takenIntoOptimal = 1;
  }

  /* Update amcInfo's optimal system */
  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
#ifdef AMC_DEBUG
    {
      Amc_SubsystemInfo_t *previousOpt = amcInfo->optimalSystem;
      Amc_SubsystemInfo_t *currentOpt  = BlockInfo.optimalSystem;

      if(!amcInfo->lowerBound) {
        if(mdd_lequal(previousOpt->satisfyStates, currentOpt->satisfyStates,
                      1, 1)) {
          fprintf(vis_stdout, "\n###AMC : We are ok.");
        }
        else {
          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
        }
      }
      else {
        if( mdd_lequal(currentOpt->satisfyStates, previousOpt->satisfyStates,
                       1, 1)) {
          fprintf(vis_stdout, "\n###AMC : We are ok.");
        }
        else {
          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
        }
      }
    }
#endif 
    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
  }
  AmcSetOptimalSystem(amcInfo, BlockInfo.optimalSystem);

  return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void AmcFreeBlock ( Amc_Info_t * amcInfo )

Function********************************************************************

Synopsis [Frees block-tearing specific data structure.]

SideEffects []

Definition at line 267 of file amcBlock.c.

{
  Amc_SubsystemInfo_t   *subSystem; 
  BlockSubsystemInfo_t  *BlockSubsystem;
  int i ;

  /* what if amc doesn't free partition */
  arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, 
                   subSystem) {
    BlockSubsystem = (BlockSubsystemInfo_t *)AmcSubsystemReadMethodSpecificData(subSystem);
    if(BlockSubsystem != NIL(BlockSubsystemInfo_t))
      FREE(BlockSubsystem);

    Amc_AmcSubsystemFree(subSystem); 
  }
  array_free(amcInfo->subSystemArray);

  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
    amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
  }

  if( amcInfo->initialStates != NIL(mdd_t)) {
    mdd_free(amcInfo->initialStates);
    amcInfo->initialStates = NIL(mdd_t);
  }

  FREE(amcInfo);

}

Here is the call graph for this function:

Here is the caller graph for this function:

static void AmcInitializeDependency	(	array_t *	subSystemArray,
		int	isMBM
	)		`[static]`

Function********************************************************************

Synopsis [Initialize dependencies between subsystems.]

SideEffects []

Definition at line 946 of file amcBlock.c.

{
  Amc_SubsystemInfo_t   *subSystem;  
  BlockSubsystemInfo_t  *BlockSubsystem;
  int   i;

  if(!isMBM) {
    int i;
    arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
      AmcSubsystemSetMethodSpecificData(subSystem, NIL(BlockSubsystemInfo_t));
    }
    return;
  }

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = ALLOC(BlockSubsystemInfo_t, 1);

    AmcSubsystemSetMethodSpecificData(subSystem, BlockSubsystem);

  }

}

Here is the caller graph for this function:

static array_t * AmcInitializeQuantifyVars ( Amc_SubsystemInfo_t * subSystem ) [static]

Function********************************************************************

Synopsis [Initialize mdd variables to be quantified. Used in under-approximation of the transition relation.]

SideEffects []

Definition at line 1136 of file amcBlock.c.

{
  array_t             *quantifyVars             = array_alloc(array_t *, 0);
  array_t             *quantifyPresentVars      = array_alloc(int, 0);
  array_t             *quantifyNextVars         = array_alloc(int, 0);
  array_t             *quantifyInputVars        = array_alloc(int, 0);
  Ntk_Network_t       *network = Fsm_FsmReadNetwork(AmcSubsystemReadFsm(subSystem));
  Ntk_Node_t          *latch;
  st_table            *vertexTable = AmcSubsystemReadVertexTable(subSystem);
  lsGen               gen;
    
  Ntk_NetworkForEachLatch(network, gen, latch) {
    char *latchName = Ntk_NodeReadName(latch); 
#ifdef AMC_DEBUG
        fprintf(vis_stdout, "\nlatch name: %s", latchName);
        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(latch));
        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
        fflush(vis_stdout);
#endif
    if(!st_lookup(vertexTable, latchName, (char **)0)) {
    
      /* Next state variables. */
      array_insert_last(int, quantifyNextVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
      /* Present state variables. */
      array_insert_last(int, quantifyPresentVars, Ntk_NodeReadMddId(latch));

    } /* end of if(st_lookup(vertexTable)) */
  } /* end of Ntk_NetworkForEachLatch */


  {
    st_table    *inputVarTable = st_init_table(st_numcmp, st_numhash);
    Ntk_Node_t  *primaryInput;
    /* Build the hash table of input vars of this subsystem. */
    /* arrayForEachItem(int, inputVarArray, i, inputVar) {
      st_insert(inputVarTable, (char *)(long)inputVar, (char *)0);
    } */

    Ntk_NetworkForEachInput(network, gen, primaryInput) {
      int       mddId = Ntk_NodeReadMddId(primaryInput);
#ifdef AMC_DEBUG
      char *inputName = Ntk_NodeReadName(primaryInput); 
      int       testMddId = Ntk_NodeReadMddId(primaryInput);
      fprintf(vis_stdout, "\nprimary input name : %s", inputName);
      fprintf(vis_stdout, "\nprimary input mdd id : %d", testMddId);
      fflush(vis_stdout);
#endif
      /* if(!st_lookup(inputVarTable, (char *)(long)mddId, (char **)0)) { */
        array_insert_last(int, quantifyInputVars, mddId);
      /* } */
    }
    st_free_table(inputVarTable);
  }

  array_insert_last(array_t *, quantifyVars, quantifyPresentVars); 
  array_insert_last(array_t *, quantifyVars, quantifyNextVars); 
  array_insert_last(array_t *, quantifyVars, quantifyInputVars); 
 
  return quantifyVars;

}

Here is the call graph for this function:

Here is the caller graph for this function:

static void AmcInitializeSchedule ( Amc_Info_t * amcInfo ) [static]

Function********************************************************************

Synopsis [Initialize scheduling information.]

SideEffects []

Definition at line 980 of file amcBlock.c.

{
  array_t                 *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t     *subSystem;  
  BlockSubsystemInfo_t    *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if(!amcInfo->isMBM)
    return;

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    if(!subSystem->takenIntoOptimal)
      AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1);
    
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

static int AmcIsEverySubsystemRescheduled ( Amc_Info_t * amcInfo ) [static]

Function********************************************************************

Synopsis [Test whether there is any subsystems to be reevaluated.]

SideEffects []

Definition at line 1011 of file amcBlock.c.

{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem;  
  BlockSubsystemInfo_t  *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if( !amcInfo->isMBM )
    return 1;

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    if( AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) )
      return 1;
    
  }
  return 0;

}

Here is the call graph for this function:

Here is the caller graph for this function:

static BlockInfo_t * AmcObtainOptimalSystemLowerBound	(	Amc_Info_t *	amcInfo,
		Ctlp_Formula_t *	formula,
		BlockInfo_t *	BlockInfo,
		int	verbosity
	)		`[static]`

Function********************************************************************

Synopsis [Obtain best subsystem that has not taken into the optimal system.]

Description [The routine is to choose a subsystem that produces a best result when proving true negative of the formula. An under-approximation of the transition is used to obtain a superset of states satisfying given formula. The best subsystem is a subsystem that produces a smallest cardinality of a superset of states satisfying given ACTL formula.]

SideEffects []

Definition at line 666 of file amcBlock.c.

{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
  mdd_t                 *initialStates;
  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
  int                   i, best = 0;
  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
  mdd_t                 *mddOne = mdd_one(mddManager);
  array_t               *quantifyVars;
  Mc_DcLevel            dcLevel;
  char                  *flagValue;
  
  /* 
   * Initial states must be set before coming into this routine.
   */
  initialStates = amcInfo->initialStates;
  if( initialStates == NIL(mdd_t) ) {
    (void)fprintf(vis_stderr, "** amc error: \n");
    return(NIL(BlockInfo_t));
  }

  /* Read in the usage of don't care level. Do not want to pass parameters. */
  flagValue = Cmd_FlagReadByName("amc_DC_level");
  if(flagValue != NIL(char)){
    dcLevel = (Mc_DcLevel) atoi(flagValue);
    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
  }
  else{
    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
    dcLevel = McDcLevelNone_c;
  }

  /*
   * Update the set of states satisfying the formula for each subsystem.
   * The process of "combining sub-systems" is equivalent of taking a 
   * "synchronous product" of multiple subsystems.
   */
  smallestStates = NIL(mdd_t);
  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
    Fsm_Fsm_t                   *combinedFsm;
    Fsm_Fairness_t              *fairCond;
    Amc_SubsystemInfo_t         *combinedSystem; 

    /* Proceed if the subsystem has not yet been taken into the optimal system. */
    if(!subSystem->takenIntoOptimal) {

      /* 
       * Combine subsystems. If optimal subsystem is NIL, duplicate the
       * subsystem.
       */
      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
                                             amcInfo->optimalSystem,
                                             subSystem);
      /* Remove input variables from the FSM */
      /*      combinedSystem = AmcClearInputVarsFromFSM(combinedSystem);*/
      combinedFsm = AmcSubsystemReadFsm(combinedSystem);

      /*
       * Use takenIntoOptimal field for the purpose of excluding current block
       * when universally quantifying variables from transition relation. 
       * Obtain lower bound of transition relation by universal quantification.
       */

      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
      combinedSystem->takenIntoOptimal = i;


      /*
       * Currently forced not to compute reachable states. This is to reduce
       * computational burden of computing it when dealing with complex
       * examples.
       */
      reachableStates = mdd_one(mddManager);
      fairStates = mdd_one(mddManager);
      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);
      careStates = mdd_dup(reachableStates);

      Ctlp_FlushStates(formula);
      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
                                                        subSystemArray, 
                                                        formula, fairStates,
                                                        fairCond, careStates,
                                                        amcInfo->lowerBound, 
                                                        quantifyVars,
                                                        (Mc_VerbosityLevel)
                                                        verbosity, dcLevel));
      {
        int x; array_t *quantifyStateVars;
        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
          array_free(quantifyStateVars); 
        }
        array_free(quantifyVars);
      }
      mdd_free(careStates); mdd_free(reachableStates); mdd_free(fairStates); 
      

      /*
       */
      if( subSystem->satisfyStates != NIL(mdd_t) ) {
        if( !(mdd_equal(satisfyStates, subSystem->satisfyStates )) &&
             (mdd_lequal(satisfyStates, subSystem->satisfyStates, 1, 1)) ) {
          /* We got a tighter approximation. */
          mdd_free(subSystem->satisfyStates);
          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
        }
      }     /* end of if( subSystem->satisfyStates != NIL(mdd_t) ) */
      else {
        /* Update subsystem when we are in level 1 of the lattice */
        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
      }

      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));


      /* Test if the formula is verified */
      {
        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
        currentErrorStates      = mdd_and(initialStates, notSatisfyStates, 1, 1);
        mdd_free(notSatisfyStates);
        mdd_free(satisfyStates);
      }

      if( verbosity == Amc_VerbosityVomit_c) {
        mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
        array_t *psVars     = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);

        fprintf(vis_stdout,
                "\n#AMC STATUS: The states satisfying the formula : %10g",
                mdd_count_onset(mddMgr, combinedSystem->satisfyStates, psVars ) );
        fflush(vis_stdout);
      }

      if ( !mdd_is_tautology(currentErrorStates, 0) ) {
        array_t *careStatesArray;

        /* Verified the formula FALSE!! */
        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1;
        amcInfo->amcAnswer = Amc_Verified_False_c;
        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));


        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);

        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem);

        {
          /* Temporarily stay here until the damn thing becomes visible. */
          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
          mcOptions->useMore = FALSE;
          mcOptions->fwdBwd = McFwd_c;
          mcOptions->reduceFsm = FALSE;
          mcOptions->printInputs = FALSE;
          mcOptions->simFormat = FALSE;
          mcOptions->verbosityLevel = McVerbosityNone_c;
          mcOptions->dbgLevel = McDbgLevelMinVerbose_c;
          mcOptions->dcLevel   = McDcLevelNone_c;
          mcOptions->ctlFile = NIL(FILE);
          mcOptions->debugFile = NIL(FILE);

          careStatesArray = array_alloc(mdd_t *, 0);
          array_insert(mdd_t *, careStatesArray, 0, mddOne);
          fprintf(vis_stdout, "\n");
          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
                            combinedSystem->fsm, careStatesArray);
          array_free(careStatesArray);
          FREE(mcOptions);
        }
        mdd_free(mddOne);
        Amc_AmcSubsystemFree(combinedSystem);
        Ctlp_FlushStates(formula);

        return BlockInfo;

      }else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
        /* The formula is verified true!! */
        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1; 
        amcInfo->amcAnswer = Amc_Verified_True_c;
        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));


        if(currentErrorStates != NIL(mdd_t))
          mdd_free(currentErrorStates); 
        if(smallestStates != NIL(mdd_t))
          mdd_free(smallestStates);
        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem); 

        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
        Ctlp_FlushStates(formula);

        return BlockInfo;
      }

      mdd_free(currentErrorStates);


      /*
       * Choose a subsystem that produces smallest satisfying states.
       */
      if( smallestStates == NIL(mdd_t) ||
          mdd_count_onset(mddManager, subSystem->satisfyStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <= 
          mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {
        /*
         * Found locally optimal subsystem. 
         * Free smallest-error-state, best combined system so far. 
         * Update smallest-error-states and best combined system. 
         */
        if( smallestStates != NIL(mdd_t) ) mdd_free(smallestStates);

        smallestStates = mdd_dup(subSystem->satisfyStates);

        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
          Amc_AmcSubsystemFree(bestCombinedSystem);
          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
        }
        bestCombinedSystem = combinedSystem; 
        best = i;
      }

      else { /* Free combined system, current error states */
        Amc_AmcSubsystemFree(combinedSystem); combinedSystem = NIL(Amc_SubsystemInfo_t);
      }

    } /* end of if(!takenIntoOptimal) */

  } /* end of arrayForEachItem(subSystemArray) */

  mdd_free(smallestStates);

  /* 
   * Flush formula that was kept in last iteration. Update Block Info.  
   */
  Ctlp_FlushStates(formula);

  /*
   * Update optimal system BlockInfo->optimalSystem. BlockInfo is a temporary 
   * storage that survive through single level of the lattice.
   */
  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
  }
  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);

  /* Set best system. */
  AmcBlockSetBestSystem(BlockInfo, best);
  mdd_free(mddOne);

  return BlockInfo;

}

Here is the call graph for this function:

Here is the caller graph for this function:

static BlockInfo_t * AmcObtainOptimalSystemUpperBound	(	Amc_Info_t *	amcInfo,
		Ctlp_Formula_t *	formula,
		BlockInfo_t *	BlockInfo,
		int	verbosity
	)		`[static]`

AutomaticStart

Function********************************************************************

Synopsis [Obtain best subsystem that has not taken into the optimal system.]

Description [The routine is used to prove true positive of given ACTL formula. An over-approximation of transition relation is used. Over-approximation of the transition relation is obtained by simply replacing the subsystems not in consideration into tautology. We are adding more behavior into the system by preserving only the subset of subsystems(subFSMs). We call this procedure a block-tearing abstraction. We do not abstract initial states in any sense.

The best subsystem is chosen from those subsystems that has not yet been taken into the optimal system. A subsystem that produces best result is determined by the smallest error states. An error states are defined as; Error States = (Initial States) - (Subset of states satisfying given ACTL formula) For each subsystem, a subset of states satisfying given ACTL formula is computed by using an over-approximation of the transition relation obtained from the subsystem. The routine picks a subsystem whose corresponding error states are cardinality wise minimal.

The optimal system is the collection of subsystems that were chosen as the best subsystem in each iteration. A function call to this routine is regarded as a single iteration when "machine by machine" refinement is turned OFF. These subsystems are synchronously combined to form a optimal system.

Once the best subsystem is chosen(from the set of subsystems that has not been combined into the optimal system), an initial states are updated with an error states. An error states are defined as; (Initial States) - (Subset of states satisfying given ACTL formula)

A more aggressive update of initial states may also be performed. If we denote a subset of states satisfying given ACTL formula as Sat^L(). New Initial States = (Old Initial States) - {i}(Sat^L_i() The routine currently does not attempt above aggressive approach. The routine update initial state as; New Initial States = (Old Initial States) - Sat^L_{Best i}().

]

SideEffects []

Definition at line 351 of file amcBlock.c.

{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
  mdd_t                 *initialStates;
  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
  int                   i, best = 0;
  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
  mdd_t                 *mddOne = mdd_one(mddManager);
  array_t               *quantifyVars;
  Mc_DcLevel            dcLevel;
  char  *flagValue;


  /* 
   * Initial states must be set before coming into this routine.
   */
  initialStates = amcInfo->initialStates;
  if( initialStates == NIL(mdd_t) ) {
    (void)fprintf(vis_stderr, "** amc error: \n");
    return(NIL(BlockInfo_t));
  }
 
  /* Read in the usage of don't care level */
  flagValue = Cmd_FlagReadByName("amc_DC_level");
  if(flagValue != NIL(char)){
    dcLevel = (Mc_DcLevel) atoi(flagValue); 
    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
  }
  else{
    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
    dcLevel = McDcLevelNone_c; 
  }

  /*
   * Update the set of states satisfying the formula for each sub-systems.
   * The process of "combining sub-systems" is equivalent of taking a 
   * "synchronous product" of multiple sub-subsystems.
   */
  smallestStates = NIL(mdd_t);
  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
    Fsm_Fsm_t                   *combinedFsm;
    Fsm_Fairness_t              *fairCond;
    Amc_SubsystemInfo_t         *combinedSystem; 

    /* Proceed if the subsystem had not yet been taken into the optimal system. */
    if(!subSystem->takenIntoOptimal) {

      /* 
       * Combine subsystems. If optimal subsystem is NIL, duplicate the
       * subsystem.
       */  
      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
                                             amcInfo->optimalSystem,
                                             subSystem);
      combinedFsm = AmcSubsystemReadFsm(combinedSystem);

      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
      
      /* 
       * Currently forced not to compute reachable states. This is to reduce
       * computational overhead of computing it when dealing with complex
       * examples.
       */
      reachableStates = mdd_one(mddManager);
      fairStates = mdd_one(mddManager);
      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);


      /* Obtain new care set from fan-in systems */
      careStates = mdd_dup(reachableStates);

      Ctlp_FlushStates(formula);
      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
                                                        subSystemArray, 
                                                        formula, fairStates,
                                                        fairCond,
                                                        careStates,
                                                        amcInfo->lowerBound, 
                                                        quantifyVars,
                                                        /*NIL(array_t),*/
                                                        (Mc_VerbosityLevel)
                                                        verbosity, dcLevel));

      {
        int x; array_t *quantifyStateVars;
        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
          array_free(quantifyStateVars); 
        }
        array_free(quantifyVars);
      }
      /* Free */
      mdd_free(careStates);
      mdd_free(reachableStates); mdd_free(fairStates); 
      

      /* 
       * Update the set of states satisfying the formula for each subsystems
       * when newly computed states are tighter than the one already stored.
       * Notice, "satisfySates" holds the set of states satisfying the formula
       * computed with the combined_system(optimal_system || current_subsystem). 
       * 
       */
      if( subSystem->satisfyStates != NIL(mdd_t) ) {

        if( !(mdd_equal(subSystem->satisfyStates, satisfyStates )) &&
            (mdd_lequal(subSystem->satisfyStates, satisfyStates, 1, 1)) ) {
          /* We got a tighter approximation. */
          mdd_free(subSystem->satisfyStates);
          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
        }
         
      }     
      else {
        /* We are in the first level of the lattice */
        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));

      }

      /* Update the set of states satisfying the formula for the combined_system. */
      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));


      if( verbosity == Amc_VerbosityVomit_c) {
         mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
         array_t     *psVars = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);

         fprintf(vis_stdout, "\n#AMC STATUS: The states satisfying the formula : %10g",
                        mdd_count_onset(  mddMgr, combinedSystem->satisfyStates, psVars ) );
         fflush(vis_stdout);
       }

      /* 
       * Check whether the formula evaluates to TRUE. 
       */
      { 
        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
        currentErrorStates = mdd_and(initialStates, notSatisfyStates, 1, 1);
        mdd_free(notSatisfyStates);
        mdd_free(satisfyStates);
      }

      if ( mdd_is_tautology(currentErrorStates, 0) ) { 
        /* The formula is verified TRUE!! */

        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1; 
        amcInfo->amcAnswer = Amc_Verified_True_c;
        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));

        if(currentErrorStates != NIL(mdd_t))
          mdd_free(currentErrorStates); 
        if(smallestStates != NIL(mdd_t))
          mdd_free(smallestStates);
        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem); 

        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
        Ctlp_FlushStates(formula);

        return BlockInfo;
      } /* end of if */
      else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
        /* The formula is verified FALSE!! */
        array_t *careStatesArray;

        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1;
        amcInfo->amcAnswer = Amc_Verified_False_c;
        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));

        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);

        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem);

        {
          /* Temporarily stay here until the damn thing becomes visible. */
          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
          mcOptions->useMore = FALSE;
          mcOptions->fwdBwd = McFwd_c;
          mcOptions->reduceFsm = FALSE;
          mcOptions->printInputs = FALSE;
          mcOptions->simFormat = FALSE;
          mcOptions->verbosityLevel = McVerbosityNone_c;
          mcOptions->dbgLevel = McDbgLevelMin_c;
          mcOptions->dcLevel   = McDcLevelNone_c;
          mcOptions->ctlFile = NIL(FILE);
          mcOptions->debugFile = NIL(FILE);

          careStatesArray = array_alloc(mdd_t *, 0);
          array_insert(mdd_t *, careStatesArray, 0, mddOne);
          fprintf(vis_stdout, "\n");
          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
                            combinedSystem->fsm, careStatesArray);
          array_free(careStatesArray);
          FREE(mcOptions);
        }
        mdd_free(mddOne);
        Amc_AmcSubsystemFree(combinedSystem);
        Ctlp_FlushStates(formula);

        return BlockInfo;       
      }

      /* 
       * Get the locally optimal subsystem by choosing a subsystem that produces
       * smallest error states.
       */
      if( smallestStates == NIL(mdd_t) ||
         mdd_count_onset(mddManager, currentErrorStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <=
         mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {

        if( smallestStates != NIL(mdd_t) )
          mdd_free(smallestStates);

        smallestStates = currentErrorStates;

        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
          Amc_AmcSubsystemFree(bestCombinedSystem);
          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
        }
        bestCombinedSystem = combinedSystem; 
        best = i;
      }

      else { /* Free combined system, current error states */
        Amc_AmcSubsystemFree(combinedSystem);
        combinedSystem = NIL(Amc_SubsystemInfo_t);
        mdd_free(currentErrorStates); 
      }

    
    } /* end of if(!takenIntoOptimal) */

  } /* end of arrayForEachItem(subSystemArray) */


  /* 
   * Flush the formula that was kept in last iteration.
   * Update Block Info.  
   */
  Ctlp_FlushStates(formula);

  /* Update the inital states */
  {
    mdd_t *initialStates;
    if((initialStates = AmcReadInitialStates(amcInfo)) != NIL(mdd_t))
      mdd_free(initialStates);
    AmcSetInitialStates(amcInfo, smallestStates);
  }

  if( verbosity == Amc_VerbositySpit_c ) {
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(bestCombinedSystem->fsm);
    array_t     *psVars = Fsm_FsmReadPresentStateVars(bestCombinedSystem->fsm);

    fprintf(vis_stdout, "\n#AMC : The BDD size of the states satisfying the formula : %d", 
                                  mdd_size(bestCombinedSystem->satisfyStates) );
    fprintf(vis_stdout, "\n#AMC : The cardinality of the states satisfying the formula : %10g ",
                          mdd_count_onset(  mddMgr, bestCombinedSystem->satisfyStates, psVars ) );
    fprintf(vis_stdout, "\n#AMC : The BDD size of the states new initial states : %d",
                                  mdd_size(smallestStates) );
    fprintf(vis_stdout, "\n#AMC : The cardinality of the new initial states : %10g ",
                          mdd_count_onset(  mddMgr, smallestStates, psVars ) );
  }


  /* 
   * Update the optimal system BlockInfo->optimalSystem. BlockInfo is a temporary 
   * storage that survive through single level of the lattice.
   */
  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
  }
  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);

  /* Set the best system. */
  AmcBlockSetBestSystem(BlockInfo, best);

  mdd_free(mddOne);
  
  return BlockInfo;

}

Here is the call graph for this function:

Here is the caller graph for this function:

static void AmcPrintScheduleInformation ( Amc_Info_t * amcInfo ) [static]

Function********************************************************************

Synopsis [Print schedule information.]

SideEffects []

Definition at line 1042 of file amcBlock.c.

{
  array_t                 *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t     *subSystem;  
  BlockSubsystemInfo_t    *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if(!amcInfo->isMBM)
    return;

  fprintf(vis_stdout, "\nSchedule information : ");

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    fprintf(vis_stdout, " %d ", AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) );
    
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

char rcsid [] UNUSED = "$Id: amcBlock.c,v 1.35 2005/04/25 20:24:53 fabio Exp $" [static]

CFile***********************************************************************

FileName [amcBlock.c]

PackageName [amc]

Synopsis [Implementation of the block-tearing abstraction.]

Author [Woohyuk Lee]

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 amcBlock.c.

src/amc/amcBlock.c File Reference

Data Structures

Typedefs

Functions

Variables

Typedef Documentation

Function Documentation

Variable Documentation