d6/dd0/mcCmd_8c_source.html

00001
00051 #include "ctlpInt.h"
00052 #include "grab.h"
00053 #include "puresat.h"
00054 #include "mcInt.h"
00055
00056
00057 /*---------------------------------------------------------------------------*/
00058 /* Constant declarations                                                     */
00059 /*---------------------------------------------------------------------------*/
00060
00061 /*---------------------------------------------------------------------------*/
00062 /* Stucture declarations                                                     */
00063 /*---------------------------------------------------------------------------*/
00064
00065 /*---------------------------------------------------------------------------*/
00066 /* Type declarations                                                         */
00067 /*---------------------------------------------------------------------------*/
00068
00069 /*---------------------------------------------------------------------------*/
00070 /* Variable declarations                                                     */
00071 /*---------------------------------------------------------------------------*/
00072
00073 #ifndef lint
00074 static char rcsid[] UNUSED = "$Id: mcCmd.c,v 1.27 2009/04/11 01:43:30 fabio Exp $";
00075 #endif
00076
00077 /*---------------------------------------------------------------------------*/
00078 /* Macro declarations                                                        */
00079 /*---------------------------------------------------------------------------*/
00080
00081 /*---------------------------------------------------------------------------*/
00082 /* Variable declarations                                                     */
00083 /*---------------------------------------------------------------------------*/
00084
00085 static jmp_buf timeOutEnv;
00086 static int mcTimeOut;           /* timeout value */
00087 static long alarmLapTime;       /* starting CPU time for timeout */
00088
00091 /*---------------------------------------------------------------------------*/
00092 /* Static function prototypes                                                */
00093 /*---------------------------------------------------------------------------*/
00094
00095 static int CommandMc(Hrc_Manager_t **hmgr, int argc, char **argv);
00096 static McOptions_t * ParseMcOptions(int argc, char **argv);
00097 static int CommandLe(Hrc_Manager_t **hmgr, int argc, char **argv);
00098 static McOptions_t * ParseLeOptions(int argc, char **argv);
00099 static int CommandInv(Hrc_Manager_t **hmgr, int argc, char **argv);
00100 static McOptions_t * ParseInvarOptions(int argc, char **argv);
00101 static void TimeOutHandle(void);
00102 static int UpdateResultArray(mdd_t *reachableStates, array_t *invarStatesArray, int *resultArray);
00103 static void PrintInvPassFail(array_t *invarFormulaArray, int *resultArray);
00104
00107 /*---------------------------------------------------------------------------*/
00108 /* Definition of exported functions                                          */
00109 /*---------------------------------------------------------------------------*/
00110
00111
00119 void
00120 Mc_Init(void)
00121 {
00122   Cmd_CommandAdd("model_check", CommandMc, /* doesn't changes_network */ 0);
00123   Cmd_CommandAdd("check_invariant", CommandInv, /* doesn't changes_network */ 0);
00124   Cmd_CommandAdd("lang_empty", CommandLe, /* doesn't changes_network */ 0);
00125   Cmd_CommandAdd("_init_state_formula", McCommandInitState, /* doesn't changes_network */ 0);
00126 }
00127
00128
00136 void
00137 Mc_End(void)
00138 {
00139 }
00140
00141 /*---------------------------------------------------------------------------*/
00142 /* Definition of internal functions                                          */
00143 /*---------------------------------------------------------------------------*/
00144
00145
00146 /*---------------------------------------------------------------------------*/
00147 /* Definition of static functions                                            */
00148 /*---------------------------------------------------------------------------*/
00149
00150
00538 static int
00539 CommandMc(
00540   Hrc_Manager_t **hmgr,
00541   int argc,
00542   char **argv)
00543 {
00544  /* options */
00545   McOptions_t         *options;
00546   Mc_VerbosityLevel   verbosity;
00547   Mc_DcLevel          dcLevel;
00548   FILE                *ctlFile;
00549   int                 timeOutPeriod     = 0;
00550   Mc_FwdBwdAnalysis   traversalDirection;
00551   int                 buildOnionRings   = 0;
00552   FILE                *guideFile;
00553   FILE                *systemFile;
00554   Mc_GuidedSearch_t   guidedSearchType  = Mc_None_c;
00555   Ctlp_FormulaArray_t *hintsArray       = NIL(Fsm_HintsArray_t);
00556   array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
00557   st_table            *systemVarBddIdTable;
00558   boolean             noShare           = 0;
00559   Mc_GSHScheduleType  GSHschedule;
00560   boolean             checkVacuity;
00561   boolean             performCoverageHoskote;
00562   boolean             performCoverageImproved;
00563
00564   /* CTL formulae */
00565   array_t *ctlArray;
00566   array_t *ctlNormalFormulaArray;
00567   int i;
00568   int numFormulae;
00569   /* FSM, network and image */
00570   Fsm_Fsm_t       *totalFsm = NIL(Fsm_Fsm_t);
00571   Fsm_Fsm_t       *modelFsm = NIL(Fsm_Fsm_t);
00572   Fsm_Fsm_t       *reducedFsm = NIL(Fsm_Fsm_t);
00573   Ntk_Network_t   *network;
00574   mdd_t           *modelCareStates = NIL(mdd_t);
00575   array_t         *modelCareStatesArray = NIL(array_t);
00576   mdd_t           *modelInitialStates;
00577   mdd_t           *fairStates;
00578   Fsm_Fairness_t  *fairCond;
00579   mdd_manager     *mddMgr;
00580   array_t         *bddIdArray;
00581   Img_ImageInfo_t *imageInfo;
00582   Mc_EarlyTermination_t *earlyTermination;
00583   /* Coverage estimation */
00584   mdd_t           *totalcoveredstates = NIL(mdd_t);
00585   array_t         *signalTypeList = array_alloc(int,0);
00586   array_t         *signalList = array_alloc(char *,0);
00587   array_t         *statesCoveredList = array_alloc(mdd_t *,0);
00588   array_t         *newCoveredStatesList = array_alloc(mdd_t *,0);
00589   array_t         *statesToRemoveList = array_alloc(mdd_t *,0);
00590
00591   /* Early termination is only partially implemented right now.  It needs
00592      distribution over all operators, including limited cases of temporal
00593      operators.  That should be relatively easy to implement. */
00594
00595   /* time keeping */
00596   long totalInitialTime; /* for model checking */
00597   long initialTime, finalTime; /* for model checking */
00598
00599   error_init();
00600   Img_ResetNumberOfImageComputation(Img_Both_c);
00601
00602   /* read options */
00603   if (!(options = ParseMcOptions(argc, argv))) {
00604     return 1;
00605   }
00606   verbosity = McOptionsReadVerbosityLevel(options);
00607   dcLevel = McOptionsReadDcLevel(options);
00608   ctlFile = McOptionsReadCtlFile(options);
00609   timeOutPeriod = McOptionsReadTimeOutPeriod(options);
00610   traversalDirection = McOptionsReadTraversalDirection(options);
00611   buildOnionRings =
00612     (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
00613   noShare = McOptionsReadUseFormulaTree(options);
00614   GSHschedule = McOptionsReadSchedule(options);
00615   checkVacuity = McOptionsReadVacuityDetect(options);
00616    /* for the command mc -C foo.ctl */
00617   performCoverageHoskote = McOptionsReadCoverageHoskote(options);
00618   /* for the command mc -I foo.ctl */
00619   performCoverageImproved = McOptionsReadCoverageImproved(options);
00620
00621   /* Check for incompatible options and do some option-specific
00622    * intializations.
00623    */
00624
00625   if (traversalDirection == McFwd_c) {
00626     if (checkVacuity) {
00627       fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n");
00628       McOptionsFree(options);
00629       return 1;
00630     }
00631     if (performCoverageHoskote || performCoverageImproved) {
00632       fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n");
00633       McOptionsFree(options);
00634       return 1;
00635     }
00636   }
00637
00638   if (checkVacuity) {
00639     if (performCoverageHoskote || performCoverageImproved) {
00640       fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n");
00641       McOptionsFree(options);
00642       return 1;
00643     }
00644   }
00645
00646   guideFile =  McOptionsReadGuideFile(options);
00647
00648   if(guideFile != NIL(FILE) ){
00649     guidedSearchType = Mc_ReadGuidedSearchType();
00650     if(guidedSearchType == Mc_None_c){  /* illegal setting */
00651       fprintf(vis_stderr, "** mc error: Unknown  hint type\n");
00652       fclose(guideFile);
00653       McOptionsFree(options);
00654       return 1;
00655     }
00656
00657     if(traversalDirection == McFwd_c){  /* illegal combination */
00658       fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n");
00659       fclose(guideFile);
00660       McOptionsFree(options);
00661       return 1;
00662     }
00663
00664     if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
00665        Img_UserSpecifiedMethod() != Img_Monolithic_c &&
00666        Img_UserSpecifiedMethod() != Img_Mlp_c){
00667       fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n");
00668       fclose(guideFile);
00669       McOptionsFree(options);
00670       return 1;
00671     }
00672
00673     hintsArray = Mc_ReadHints(guideFile);
00674     fclose(guideFile); guideFile = NIL(FILE);
00675     if( hintsArray == NIL(array_t) ){
00676       McOptionsFree(options);
00677       return 1;
00678     }
00679
00680   } /* if guided search */
00681
00682   /* If don't-cares are used, -r implies -c.  Note that the satisfying
00683      sets of a subformula are only in terms of propositions therein
00684      and their cone of influence.  Hence, we can share satisfying sets
00685      among formulae.  I don't quite understand what the problem with
00686      don't-cares is (RB) */
00687   if (McOptionsReadReduceFsm(options))
00688     if (dcLevel != McDcLevelNone_c)
00689       McOptionsSetUseFormulaTree(options, TRUE);
00690
00691   if (traversalDirection == McFwd_c &&
00692       McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
00693     McOptionsSetDbgLevel(options, McDbgLevelNone_c);
00694     (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n");
00695   }
00696
00697   /* Read CTL formulae */
00698   ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile);
00699   fclose(ctlFile); ctlFile = NIL(FILE);
00700   if (ctlArray == NIL(array_t)) {
00701     (void) fprintf(vis_stderr,
00702                    "** mc error: error in parsing formulas from file\n");
00703     McOptionsFree(options);
00704     return 1;
00705   }
00706
00707   /* read network */
00708   network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
00709   if (network == NIL(Ntk_Network_t)) {
00710     fprintf(vis_stdout, "%s\n", error_string());
00711     error_init();
00712     Ctlp_FormulaArrayFree(ctlArray);
00713     McOptionsFree(options);
00714     return 1;
00715   }
00716
00717   /* read fsm */
00718   totalFsm = Fsm_NetworkReadOrCreateFsm(network);
00719   if (totalFsm == NIL(Fsm_Fsm_t)) {
00720     fprintf(vis_stdout, "%s\n", error_string());
00721     error_init();
00722     Ctlp_FormulaArrayFree(ctlArray);
00723     McOptionsFree(options);
00724     return 1;
00725   }
00726
00727   /* Assign variables to system if doing FAFW */
00728   systemVarBddIdTable = NIL(st_table);
00729   systemFile = McOptionsReadSystemFile(options);
00730   if (systemFile != NIL(FILE)) {
00731     systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
00732     fclose(systemFile); systemFile = NIL(FILE);
00733     if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */
00734       Ctlp_FormulaArrayFree(ctlArray);
00735       McOptionsFree(options);
00736       return 1;
00737     }
00738   } /* if FAFW */
00739
00740   if(options->FAFWFlag && systemVarBddIdTable == 0) {
00741     systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
00742   }
00743
00744   if (verbosity > McVerbosityNone_c)
00745     totalInitialTime = util_cpu_time();
00746   else /* to remove uninitialized variable warning */
00747     totalInitialTime = 0;
00748
00749   if(traversalDirection == McFwd_c){
00750     mdd_t *totalInitialStates;
00751     double nInitialStates;
00752
00753     totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm);
00754     nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm),
00755                                      totalInitialStates,
00756                                      Fsm_FsmReadPresentStateVars(totalFsm));
00757     mdd_free(totalInitialStates);
00758
00759     /* If the number of initial states is only one, we can use both
00760      * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE),
00761      * however, if we have multiple initial states, we should use
00762      * p0 ^ !f == FALSE.
00763      */
00764     ctlNormalFormulaArray =
00765       Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0),
00766                                         noShare);
00767     /* end conversion for forward traversal */
00768   } else if (noShare) { /* conversion for backward, no sharing */
00769     ctlNormalFormulaArray =
00770       Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
00771   }else{ /* conversion for backward, with sharing */
00772     /* Note that converting to DAG after converting to existential form would
00773        lead to more sharing, but it cannot be done since equal subformula that
00774        are converted from different formulae need different pointers back to
00775        their originals */
00776     if (checkVacuity) {
00777       ctlNormalFormulaArray =
00778         Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
00779     }
00780     else {
00781       array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray );
00782       array_free( ctlArray );
00783       ctlArray = temp;
00784       ctlNormalFormulaArray =
00785         Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray);
00786     }
00787   }
00788   /* At this point, ctlNormalFormulaArray contains the formulas that are
00789      actually going to be checked, and ctlArray contains the formulas from
00790      which the conversion has been done.  Both need to be kept around until the
00791      end, for debugging purposes. */
00792
00793   numFormulae = array_n(ctlNormalFormulaArray);
00794
00795   /* time out */
00796   if (timeOutPeriod > 0) {
00797     /* Set the static variables used by the signal handler. */
00798     mcTimeOut = timeOutPeriod;
00799     alarmLapTime = util_cpu_ctime();
00800     (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
00801     (void) alarm(timeOutPeriod);
00802     if (setjmp(timeOutEnv) > 0) {
00803       (void) fprintf(vis_stdout,
00804                 "# MC: timeout occurred after %d seconds.\n", timeOutPeriod);
00805       (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n");
00806       if (verbosity > McVerbosityNone_c) {
00807         fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n",
00808                 Img_GetNumberOfImageComputation(Img_Forward_c),
00809                 Img_GetNumberOfImageComputation(Img_Backward_c));
00810       }
00811       alarm(0);
00812       return 1;
00813     }
00814   }
00815
00816   /* Create reduced fsm, if necessary */
00817   if (!McOptionsReadReduceFsm(options)){
00818     /* We want to minimize only when "-r" option is not specified */
00819     /* reduceFsm would be NIL, if there is no reduction observed */
00820     assert (reducedFsm == NIL(Fsm_Fsm_t));
00821     reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
00822     if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) {
00823       mddMgr = Fsm_FsmReadMddManager(reducedFsm);
00824       bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
00825                    Fsm_FsmReadPresentStateVars(reducedFsm));
00826       (void)fprintf(vis_stdout,"Local system includes ");
00827       (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
00828                     array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
00829                     array_n(bddIdArray));
00830       array_free(bddIdArray);
00831     }
00832   }
00833
00834   /************** for all formulae **********************************/
00835   for(i = 0; i < numFormulae; i++) {
00836     int nImgComps, nPreComps;
00837     boolean result;
00838     Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
00839                                              ctlNormalFormulaArray, i);
00840
00841     modelFsm = NIL(Fsm_Fsm_t);
00842
00843     /* do a check */
00844     if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
00845       (void) fprintf(vis_stdout,
00846                      "** mc error: error in parsing Atomic Formula:\n%s\n",
00847                      error_string());
00848       error_init();
00849       Ctlp_FormulaFree(ctlFormula);
00850       continue;
00851     }
00852
00853     /* Create reduced fsm */
00854     if (McOptionsReadReduceFsm(options)) {
00855       /* We have not done top level reduction. */
00856       /* Using the same variable reducedFsm here   */
00857       array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
00858
00859       assert(reducedFsm == NIL(Fsm_Fsm_t));
00860       array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula);
00861       reducedFsm = McConstructReducedFsm(network, oneFormulaArray);
00862       array_free(oneFormulaArray);
00863
00864       if (reducedFsm && verbosity != McVerbosityNone_c) {
00865         mddMgr = Fsm_FsmReadMddManager(reducedFsm);
00866         bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
00867                        Fsm_FsmReadPresentStateVars(reducedFsm));
00868         (void)fprintf(vis_stdout,"Local system includes ");
00869         (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
00870                       array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
00871                       array_n(bddIdArray));
00872         array_free(bddIdArray);
00873       }
00874     }/* if readreducefsm */
00875
00876     /* Let us see if we got any reduction via top level or via "-r" */
00877     if (reducedFsm == NIL(Fsm_Fsm_t))
00878       modelFsm = totalFsm; /* no reduction */
00879     else
00880       modelFsm = reducedFsm; /* some reduction at some point */
00881
00882     /* compute initial states */
00883     modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
00884     if (modelInitialStates == NIL(mdd_t)) {
00885       int j;
00886       (void) fprintf(vis_stdout,
00887       "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n",
00888                      error_string());
00889       if (modelFsm != totalFsm)
00890         Fsm_FsmFree(reducedFsm);
00891
00892       alarm(0);
00893
00894       for(j = i; j < numFormulae; j++)
00895         Ctlp_FormulaFree(
00896           array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
00897       array_free( ctlNormalFormulaArray );
00898
00899       Ctlp_FormulaArrayFree( ctlArray );
00900
00901       McOptionsFree(options);
00902
00903       return 1;
00904     }
00905
00906     earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
00907
00908     if(hintsArray != NIL(Ctlp_FormulaArray_t)) {
00909       hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
00910       if( hintsStatesArray == NIL(array_t) ||
00911           (guidedSearchType == Mc_Global_c &&
00912            Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) {
00913         int j;
00914
00915         if( guidedSearchType == Mc_Global_c &&
00916             Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)
00917           fprintf(vis_stderr, "** mc error: global hints incompatible with "
00918                   "mixed formulae\n");
00919
00920         Mc_EarlyTerminationFree(earlyTermination);
00921         mdd_free(modelInitialStates);
00922         if (modelFsm != totalFsm)
00923           Fsm_FsmFree(reducedFsm);
00924         alarm(0);
00925         for(j = i; j < numFormulae; j++)
00926           Ctlp_FormulaFree(
00927             array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
00928         array_free( ctlNormalFormulaArray );
00929         Ctlp_FormulaArrayFree( ctlArray );
00930         McOptionsFree(options);
00931         return 1;
00932       } /* problem with hints */
00933     } /* hints exist */
00934
00935     /* stats */
00936     if (verbosity > McVerbosityNone_c) {
00937       initialTime = util_cpu_time();
00938       nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
00939       nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
00940     } else { /* to remove uninitialized variable warnings */
00941       initialTime = 0;
00942       nImgComps = 0;
00943       nPreComps = 0;
00944     }
00945     mddMgr = Fsm_FsmReadMddManager(modelFsm);
00946
00947     /* compute don't cares. */
00948     if (modelCareStatesArray == NIL(array_t)) {
00949       long iTime; /* starting time for reachability analysis */
00950       if (verbosity > McVerbosityNone_c && i == 0)
00951         iTime = util_cpu_time();
00952       else /* to remove uninitialized variable warnings */
00953         iTime = 0;
00954
00955       /* ardc */
00956       if (dcLevel == McDcLevelArdc_c) {
00957         Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options);
00958
00959         modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates(
00960           modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
00961         if (verbosity > McVerbosityNone_c && i == 0)
00962           Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime);
00963
00964       /* rch dc */
00965       } else if (dcLevel >= McDcLevelRch_c) {
00966         modelCareStates =
00967           Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0,
00968                                         Fsm_Rch_Default_c, 0, 0,
00969                                         NIL(array_t), FALSE, NIL(array_t));
00970         if (verbosity > McVerbosityNone_c && i == 0) {
00971           Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime,
00972                                           Fsm_Rch_Default_c);
00973         }
00974
00975         modelCareStatesArray = array_alloc(mdd_t *, 0);
00976         array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
00977       } else {
00978         modelCareStates = mdd_one(mddMgr);
00979         modelCareStatesArray = array_alloc(mdd_t *, 0);
00980         array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
00981       }
00982     }
00983
00984     Fsm_MinimizeTransitionRelationWithReachabilityInfo(
00985       modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c,
00986       verbosity > 1);
00987
00988     /* fairness conditions */
00989     fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
00990                                           verbosity, dcLevel, GSHschedule,
00991                                           McBwd_c, FALSE);
00992     fairCond = Fsm_FsmReadFairnessConstraint(modelFsm);
00993
00994     if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) {
00995       (void)fprintf(vis_stdout,
00996                     "** mc warning: There are no fair initial states\n");
00997     }
00998     else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) {
00999       (void)fprintf(vis_stdout,
01000                     "** mc warning: Some initial states are not fair\n");
01001     }
01002
01003     /* some user feedback */
01004     if (verbosity != McVerbosityNone_c) {
01005       (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1);
01006       Ctlp_FormulaPrint(vis_stdout,
01007                         Ctlp_FormulaReadOriginalFormula(ctlFormula));
01008       (void)fprintf (vis_stdout, "\n");
01009       if (traversalDirection == McFwd_c) {
01010         (void)fprintf(vis_stdout, "Forward formula : ");
01011         Ctlp_FormulaPrint(vis_stdout, ctlFormula);
01012         (void)fprintf(vis_stdout, "\n");
01013       }
01014     }
01015
01016     /************** the actual computation **********************************/
01017     if (checkVacuity) {
01018       McVacuityDetection(modelFsm, ctlFormula, i,
01019                          fairStates, fairCond, modelCareStatesArray,
01020                          earlyTermination, hintsStatesArray,
01021                          guidedSearchType, modelInitialStates,
01022                          options);
01023     }
01024     else { /* Normal Model Checking */
01025       mdd_t *ctlFormulaStates =
01026         Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
01027                               fairCond, modelCareStatesArray,
01028                               earlyTermination, hintsStatesArray,
01029                               guidedSearchType, verbosity, dcLevel,
01030                               buildOnionRings, GSHschedule);
01031
01032       McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond,
01033                          modelCareStatesArray, earlyTermination,
01034                          hintsStatesArray, guidedSearchType, verbosity,
01035                          dcLevel, buildOnionRings, GSHschedule,
01036                          traversalDirection, modelInitialStates,
01037                          ctlFormulaStates, &totalcoveredstates,
01038                          signalTypeList, signalList, statesCoveredList,
01039                          newCoveredStatesList, statesToRemoveList,
01040                          performCoverageHoskote, performCoverageImproved);
01041
01042       Mc_EarlyTerminationFree(earlyTermination);
01043       if(hintsStatesArray != NIL(array_t))
01044         mdd_array_free(hintsStatesArray);
01045       /* Set up things for possible FAFW analysis of counterexample. */
01046       Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
01047       Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
01048       /* user feedback on succes/fail */
01049       result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
01050                                ctlFormula, ctlFormulaStates,
01051                                modelInitialStates, modelCareStatesArray,
01052                                options, verbosity);
01053       Fsm_FsmSetFAFWFlag(modelFsm, 0);
01054       Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL);
01055       mdd_free(ctlFormulaStates);
01056     }
01057
01058     if (verbosity > McVerbosityNone_c) {
01059       finalTime = util_cpu_time();
01060       fprintf(vis_stdout, "-- mc time = %10g\n",
01061         (double)(finalTime - initialTime) / 1000.0);
01062       fprintf(vis_stdout,
01063               "-- %d image computations and %d preimage computations\n",
01064               Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
01065               Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
01066     }
01067     mdd_free(modelInitialStates);
01068     mdd_free(fairStates);
01069     Ctlp_FormulaFree(ctlFormula);
01070
01071     if ((McOptionsReadReduceFsm(options)) &&
01072         (reducedFsm != NIL(Fsm_Fsm_t))) {
01073       /*
01074       ** We need to free the reducedFsm only if it was created under "-r"
01075       ** option and was non-NIL.
01076       */
01077       Fsm_FsmFree(reducedFsm);
01078       reducedFsm = NIL(Fsm_Fsm_t);
01079       modelFsm = NIL(Fsm_Fsm_t);
01080       if (modelCareStates) {
01081         mdd_array_free(modelCareStatesArray);
01082         modelCareStates = NIL(mdd_t);
01083         modelCareStatesArray = NIL(array_t);
01084       } else if (modelCareStatesArray) {
01085         modelCareStatesArray = NIL(array_t);
01086       }
01087     }
01088   }/* for all formulae */
01089
01090   if (verbosity > McVerbosityNone_c) {
01091     finalTime = util_cpu_time();
01092     fprintf(vis_stdout, "-- total mc time = %10g\n",
01093       (double)(finalTime - totalInitialTime) / 1000.0);
01094     fprintf(vis_stdout,
01095             "-- total %d image computations and %d preimage computations\n",
01096             Img_GetNumberOfImageComputation(Img_Forward_c),
01097             Img_GetNumberOfImageComputation(Img_Backward_c));
01098     /* Print tfm options if we have a global fsm. */
01099     if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) {
01100       imageInfo = Fsm_FsmReadImageInfo(modelFsm);
01101       if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
01102           Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
01103         Img_TfmPrintStatistics(imageInfo, Img_Both_c);
01104       }
01105     }
01106   }
01107
01108   /* Print results of coverage computation */
01109   McPrintCoverageSummary(modelFsm, dcLevel,
01110                          options, modelCareStatesArray,
01111                          modelCareStates, totalcoveredstates,
01112                          signalTypeList, signalList, statesCoveredList,
01113                          performCoverageHoskote, performCoverageImproved);
01114   mdd_array_free(newCoveredStatesList);
01115   mdd_array_free(statesToRemoveList);
01116   array_free(signalTypeList);
01117   array_free(signalList);
01118   mdd_array_free(statesCoveredList);
01119   if (totalcoveredstates != NIL(mdd_t))
01120     mdd_free(totalcoveredstates);
01121
01122   if (modelCareStates) {
01123     mdd_array_free(modelCareStatesArray);
01124   }
01125
01126   if(hintsArray)
01127     Ctlp_FormulaArrayFree(hintsArray);
01128
01129   if ((McOptionsReadReduceFsm(options) == FALSE) &&
01130       (reducedFsm != NIL(Fsm_Fsm_t))) {
01131     /* If "-r" was not specified and we did some reduction at top
01132        level, we need to free it */
01133     Fsm_FsmFree(reducedFsm);
01134     reducedFsm = NIL(Fsm_Fsm_t);
01135     modelFsm = NIL(Fsm_Fsm_t);
01136   }
01137
01138   if(systemVarBddIdTable)
01139     st_free_table(systemVarBddIdTable);
01140   array_free(ctlNormalFormulaArray);
01141   (void) fprintf(vis_stdout, "\n");
01142
01143   Ctlp_FormulaArrayFree(ctlArray);
01144   McOptionsFree(options);
01145   alarm(0);
01146   return 0;
01147 }
01148
01149
01157 static McOptions_t *
01158 ParseMcOptions(
01159   int argc,
01160   char **argv)
01161 {
01162   unsigned int i;
01163   int c;
01164   char *guideFileName = NIL(char);
01165   char *variablesForSystem = NIL(char);
01166   FILE *guideFile = NIL(FILE);
01167   FILE *systemFile = NIL(FILE);
01168   boolean doCoverageHoskote = FALSE;
01169   boolean doCoverageImproved = FALSE;
01170   boolean useMore = FALSE;
01171   boolean reduceFsm = FALSE;
01172   boolean printInputs = FALSE;
01173   boolean useFormulaTree = FALSE;
01174   boolean vd = FALSE;
01175   boolean beer = FALSE;
01176   boolean FAFWFlag = FALSE;
01177   boolean GFAFWFlag = FALSE;
01178   FILE *inputFp=NIL(FILE);
01179   FILE *debugOut=NIL(FILE);
01180   char *debugOutName=NIL(char);
01181   Mc_DcLevel dcLevel = McDcLevelRch_c;
01182   McDbgLevel dbgLevel = McDbgLevelNone_c;
01183   Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
01184   Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
01185   McOptions_t *options = McOptionsAlloc();
01186   int timeOutPeriod = 0;
01187   Mc_FwdBwdAnalysis traversalDirection = McBwd_c;
01188   Fsm_ArdcOptions_t *ardcOptions;
01189   Mc_GSHScheduleType schedule = McGSH_EL_c;
01190
01191   /*
01192    * Parse command line options.
01193    */
01194
01195   util_getopt_reset();
01196   while ((c = util_getopt(argc, argv, "bcirmg:hv:d:D:VBf:t:CIFR:S:GWw:")) != EOF) {
01197     switch(c) {
01198     case 'g':
01199       guideFileName = util_strsav(util_optarg);
01200       break;
01201     case 'h':
01202       goto usage;
01203     case 'v':
01204       for (i = 0; i < strlen(util_optarg); i++) {
01205         if (!isdigit((int)util_optarg[i])) {
01206           goto usage;
01207         }
01208       }
01209       verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
01210       break;
01211     case 'd':
01212       for (i = 0; i < strlen(util_optarg); i++) {
01213         if (!isdigit((int)util_optarg[i])) {
01214           goto usage;
01215         }
01216       }
01217       dbgLevel = (McDbgLevel) atoi(util_optarg);
01218       break;
01219     case 'D':
01220       for (i = 0; i < strlen(util_optarg); i++) {
01221         if (!isdigit((int)util_optarg[i])) {
01222           goto usage;
01223         }
01224       }
01225       dcLevel = (Mc_DcLevel) atoi(util_optarg);
01226       break;
01227     case 'b':
01228       fwdBwd = McBwd_c;
01229       break;
01230     case 'V':         /*Vacuity detection option*/
01231       vd = TRUE;
01232       break;
01233     case 'B':         /*Vacuity detection Beer et al method option*/
01234       vd = TRUE;
01235       beer = TRUE;
01236       break;
01237     case 'f':
01238       debugOutName = util_strsav(util_optarg);
01239       break;
01240     case 'm':
01241       useMore = TRUE;
01242       break;
01243     case 'r' :
01244       reduceFsm = TRUE;
01245       break;
01246     case 'c':
01247       useFormulaTree = TRUE;
01248       break;
01249     case 't' :
01250       timeOutPeriod  = atoi(util_optarg);
01251       break;
01252     case 'i' :
01253       printInputs = TRUE;
01254       break;
01255     case 'F' :
01256       traversalDirection = McFwd_c;
01257       break;
01258     case 'S' :
01259       schedule = McStringConvertToScheduleType(util_optarg);
01260       break;
01261     case 'w':
01262       variablesForSystem = util_strsav(util_optarg);
01263     case 'W':
01264       FAFWFlag = 1;
01265       break;
01266     case 'G':
01267       GFAFWFlag = 1;
01268       break;
01269     case 'C' :
01270       doCoverageHoskote = TRUE;
01271       break;
01272     case 'I' :
01273       doCoverageImproved = TRUE;
01274       break;
01275     default:
01276       goto usage;
01277     }
01278   }
01279
01280   /*
01281    * Open the ctl file.
01282    */
01283   if (argc - util_optind == 0) {
01284     (void) fprintf(vis_stderr, "** mc error: file containing ctl formulas not provided\n");
01285     goto usage;
01286   }
01287   else if (argc - util_optind > 1) {
01288     (void) fprintf(vis_stderr, "** mc error: too many arguments\n");
01289     goto usage;
01290   }
01291
01292   McOptionsSetFwdBwd(options, fwdBwd);
01293   McOptionsSetUseMore(options, useMore);
01294   McOptionsSetReduceFsm(options, reduceFsm);
01295   McOptionsSetVacuityDetect(options, vd);
01296   McOptionsSetBeerMethod(options, beer);
01297   McOptionsSetUseFormulaTree(options, useFormulaTree);
01298   McOptionsSetPrintInputs(options, printInputs);
01299   McOptionsSetTimeOutPeriod(options, timeOutPeriod);
01300   McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
01301   McOptionsSetCoverageHoskote(options, doCoverageHoskote);
01302   McOptionsSetCoverageImproved(options, doCoverageImproved);
01303
01304   if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
01305     fprintf(vis_stderr, "** mc warning : -w and -W options are ignored without -d option\n");
01306   }
01307
01308   if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
01309     fprintf(vis_stderr, "** mc warning : -i is recommended with -w or -W option\n");
01310   }
01311   if(FAFWFlag) {
01312     if (bdd_get_package_name() != CUDD) {
01313       fprintf(vis_stderr, "** mc warning : -w and -W option is only available with CUDD\n");
01314       FAFWFlag = 0;
01315       FREE(variablesForSystem);
01316       variablesForSystem = NIL(char);
01317     }
01318   }
01319
01320
01321   if (schedule == McGSH_Unassigned_c) {
01322     (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
01323     goto usage;
01324   } else {
01325     McOptionsSetSchedule(options, schedule);
01326   }
01327   inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
01328   if (inputFp == NIL(FILE)) {
01329     McOptionsFree(options);
01330     if (guideFileName != NIL(char)) FREE(guideFileName);
01331     return NIL(McOptions_t);
01332   }
01333   McOptionsSetCtlFile(options, inputFp);
01334
01335   if (debugOutName != NIL(char)) {
01336     debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
01337     FREE(debugOutName);
01338     if (debugOut == NIL(FILE)) {
01339       McOptionsFree(options);
01340       if (guideFileName != NIL(char)) FREE(guideFileName);
01341       return NIL(McOptions_t);
01342     }
01343   }
01344   McOptionsSetDebugFile(options, debugOut);
01345
01346
01347   if (guideFileName != NIL(char)) {
01348     guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
01349     if (guideFile == NIL(FILE)) {
01350       fprintf(vis_stderr, "** mc error: cannot open guided search file %s.\n",
01351               guideFileName);
01352       FREE(guideFileName);
01353       guideFileName = NIL(char);
01354       McOptionsFree(options);
01355       return NIL(McOptions_t);
01356     }
01357     FREE(guideFileName);
01358     guideFileName = NIL(char);
01359   }
01360   McOptionsSetGuideFile(options, guideFile);
01361
01362   if (variablesForSystem != NIL(char)) {
01363     systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
01364     if (systemFile == NIL(FILE)) {
01365       fprintf(vis_stderr, "** mc error: cannot open system variables file for FAFW %s.\n",
01366               variablesForSystem);
01367       FREE(variablesForSystem);
01368       variablesForSystem = NIL(char);
01369       McOptionsFree(options);
01370       return NIL(McOptions_t);
01371     }
01372     FREE(variablesForSystem);
01373     variablesForSystem = NIL(char);
01374   }
01375   McOptionsSetVariablesForSystem(options, systemFile);
01376
01377   if ((verbosityLevel != McVerbosityNone_c) &&
01378        (verbosityLevel != McVerbosityLittle_c) &&
01379        (verbosityLevel != McVerbositySome_c) &&
01380        (verbosityLevel != McVerbosityMax_c)) {
01381     goto usage;
01382   }
01383   else {
01384     McOptionsSetVerbosityLevel(options, verbosityLevel);
01385   }
01386
01387   if ((dbgLevel != McDbgLevelNone_c) &&
01388        (dbgLevel != McDbgLevelMin_c) &&
01389        (dbgLevel != McDbgLevelMinVerbose_c) &&
01390        (dbgLevel != McDbgLevelMax_c) &&
01391        (dbgLevel != McDbgLevelInteractive_c)) {
01392     goto usage;
01393   }
01394   else {
01395     McOptionsSetDbgLevel(options, dbgLevel);
01396   }
01397
01398   if ((dcLevel != McDcLevelNone_c) &&
01399        (dcLevel != McDcLevelRch_c ) &&
01400        (dcLevel != McDcLevelRchFrontier_c ) &&
01401        (dcLevel != McDcLevelArdc_c )) {
01402     goto usage;
01403   }
01404   else {
01405     McOptionsSetDcLevel(options, dcLevel);
01406   }
01407
01408   McOptionsSetTraversalDirection(options, traversalDirection);
01409   if (dcLevel == McDcLevelArdc_c) {
01410     ardcOptions = Fsm_ArdcAllocOptionsStruct();
01411     Fsm_ArdcGetDefaultOptions(ardcOptions);
01412   } else
01413     ardcOptions = NIL(Fsm_ArdcOptions_t);
01414   McOptionsSetArdcOptions(options, ardcOptions);
01415
01416   return options;
01417
01418   usage:
01419   (void) fprintf(vis_stderr, "usage: model_check [-b][-c][-d dbg_level][-f dbg_file][-g <hintfile>][-h][-i][-m][-r][-V][-B][-t period][-C][-I][-P][-v verbosity_level][-D dc_level][-F][-S <schedule>] <ctl_file>\n");
01420   (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\n");
01421   (void) fprintf(vis_stderr, "    -c \tNo sharing of CTL parse tree. This option does not matter for vacuity detection.\n");
01422   (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
01423   (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
01424   (void) fprintf(vis_stderr, "        debug_level = 1 => automatic minimal debugging\n");
01425   (void) fprintf(vis_stderr, "        debug_level = 2 => automatic minimal debugging with extra verbosity\n");
01426   (void) fprintf(vis_stderr, "        debug_level = 3 => automatic maximal debugging\n");
01427   (void) fprintf(vis_stderr, "        debug_level = 4 => interactive debugging\n");
01428   (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
01429   (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
01430   (void) fprintf(vis_stderr, "    -g <hint_file> \tSpecify file for guided search.\n");
01431   (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
01432   (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
01433   (void) fprintf(vis_stderr, "    -m \tPipe debug output through more.\n");
01434   (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to formula being verified\n");
01435   (void) fprintf(vis_stderr, "    -t <period> time out period\n");
01436   (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
01437   (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
01438   (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
01439   (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
01440   (void) fprintf(vis_stderr, "    -w <node file> \tSpecify variables controlled by system.\n");
01441   (void) fprintf(vis_stderr, "    -B  vacuity detection for w-ACTL formulae using method of Beer et al \n");
01442   (void) fprintf(vis_stderr, "    -C Compute coverage of all observable signals using Hoskote et.al's implementation\n");
01443   (void) fprintf(vis_stderr, "    -D <dc_level>\n");
01444   (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
01445   (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
01446   (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");
01447
01448   (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
01449   (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
01450   (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
01451   (void) fprintf(vis_stderr, "    -F \tUse forward model checking.\n");
01452   (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
01453   (void) fprintf(vis_stderr, "    -I Compute coverage of all observable signals using improved coverage implementation\n");
01454   (void) fprintf(vis_stderr, "    -S <schedule>\n");
01455   (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
01456   (void) fprintf(vis_stderr, "    -V  thorough vacuity detection\n");
01457   (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
01458   (void) fprintf(vis_stderr, "    <ctl_file> The input file containing CTL formula to be checked.\n");
01459
01460   if (guideFileName != NIL(char)) FREE(guideFileName);
01461   McOptionsFree(options);
01462
01463   return NIL(McOptions_t);
01464 }
01465
01466
01667 static int
01668 CommandLe(
01669   Hrc_Manager_t **hmgr,
01670   int argc,
01671   char **argv)
01672 {
01673   McOptions_t *options;
01674   Mc_VerbosityLevel verbosity;
01675   Mc_LeMethod_t leMethod;
01676   Mc_DcLevel dcLevel;
01677   McDbgLevel dbgLevel;
01678   FILE *dbgFile= NIL(FILE);
01679   boolean printInputs = FALSE;
01680   int timeOutPeriod = 0;
01681   Mc_GSHScheduleType GSHschedule;
01682   Mc_FwdBwdAnalysis GSHdirection;
01683   int lockstep;
01684   int useMore;
01685   int simValue;
01686   int reduceFsm_flag = 1;
01687   long startRchTime;
01688   mdd_t *modelCareStates;
01689   Fsm_Fsm_t *totalFsm;
01690   Fsm_Fsm_t *modelFsm, *reducedFsm = NIL(Fsm_Fsm_t);
01691   mdd_t *fairInitStates;
01692   array_t *modelCareStatesArray;
01693   long initialTime, finalTime; /* for lang_empty checking */
01694
01695   Img_ResetNumberOfImageComputation(Img_Both_c);
01696
01697   /* Read options and set timeout if requested. */
01698   if (!(options = ParseLeOptions(argc, argv))) {
01699     return 1;
01700   }
01701
01702   totalFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
01703   if (totalFsm == NIL(Fsm_Fsm_t)) {
01704     (void) fprintf(vis_stdout, "%s\n", error_string());
01705     error_init();
01706     McOptionsFree(options);
01707     return 1;
01708   }
01709
01710   initialTime = util_cpu_time();
01711
01712   verbosity     = McOptionsReadVerbosityLevel(options);
01713   leMethod      = McOptionsReadLeMethod(options);
01714   dcLevel       = McOptionsReadDcLevel(options);
01715   dbgLevel      = McOptionsReadDbgLevel(options);
01716   printInputs   = McOptionsReadPrintInputs(options);
01717   timeOutPeriod = McOptionsReadTimeOutPeriod(options);
01718   GSHschedule   = McOptionsReadSchedule(options);
01719   GSHdirection  = McOptionsReadTraversalDirection(options);
01720   lockstep      = McOptionsReadLockstep(options);
01721   dbgFile       = McOptionsReadDebugFile(options);
01722   useMore       = McOptionsReadUseMore(options);
01723   simValue      = McOptionsReadSimValue(options);
01724
01725   if (dbgLevel != McDbgLevelNone_c && GSHdirection == McFwd_c) {
01726     (void) fprintf(vis_stderr, "** le error: -d is incompatible with -F\n");
01727     McOptionsFree(options);
01728     return 1;
01729   }
01730   if (dcLevel !=  McDcLevelRch_c && GSHdirection == McFwd_c) {
01731     (void) fprintf(vis_stderr, "** le error: -F can only be used with -D1\n");
01732     McOptionsFree(options);
01733     return 1;
01734   }
01735
01736   if (timeOutPeriod > 0) {
01737     /* Set the static variables used by the signal handler. */
01738     mcTimeOut = timeOutPeriod;
01739     alarmLapTime  = util_cpu_ctime();
01740     (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
01741     (void) alarm(timeOutPeriod);
01742     if (setjmp(timeOutEnv) > 0) {
01743       (void) fprintf(vis_stdout,
01744                      "# LE: language emptiness - timeout occurred after %d seconds.\n",
01745                      timeOutPeriod);
01746       (void) fprintf(vis_stdout, "# LE: data may be corrupted.\n");
01747       if (verbosity > McVerbosityNone_c) {
01748         (void) fprintf(vis_stdout,
01749                        "-- total %d image computations and %d preimage computations\n",
01750                        Img_GetNumberOfImageComputation(Img_Forward_c),
01751                        Img_GetNumberOfImageComputation(Img_Backward_c));
01752       }
01753       alarm(0);
01754       return 1;
01755     }
01756   }
01757
01758   /* Reduce FSM to cone of influence of fairness constraints. */
01759   if (reduceFsm_flag) {
01760     Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
01761     array_t *ctlNormalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
01762     reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
01763     array_free(ctlNormalFormulaArray);
01764   }
01765
01766   if (reducedFsm == NIL(Fsm_Fsm_t)) {
01767     modelFsm = totalFsm;
01768   }else {
01769     modelFsm = reducedFsm;
01770   }
01771
01772   /* Find care states and put them in an array */
01773   if (dcLevel == McDcLevelArdc_c) { /* aRDC */
01774     Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
01775     array_t *tmpArray;
01776     Fsm_ArdcGetDefaultOptions(ardcOptions);
01777
01778     if (verbosity > 0)
01779       startRchTime = util_cpu_time();
01780     else /* to remove uninitialized variable warning */
01781       startRchTime = 0;
01782     tmpArray = Fsm_ArdcComputeOverApproximateReachableStates(
01783       modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
01784     modelCareStatesArray = mdd_array_duplicate(tmpArray);
01785
01786     FREE(ardcOptions);
01787
01788     if (verbosity > 0 )
01789       Fsm_ArdcPrintReachabilityResults(modelFsm,
01790                                        util_cpu_time() - startRchTime);
01791
01792   }else if (dcLevel >= McDcLevelRch_c) { /*RDC*/
01793     if (verbosity > 0)
01794       startRchTime = util_cpu_time();
01795     else /* to remove uninitialized variable warning */
01796       startRchTime = 0;
01797     modelCareStates =
01798       Fsm_FsmComputeReachableStates(modelFsm, 0, verbosity, 0, 0,
01799                                     (lockstep != MC_LOCKSTEP_OFF), 0, 0,
01800                                     Fsm_Rch_Default_c, 0, 0,
01801                                     NIL(array_t), FALSE, NIL(array_t));
01802     if (verbosity > 0) {
01803       Fsm_FsmReachabilityPrintResults(modelFsm,
01804                                       util_cpu_time() - startRchTime,
01805                                       Fsm_Rch_Default_c);
01806     }
01807     modelCareStatesArray = array_alloc(mdd_t *, 0);
01808     array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
01809
01810   } else {  /* mdd_one */
01811     modelCareStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
01812     modelCareStatesArray = array_alloc(mdd_t *, 0);
01813     array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
01814   }
01815
01816
01817   fairInitStates = Mc_FsmCheckLanguageEmptiness(modelFsm,
01818                                                 modelCareStatesArray,
01819                                                 Mc_Aut_Strong_c,
01820                                                 leMethod,
01821                                                 dcLevel,
01822                                                 dbgLevel,
01823                                                 printInputs,
01824                                                 verbosity,
01825                                                 GSHschedule,
01826                                                 GSHdirection,
01827                                                 lockstep,
01828                                                 dbgFile,
01829                                                 useMore,
01830                                                 simValue,
01831                                                 "LE");
01832
01833   if (verbosity > McVerbosityNone_c) {
01834     finalTime = util_cpu_time();
01835     fprintf(vis_stdout, "-- total le time = %10g\n",
01836             (double)(finalTime - initialTime) / 1000.0);
01837     fprintf(vis_stdout,
01838             "-- total %d image computations and %d preimage computations\n",
01839             Img_GetNumberOfImageComputation(Img_Forward_c),
01840             Img_GetNumberOfImageComputation(Img_Backward_c));
01841   }
01842
01843   /* Clean up. */
01844   if (fairInitStates) {
01845     mdd_free(fairInitStates);
01846   }
01847   mdd_array_free(modelCareStatesArray);
01848   McOptionsFree(options);
01849   if (reducedFsm) {
01850     Fsm_FsmFree(reducedFsm);
01851   }
01852
01853   alarm(0);
01854   return 0;
01855
01856 } /* CommandLe */
01857
01858
01866 static McOptions_t *
01867 ParseLeOptions(
01868   int argc,
01869   char **argv)
01870 {
01871   unsigned int i;
01872   int c;
01873   boolean useSimFormat = FALSE;
01874   FILE *debugOut=NIL(FILE);
01875   char *debugOutName=NIL(char);
01876   Mc_DcLevel dcLevel = McDcLevelRch_c;
01877   Mc_LeMethod_t leMethod = Mc_Le_Default_c;
01878   McDbgLevel dbgLevel = McDbgLevelNone_c;
01879   Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
01880   Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
01881   McOptions_t *options = McOptionsAlloc();
01882   boolean printInputs = FALSE;
01883   boolean useMore = FALSE;
01884   int timeOutPeriod = 0;
01885   Mc_GSHScheduleType schedule = McGSH_EL_c;
01886   Mc_FwdBwdAnalysis direction = McBwd_c;
01887   int lockstep = MC_LOCKSTEP_OFF;
01888   Fsm_ArdcOptions_t *ardcOptions;
01889
01890   /*
01891    * Parse command line options.
01892    */
01893
01894   util_getopt_reset();
01895   while ((c = util_getopt(argc, argv, "bihmt:v:d:A:D:f:sS:L:F")) != EOF) {
01896     switch(c) {
01897     case 'h':
01898       goto usage;
01899     case 'v':
01900       for (i = 0; i < strlen(util_optarg); i++) {
01901         if (!isdigit((int)util_optarg[i])) {
01902           goto usage;
01903         }
01904       }
01905       verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
01906       break;
01907     case 'd':
01908       for (i = 0; i < strlen(util_optarg); i++) {
01909         if (!isdigit((int)util_optarg[i])) {
01910           goto usage;
01911         }
01912       }
01913       dbgLevel = (McDbgLevel) atoi(util_optarg);
01914       break;
01915     case 'A':
01916       for (i = 0; i < strlen(util_optarg); i++) {
01917         if (!isdigit((int)util_optarg[i])) {
01918           goto usage;
01919         }
01920       }
01921       leMethod = (Mc_LeMethod_t) atoi(util_optarg);
01922       break;
01923     case 'D':
01924       for (i = 0; i < strlen(util_optarg); i++) {
01925         if (!isdigit((int)util_optarg[i])) {
01926           goto usage;
01927         }
01928       }
01929       dcLevel = (Mc_DcLevel) atoi(util_optarg);
01930       break;
01931     case 'f':
01932       debugOutName = util_strsav(util_optarg);
01933       break;
01934     case 's':
01935       useSimFormat = TRUE;
01936       break;
01937     case 't':
01938       timeOutPeriod = atoi(util_optarg);
01939       break;
01940     case 'i':
01941       printInputs = TRUE;
01942       break;
01943     case 'm':
01944       useMore = TRUE;
01945       break;
01946     case 'b':
01947       fwdBwd = McBwd_c;
01948       break;
01949     case 'S' :
01950       schedule = McStringConvertToScheduleType(util_optarg);
01951       break;
01952     case 'L' :
01953       lockstep = McStringConvertToLockstepMode(util_optarg);
01954       break;
01955     case 'F' :
01956       direction = McFwd_c;
01957       break;
01958     default:
01959       goto usage;
01960     }
01961   }
01962
01963   if (schedule == McGSH_Unassigned_c) {
01964     (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
01965     goto usage;
01966   } else {
01967     McOptionsSetSchedule(options, schedule);
01968   }
01969   McOptionsSetTraversalDirection(options, direction);
01970   if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
01971     (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
01972     goto usage;
01973   } else {
01974     McOptionsSetLockstep(options, lockstep);
01975   }
01976   if ((verbosityLevel != McVerbosityNone_c) &&
01977        (verbosityLevel != McVerbosityLittle_c) &&
01978        (verbosityLevel != McVerbositySome_c) &&
01979        (verbosityLevel != McVerbosityMax_c)) {
01980     goto usage;
01981   }
01982   else {
01983     McOptionsSetVerbosityLevel(options, verbosityLevel);
01984   }
01985
01986   if (debugOutName != NIL(char)) {
01987     debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
01988     if (debugOut == NIL(FILE)) {
01989       McOptionsFree(options);
01990       return NIL(McOptions_t);
01991     }
01992   }
01993   McOptionsSetDebugFile(options, debugOut);
01994
01995   if ((dbgLevel != McDbgLevelNone_c) &&
01996        (dbgLevel != McDbgLevelMin_c)) {
01997     goto usage;
01998   }
01999   else {
02000     McOptionsSetDbgLevel(options, dbgLevel);
02001   }
02002
02003   if ((dcLevel != McDcLevelNone_c)  &&
02004        (dcLevel != McDcLevelRch_c )  &&
02005        (dcLevel != McDcLevelRchFrontier_c )  &&
02006        (dcLevel != McDcLevelArdc_c )) {
02007     goto usage;
02008   }
02009   else {
02010     McOptionsSetDcLevel(options, dcLevel);
02011   }
02012
02013   if ((leMethod != Mc_Le_Default_c) &&
02014       (leMethod != Mc_Le_Dnc_c)) {
02015     goto usage;
02016   }
02017   else {
02018     McOptionsSetLeMethod(options, leMethod);
02019   }
02020
02021   /* set Ardc options for le : C.W. */
02022   if (dcLevel == McDcLevelArdc_c) {
02023       ardcOptions = Fsm_ArdcAllocOptionsStruct();
02024       Fsm_ArdcGetDefaultOptions(ardcOptions);
02025   } else
02026       ardcOptions = NIL(Fsm_ArdcOptions_t);
02027   McOptionsSetArdcOptions(options, ardcOptions);
02028
02029   McOptionsSetFwdBwd(options, fwdBwd);
02030   McOptionsSetSimValue(options, useSimFormat);
02031   McOptionsSetUseMore(options, useMore);
02032   McOptionsSetPrintInputs(options, printInputs);
02033   McOptionsSetTimeOutPeriod(options, timeOutPeriod);
02034   return options;
02035
02036   usage:
02037   (void) fprintf(vis_stderr, "usage: lang_empty [-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A <le_method>][-D <dc_level>][-S <schedule>][-F][-L <lockstep_mode>]\n");
02038   (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\n");
02039   (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
02040   (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
02041   (void) fprintf(vis_stderr, "        debug_level = 1 => automatic debugging\n");
02042   (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
02043   (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
02044   (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
02045   (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
02046   (void) fprintf(vis_stderr, "    -m \tPipe debug output through more\n");
02047   (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
02048   (void) fprintf(vis_stderr, "    -t <period> time out period\n");
02049   (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
02050   (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
02051   (void) fprintf(vis_stderr, "        verbosity_level = 1 => feedback\n");
02052   (void) fprintf(vis_stderr, "        verbosity_level = 2 => feedback and CPU usage profile\n");
02053   (void) fprintf(vis_stderr, "    -A <le_method>\n");
02054   (void) fprintf(vis_stderr, "        le_method = 0 => no use of Divide and Compose (Default)\n");
02055   (void) fprintf(vis_stderr, "        le_method = 1 => use Divide and Compose\n");
02056   (void) fprintf(vis_stderr, "    -D <dc_level>\n");
02057   (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
02058   (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
02059   (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");
02060
02061   (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
02062   (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
02063   (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
02064   (void) fprintf(vis_stderr, "    -S <schedule>\n");
02065   (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
02066   (void) fprintf(vis_stderr, "    -F \tUse forward analysis in fixpoint computation.\n");
02067   (void) fprintf(vis_stderr, "    -L <lockstep_mode>\n");
02068   (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");
02069
02070   McOptionsFree(options);
02071
02072   return NIL(McOptions_t);
02073 }
02074
02075
02373 static int
02374 CommandInv(
02375   Hrc_Manager_t **hmgr,
02376   int argc,
02377   char **argv)
02378 {
02379   int i, j;
02380   mdd_t *tautology;
02381   McOptions_t *options;
02382   FILE *invarFile;
02383   array_t *invarArray, *formulas, *sortedFormulaArray;
02384   static Fsm_Fsm_t *totalFsm, *modelFsm;
02385   mdd_manager *mddMgr;
02386   Ntk_Network_t *network;
02387   Mc_VerbosityLevel verbosity;
02388   Mc_DcLevel dcLevel;
02389   array_t *invarNormalFormulaArray, *invarStatesArray;
02390   int timeOutPeriod = 0;
02391   int debugFlag;
02392   int buildOnionRings;
02393   Fsm_RchType_t approxFlag;
02394   int ardc;
02395   int someLeft;
02396   Ctlp_Formula_t *invarFormula;
02397   mdd_t *invarFormulaStates;
02398   mdd_t *reachableStates;
02399   array_t *fsmArray;
02400   int printStep = 0;
02401   long initTime, finalTime;
02402   array_t *careSetArray;
02403   FILE              *guideFile;
02404   FILE          *systemFile;
02405   st_table      *systemVarBddIdTable;
02406   Ctlp_FormulaArray_t *hintsArray    = NIL(Fsm_HintsArray_t);
02407   array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
02408
02409   error_init();
02410   initTime = util_cpu_time();
02411
02412   /* get command line options */
02413   if (!(options = ParseInvarOptions(argc, argv))) {
02414     return 1;
02415   }
02416   verbosity = McOptionsReadVerbosityLevel(options);
02417   dcLevel = McOptionsReadDcLevel(options);
02418   invarFile = McOptionsReadCtlFile(options);
02419   timeOutPeriod = McOptionsReadTimeOutPeriod(options);
02420   approxFlag = McOptionsReadInvarApproxFlag(options);
02421   buildOnionRings = (int)McOptionsReadInvarOnionRingsFlag(options);
02422
02423   /* read the array of invariants */
02424   invarArray = Ctlp_FileParseFormulaArray(invarFile);
02425   fclose(invarFile);
02426   if (invarArray == NIL(array_t)) {
02427     (void) fprintf(vis_stderr, "** inv error: Error in parsing invariants from file\n");
02428     McOptionsFree(options);
02429     return 1;
02430   }
02431   if (array_n(invarArray) == 0) {
02432     (void) fprintf(vis_stderr, "** inv error: No formula in file\n");
02433     McOptionsFree(options);
02434     return 1;
02435   }
02436
02437   /* read the netwrok */
02438   network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
02439   if (network == NIL(Ntk_Network_t)) {
02440     fprintf(vis_stderr, "%s\n", error_string());
02441     error_init();
02442     McOptionsFree(options);
02443     return 1;
02444   }
02445
02446   /**************************************************************************
02447    * if "-A 3" is enabled (using the abstraction refinement method GRAB ),
02448    *    call GRAB.
02449    **************************************************************************/
02450   if (approxFlag == Fsm_Rch_Grab_c) {
02451
02452     if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
02453       McOptionsFree(options);
02454       fprintf(vis_stderr,
02455               "** inv error: To use GRAB, please run build_partition_maigs first\n");
02456       /*McOptionsFree(options);*/
02457       return 1;
02458     }
02459
02460     if (timeOutPeriod > 0) {
02461       /* Set the static variables used by the signal handler. */
02462       mcTimeOut = timeOutPeriod;
02463       alarmLapTime = util_cpu_ctime();
02464       (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
02465       (void) alarm(timeOutPeriod);
02466       if (setjmp(timeOutEnv) > 0) {
02467         (void) fprintf(vis_stdout,
02468            "# INV: Checking Invariant: timeout occurred after %d seconds.\n",
02469                        timeOutPeriod);
02470         (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
02471         alarm(0);
02472         return 1;
02473       }
02474     }
02475
02476     Grab_NetworkCheckInvariants(network,
02477                                 invarArray,
02478                                 "GRAB", /* refineAlgorithm, */
02479                                 TRUE,   /* fineGrainFlag, */
02480                                 TRUE,   /* refineMinFlag, */
02481                                 FALSE,  /* useArdcFlag, */
02482                                 2,      /* cexType = SOR */
02483                                 verbosity,
02484                                 McOptionsReadDbgLevel(options),
02485                                 McOptionsReadPrintInputs(options),
02486                                 McOptionsReadDebugFile(options),
02487                                 McOptionsReadUseMore(options),
02488                                 "INV" /* driverName */
02489                                 );
02490     McOptionsFree(options);
02491     return 0;
02492   }
02493
02494   if (approxFlag == Fsm_Rch_PureSat_c) {
02495
02496     if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
02497       McOptionsFree(options);
02498       fprintf(vis_stderr,
02499               "** inv error: Please run build_partition_maigs first\n");
02500       McOptionsFree(options);
02501       return 1;
02502     }
02503
02504     if (timeOutPeriod > 0) {
02505       /* Set the static variables used by the signal handler. */
02506       mcTimeOut = timeOutPeriod;
02507       alarmLapTime = util_cpu_ctime();
02508       (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
02509       (void) alarm(timeOutPeriod);
02510       if (setjmp(timeOutEnv) > 0) {
02511         (void) fprintf(vis_stdout,
02512            "# INV by PURESAT: Checking Invariant using PURESAT: timeout occurred after %d seconds.\n",
02513                        timeOutPeriod);
02514         (void) fprintf(vis_stdout, "# INV by PURESAT: data may be corrupted.\n");
02515         alarm(0);
02516         return 1;
02517       }
02518     }
02519     PureSat_CheckInvariant(network,invarArray,
02520                            (int)options->verbosityLevel,
02521                            options->dbgLevel,McOptionsReadDebugFile(options),
02522                            McOptionsReadPrintInputs(options),options->incre,
02523                            options->sss, options->flatIP, options->IPspeed);
02524     McOptionsFree(options);
02525     return 0;
02526   }
02527   guideFile =  McOptionsReadGuideFile(options);
02528
02529   if(guideFile != NIL(FILE) ){
02530     hintsArray = Mc_ReadHints(guideFile);
02531     fclose(guideFile); guideFile = NIL(FILE);
02532     if( hintsArray == NIL(array_t) ){
02533       McOptionsFree(options);
02534       return 1;
02535     }
02536   } /* if guided search */
02537
02538   if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
02539      Img_UserSpecifiedMethod() != Img_Monolithic_c &&
02540      Img_UserSpecifiedMethod() != Img_Mlp_c &&
02541      guideFile != NIL(FILE)){
02542     fprintf(vis_stdout,
02543  "** inv error: The Tfm and Hybrid image methods are incompatible with -g\n");
02544     McOptionsFree(options);
02545     return 1;
02546   }
02547
02548   if (dcLevel == McDcLevelArdc_c)
02549     ardc = 1;
02550   else
02551     ardc = 0;
02552
02553   /* obtain the fsm and mdd manager */
02554   totalFsm = Fsm_NetworkReadOrCreateFsm(network);
02555   if (totalFsm == NIL(Fsm_Fsm_t)) {
02556     fprintf(vis_stderr, "%s\n", error_string());
02557     error_init();
02558     McOptionsFree(options);
02559     return 1;
02560   }
02561
02562   systemVarBddIdTable = 0;
02563   systemFile = McOptionsReadSystemFile(options);
02564   if(systemFile != NIL(FILE) ){
02565     systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
02566     fclose(systemFile); systemFile = NIL(FILE);
02567     if(systemVarBddIdTable == (st_table *)-1 ){
02568       McOptionsFree(options);
02569       return 1;
02570     }
02571   } /* if FAFW */
02572
02573   if(options->FAFWFlag && systemVarBddIdTable == 0) {
02574     systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
02575   }
02576
02577   mddMgr = Fsm_FsmReadMddManager(totalFsm);
02578   tautology = mdd_one(mddMgr);
02579
02580   /* set time out */
02581   if (timeOutPeriod > 0) {
02582     /* Set the static variables used by the signal handler. */
02583     mcTimeOut = timeOutPeriod;
02584     alarmLapTime = util_cpu_ctime();
02585     (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
02586     (void) alarm(timeOutPeriod);
02587     if (setjmp(timeOutEnv) > 0) {
02588       (void) fprintf(vis_stdout, "# INV: Checking Invariant: timeout occurred after %d seconds.\n", timeOutPeriod);
02589       (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
02590       alarm(0);
02591       return 1;
02592     }
02593   }
02594
02595   /* debugFlag = 1 -> need to store/compute onion shells, else not */
02596   debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
02597
02598   /* use formula tree if reduce option and dont-care level is high */
02599   if ((McOptionsReadReduceFsm(options) == TRUE) &&
02600      (dcLevel != McDcLevelNone_c)) {
02601       McOptionsSetUseFormulaTree(options, TRUE);
02602   }
02603
02604   /* derive the normalized array of invariant formulas */
02605   if (McOptionsReadUseFormulaTree(options) == TRUE) {
02606     invarNormalFormulaArray =
02607       Ctlp_FormulaArrayConvertToExistentialFormTree(invarArray);
02608   } else {
02609     array_t *temp = Ctlp_FormulaArrayConvertToDAG( invarArray );
02610     array_free( invarArray );
02611     invarArray = temp;
02612     invarNormalFormulaArray = Ctlp_FormulaDAGConvertToExistentialFormDAG(
02613       invarArray );
02614   }
02615
02616   if (array_n(invarNormalFormulaArray) == 0) {
02617     array_free(invarNormalFormulaArray);
02618     Ctlp_FormulaArrayFree(invarArray);
02619     mdd_free(tautology);
02620     return 1;
02621   }
02622   fsmArray = array_alloc(Fsm_Fsm_t *, 0);
02623   sortedFormulaArray = SortFormulasByFsm(totalFsm, invarNormalFormulaArray,
02624                                          fsmArray, options);
02625   if (sortedFormulaArray == NIL(array_t)) {
02626     array_free(invarNormalFormulaArray);
02627     Ctlp_FormulaArrayFree(invarArray);
02628     mdd_free(tautology);
02629     return 1;
02630   }
02631   assert(array_n(fsmArray) == array_n(sortedFormulaArray));
02632
02633   careSetArray = array_alloc(mdd_t *, 0);
02634
02635   /* main loop for array of array of formulas. Each of the latter
02636      arrays corresponds to one reduced fsm. */
02637   arrayForEachItem(array_t *, sortedFormulaArray, i, formulas) {
02638     int *resultArray;
02639     int fail;
02640     /* initialize pass, fail array */
02641     resultArray = ALLOC(int, array_n(formulas));
02642     for (j = 0; j < array_n(formulas); j++) {
02643       resultArray[j] = 1;
02644     }
02645     /* get reduced fsm for this set of formulas */
02646     modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, i);
02647
02648     /* evaluate hints for this reduced fsm, stop if the hints contain variables
02649      * outside this model FSM.
02650      */
02651     if (hintsArray != NIL(Ctlp_FormulaArray_t)) {
02652       int k;
02653       hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
02654       if( hintsStatesArray == NIL(array_t)) { /* something wrong, clean up */
02655         int l;
02656         fprintf(vis_stdout, "Hints dont match the reduced FSM for this set of invariants.\n");
02657         fprintf(vis_stdout, "Continuing with the next set of invariants\n");
02658         for (k = i; k < array_n(sortedFormulaArray); k++) {
02659           formulas = array_fetch(array_t *, sortedFormulaArray, k);
02660           arrayForEachItem(Ctlp_Formula_t *, formulas, l, invarFormula) {
02661             Ctlp_FormulaFree(invarFormula);
02662           }
02663           array_free(formulas);
02664           /* get reduced fsm for this set of formulas */
02665           modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, k);
02666           /* free the Fsm if it was reduced here */
02667           if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
02668         }
02669         array_free(careSetArray);
02670         array_free(fsmArray);
02671         array_free(sortedFormulaArray);
02672         array_free(invarNormalFormulaArray);
02673         (void) fprintf(vis_stdout, "\n");
02674
02675         Ctlp_FormulaArrayFree(invarArray);
02676         McOptionsFree(options);
02677         mdd_free(tautology);
02678         return 1;
02679       }
02680     }/* hints exist */
02681
02682     if(options->FAFWFlag > 1) {
02683       reachableStates = Fsm_FsmComputeReachableStates(
02684           modelFsm, 0, verbosity , 0, 0, 1, 0, 0,
02685           approxFlag, ardc, 0, 0, (verbosity > 1),
02686           hintsStatesArray);
02687       mdd_free(reachableStates);
02688     }
02689
02690
02691     invarStatesArray = array_alloc(mdd_t *, 0);
02692     array_insert(mdd_t *, careSetArray, 0, tautology);
02693     arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
02694       /* compute the set of states represented by the invariant. */
02695       invarFormulaStates =
02696         Mc_FsmEvaluateFormula(modelFsm, invarFormula, tautology,
02697                               NIL(Fsm_Fairness_t), careSetArray,
02698                               MC_NO_EARLY_TERMINATION,
02699                               NIL(Fsm_HintsArray_t), Mc_None_c,
02700                               verbosity, dcLevel, buildOnionRings,
02701                               McGSH_EL_c);
02702
02703       array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
02704     }
02705
02706     printStep = (verbosity == McVerbosityMax_c) && (totalFsm == modelFsm);
02707     /* main loop to check a set of invariants. */
02708     do {
02709       boolean compute = FALSE;
02710       /* check if the computed reachable set in the total FSM already violates an invariant. */
02711       compute = TestInvariantsInTotalFsm(totalFsm, invarStatesArray, (debugFlag ||
02712                                                          buildOnionRings));
02713
02714       /* compute reachable set or until early failure */
02715       if (compute)
02716         reachableStates = Fsm_FsmComputeReachableStates(
02717           modelFsm, 0, verbosity , 0, 0, (debugFlag || buildOnionRings), 0, 0,
02718           approxFlag, ardc, 0, invarStatesArray, (verbosity > 1),
02719           hintsStatesArray);
02720       else if (debugFlag || buildOnionRings) {
02721         (void)Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
02722       } else {
02723         reachableStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(totalFsm));
02724       }
02725
02726       ardc = 0; /* once ardc is applied, we don't need it again. */
02727       /* updates result array and sets fail if any formula failed.*/
02728       fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
02729       mdd_free(reachableStates);
02730       someLeft = 0;
02731       if (fail) {
02732         /* some invariant failed */
02733         if (debugFlag) {
02734           assert (approxFlag != Fsm_Rch_Oa_c);
02735           Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
02736           Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
02737           InvarPrintDebugInformation(modelFsm, formulas, invarStatesArray,
02738                                      resultArray, options, hintsStatesArray);
02739           Fsm_FsmSetFAFWFlag(modelFsm, 0);
02740           Fsm_FsmSetSystemVariableFAFW(modelFsm, 0);
02741         } else if (approxFlag == Fsm_Rch_Oa_c) {
02742           assert(!buildOnionRings);
02743           /* May be a false negative */
02744           /* undo failed results in the result array, report passed formulae */
02745           arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
02746             if (invarFormulaStates == NIL(mdd_t)) continue;
02747             /* print all formulae that are known to have passed */
02748             if (resultArray[j] == 1) {
02749               mdd_free(invarFormulaStates);
02750               array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
02751               (void) fprintf(vis_stdout, "# INV: Early detection - formula passed --- ");
02752               invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
02753               Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
02754               fprintf(vis_stdout, "\n");
02755             } else resultArray[j] = 1;
02756           }
02757           fprintf(vis_stdout, "# INV: Invariant violated by over-approximated reachable states\n");
02758           fprintf(vis_stdout, "# INV: Switching to BFS (exact computation) to resolve false negatives\n");
02759           /* compute reachable set or until early failure */
02760           reachableStates = Fsm_FsmComputeReachableStates(
02761             modelFsm, 0, verbosity , 0, 0, 0, 0, 0, Fsm_Rch_Bfs_c, ardc, 0,
02762             invarStatesArray, (verbosity > 1), hintsStatesArray);
02763           /* either invariant has failed or all reachable states are computed */
02764           /* updates result array */
02765           fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
02766           mdd_free(reachableStates);
02767         }
02768         /* remove the failed invariants from the invariant list. */
02769         if (fail) {
02770           arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
02771             if (invarFormulaStates == NIL(mdd_t)) continue;
02772             /* free the failed invariant mdds */
02773             if (resultArray[j] == 0) {
02774               mdd_free(invarFormulaStates);
02775               array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
02776               if (!debugFlag) {
02777                 (void) fprintf(vis_stdout, "# INV: Early detection - formula failed --- ");
02778                 invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
02779                 Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
02780                 fprintf(vis_stdout, "\n");
02781               }
02782             } else {
02783               someLeft = 1;
02784             }
02785           }
02786         }
02787       } /* end of recomputation dur to over approximate computation */
02788     } while (someLeft);
02789
02790     arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
02791       if (invarFormulaStates == NIL(mdd_t)) continue;
02792       /* free the passed invariant mdds */
02793       mdd_free(invarFormulaStates);
02794     }
02795     array_free(invarStatesArray);
02796     if (printStep) {
02797       finalTime = util_cpu_time();
02798       Fsm_FsmReachabilityPrintResults(modelFsm,finalTime-initTime ,approxFlag);
02799     }
02800     /* free the Fsm if it was reduced here */
02801     if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
02802
02803
02804     PrintInvPassFail(formulas, resultArray);
02805
02806
02807     arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
02808       Ctlp_FormulaFree(invarFormula);
02809     }
02810     array_free(formulas);
02811     FREE(resultArray);
02812   } /* end of processing the sorted array of array of invariants */
02813
02814   if(hintsStatesArray != NIL(array_t))
02815     mdd_array_free(hintsStatesArray);
02816   if(hintsArray)
02817     Ctlp_FormulaArrayFree(hintsArray);
02818   array_free(careSetArray);
02819   array_free(fsmArray);
02820   array_free(sortedFormulaArray);
02821   array_free(invarNormalFormulaArray);
02822   (void) fprintf(vis_stdout, "\n");
02823
02824   if (options->FAFWFlag) {
02825     st_free_table(systemVarBddIdTable);
02826   }
02827
02828   Ctlp_FormulaArrayFree(invarArray);
02829   McOptionsFree(options);
02830   mdd_free(tautology);
02831
02832   alarm(0);
02833   return 0;
02834 }
02835
02836
02844 static McOptions_t *
02845 ParseInvarOptions(
02846   int argc,
02847   char **argv)
02848 {
02849   unsigned int i;
02850   int c;
02851   boolean useMore = FALSE;
02852   boolean reduceFsm = FALSE;
02853   boolean printInputs = FALSE;
02854   boolean useFormulaTree = FALSE;
02855   FILE *inputFp=NIL(FILE);
02856   FILE *debugOut=NIL(FILE);
02857   char *debugOutName=NIL(char);
02858   McDbgLevel dbgLevel = McDbgLevelNone_c;
02859   Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
02860   int timeOutPeriod = 0;
02861   McOptions_t *options = McOptionsAlloc();
02862   int approxFlag = 0, ardc = 0, shellFlag = 0;
02863   Fsm_RchType_t rchType;
02864   FILE *guideFile;
02865   FILE *systemFile = NIL(FILE);
02866   boolean FAFWFlag = FALSE;
02867   boolean GFAFWFlag = FALSE;
02868   char *guideFileName = NIL(char);
02869   char *variablesForSystem = NIL(char);
02870   int incre, speed;
02871   /* int sss; */
02872
02873   /*
02874    * Parse command line options.
02875    */
02876
02877   util_getopt_reset();
02878   while ((c = util_getopt(argc, argv, "ifcrt:g:hmv:d:A:DO:Ww:I:SPs:")) != EOF) {
02879     switch(c) {
02880       case 'g':
02881         guideFileName = util_strsav(util_optarg);
02882         break;
02883       case 'h':
02884         goto usage;
02885       case 't':
02886         timeOutPeriod = atoi(util_optarg);
02887         break;
02888       case 'v':
02889         for (i = 0; i < strlen(util_optarg); i++) {
02890           if (!isdigit((int)util_optarg[i])) {
02891             goto usage;
02892           }
02893         }
02894         verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
02895         break;
02896       case 'd':
02897         for (i = 0; i < strlen(util_optarg); i++) {
02898           if (!isdigit((int)util_optarg[i])) {
02899             goto usage;
02900           }
02901         }
02902         dbgLevel = (McDbgLevel) atoi(util_optarg);
02903         break;
02904       case 'f':
02905         shellFlag = 1;
02906         break;
02907       case 'r' :
02908         reduceFsm = TRUE;
02909         break;
02910       case 'm':
02911         useMore = TRUE;
02912         break;
02913       case 'i' :
02914         printInputs = TRUE;
02915         break;
02916       case 'c' :
02917         useFormulaTree = TRUE;
02918         break;
02919       case 'A':
02920         approxFlag = atoi(util_optarg);
02921         if ((approxFlag > 4) || (approxFlag < 0)) {
02922             goto usage;
02923         }
02924         break;
02925       case 'D':
02926         ardc = 1;
02927         break;
02928       case 'O':
02929         debugOutName = util_strsav(util_optarg);
02930         break;
02931       case 'w':
02932         variablesForSystem = util_strsav(util_optarg);
02933       case 'W':
02934         FAFWFlag = 1;
02935         break;
02936       case 'G':
02937         GFAFWFlag = 1;
02938         break;
02939       case 'I':
02940         incre = atoi(util_optarg);
02941         options->incre = (incre==0)? FALSE:TRUE;
02942         break;
02943       case 'S':
02944         /*sss = atoi(util_optarg);*/
02945         /*options->sss = (sss==0)? FALSE:TRUE;*/
02946         options->sss = TRUE;
02947         break;
02948       case 'P':
02949         options->flatIP = TRUE;
02950         break;
02951       case 's':
02952         speed = atoi(util_optarg);
02953         options->IPspeed = speed;
02954         break;
02955       default:
02956         goto usage;
02957     }
02958   }
02959
02960   if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
02961     fprintf(vis_stderr, "** inv warning : -w and -W options are ignored without -d option\n");
02962   }
02963
02964   if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
02965     fprintf(vis_stderr, "** inv warning : -i is recommended with -w or -W option\n");
02966   }
02967
02968   if(FAFWFlag) {
02969     if (bdd_get_package_name() != CUDD) {
02970       fprintf(vis_stderr, "** inv warning : -w and -W option is only available with CUDD\n");
02971       FAFWFlag = 0;
02972       FREE(variablesForSystem);
02973       variablesForSystem = NIL(char);
02974     }
02975   }
02976
02977
02978   /* translate approx flag */
02979   switch(approxFlag) {
02980   case 0: rchType = Fsm_Rch_Bfs_c; break;
02981   case 1: rchType = Fsm_Rch_Hd_c; break;
02982   case 2: rchType = Fsm_Rch_Oa_c; break;
02983   case 3: rchType = Fsm_Rch_Grab_c; break;
02984   case 4: rchType = Fsm_Rch_PureSat_c; break;
02985   default: rchType = Fsm_Rch_Default_c; break;
02986   }
02987
02988   if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
02989     fprintf(vis_stderr, "** inv error: check_invariant with -A 1 option is currently supported by only CUDD.\n");
02990     return NIL(McOptions_t);
02991   }
02992
02993   if (rchType == Fsm_Rch_Oa_c) {
02994     if (dbgLevel > 0) {
02995       fprintf(vis_stdout, "Over approximation and debug level 1 are incompatible\n");
02996       fprintf(vis_stdout, "Read check_invariant help page\n");
02997       goto usage;
02998     } else if (shellFlag == 1) {
02999       fprintf(vis_stdout, "Over approximation and shell flag are incompatible\n");
03000       fprintf(vis_stdout, "Read check_invariant help page\n");
03001       goto usage;
03002     }
03003   }
03004
03005   if (rchType == Fsm_Rch_Grab_c) {
03006     if (guideFileName != NIL(char)) {
03007       fprintf(vis_stdout, "Abstraction refinement Grab and guided search are incompatible\n");
03008       fprintf(vis_stdout, "Read check_invariant help page\n");
03009       goto usage;
03010     }
03011   }
03012
03013   if (rchType == Fsm_Rch_PureSat_c) {
03014     if (guideFileName != NIL(char)) {
03015       fprintf(vis_stdout, "Abstraction refinement PureSat and guided search are incompatible\n");
03016       fprintf(vis_stdout, "Read check_invariant help page\n");
03017       goto usage;
03018     }
03019   }
03020
03021   if (guideFileName != NIL(char)) {
03022     guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
03023     FREE(guideFileName);
03024     if (guideFile == NIL(FILE)) {
03025       McOptionsFree(options);
03026       return NIL(McOptions_t);
03027     }
03028     McOptionsSetGuideFile(options, guideFile);
03029   }
03030
03031   /*
03032    * Open the ctl file.
03033    */
03034   if (argc - util_optind == 0) {
03035     (void) fprintf(vis_stderr, "** inv error: file containing invariant formulas not provided\n");
03036     goto usage;
03037   }
03038   else if (argc - util_optind > 1) {
03039     (void) fprintf(vis_stderr, "** inv error: too many arguments\n");
03040     goto usage;
03041   }
03042
03043   McOptionsSetUseMore(options, useMore);
03044   McOptionsSetReduceFsm(options, reduceFsm);
03045   McOptionsSetPrintInputs(options, printInputs);
03046   McOptionsSetUseFormulaTree(options, useFormulaTree);
03047   McOptionsSetTimeOutPeriod(options, timeOutPeriod);
03048   McOptionsSetInvarApproxFlag(options, rchType);
03049   if (ardc)
03050     McOptionsSetDcLevel(options, McDcLevelArdc_c);
03051   else
03052     McOptionsSetDcLevel(options, McDcLevelNone_c);
03053   McOptionsSetInvarOnionRingsFlag(options, shellFlag);
03054   McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
03055
03056   inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
03057   if (inputFp == NIL(FILE)) {
03058     McOptionsFree(options);
03059     return NIL(McOptions_t);
03060   }
03061   McOptionsSetCtlFile(options, inputFp);
03062
03063   if (debugOutName != NIL(char)) {
03064     debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
03065     if (debugOut == NIL(FILE)) {
03066       McOptionsFree(options);
03067       return NIL(McOptions_t);
03068     }
03069   }
03070   McOptionsSetDebugFile(options, debugOut);
03071
03072   if ((verbosityLevel != McVerbosityNone_c) &&
03073        (verbosityLevel != McVerbosityLittle_c) &&
03074        (verbosityLevel != McVerbositySome_c) &&
03075        (verbosityLevel != McVerbosityMax_c)) {
03076     goto usage;
03077   }
03078   else {
03079     McOptionsSetVerbosityLevel(options, verbosityLevel);
03080   }
03081
03082   if ((dbgLevel != McDbgLevelNone_c) &&
03083        (dbgLevel != McDbgLevelMin_c)) {
03084     if(((rchType == Fsm_Rch_Grab_c) && (dbgLevel == McDbgLevelMinVerbose_c)))
03085     {
03086       McOptionsSetDbgLevel(options, dbgLevel);
03087     }
03088     else
03089     {
03090       if((rchType == Fsm_Rch_PureSat_c) && (options->flatIP == TRUE) && (dbgLevel == McDbgLevelMinVerbose_c))
03091       {
03092         McOptionsSetDbgLevel(options, dbgLevel);
03093       }
03094       else
03095       {
03096         if((rchType == Fsm_Rch_Bfs_c) && (dbgLevel == McDbgLevelMinVerbose_c))
03097         {
03098           McOptionsSetDbgLevel(options, dbgLevel);
03099         }
03100         else
03101         {
03102           goto usage;
03103         }
03104       }
03105     }
03106   }
03107   else {
03108     McOptionsSetDbgLevel(options, dbgLevel);
03109   }
03110
03111   if (variablesForSystem != NIL(char)) {
03112     systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
03113     if (systemFile == NIL(FILE)) {
03114       fprintf(vis_stderr, "** inv error: cannot open system variables file for FAFW %s.\n",
03115               variablesForSystem);
03116       FREE(variablesForSystem);
03117       variablesForSystem = NIL(char);
03118       McOptionsFree(options);
03119       return NIL(McOptions_t);
03120     }
03121     FREE(variablesForSystem);
03122     variablesForSystem = NIL(char);
03123   }
03124   McOptionsSetVariablesForSystem(options, systemFile);
03125
03126
03127   return options;
03128
03129   usage:
03130   (void) fprintf(vis_stderr, "usage: check_invariant [-c][-d dbg_level][-f][-g <hintfile>][-h][-i][-m][-r][-v verbosity_level][-t time_out][-A <number>][-D dc_level] [-O <dbg_out>] <invar_file>\n");
03131   (void) fprintf(vis_stderr, "    -c  avoid sub-formula sharing between formulae\n");
03132   (void) fprintf(vis_stderr, "    -d  <dbg_level>");
03133   (void) fprintf(vis_stderr, "        dbg_level = 0 => no debug output (Default)\n");
03134   (void) fprintf(vis_stderr, "        dbg_level = 1 => print debug trace. (available for all options)\n ");
03135   (void) fprintf(vis_stderr, "        dbg_level = 2 => print debug trace in Aiger format. (available for -A0, -A3, -A4 and -A4 -P)\n");
03136   (void) fprintf(vis_stderr, "    -f \tStore the onion rings at each step.\n");
03137   (void) fprintf(vis_stderr, "    -g <hint_file> \tSpecify file for guided search.\n");
03138   (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
03139   (void) fprintf(vis_stderr, "    -m  pipe debugger output through UNIX utility more\n");
03140   (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to invariant being checked\n");
03141   (void) fprintf(vis_stderr, "    -t <period> Time out period.\n");
03142   (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
03143   (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
03144   (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
03145   (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
03146   (void) fprintf(vis_stderr, "    -A  <number> Use Different types of reachability analysis\n");
03147   (void) fprintf(vis_stderr, "            0 (default) - BFS method.\n");
03148   (void) fprintf(vis_stderr, "            1 - HD method.\n");
03149   (void) fprintf(vis_stderr, "            2 - Over-approximation.\n");
03150   (void) fprintf(vis_stderr, "            3 - Abstraction refinement GRAB.\n");
03151   (void) fprintf(vis_stderr, "    -D  minimize transition relation with ARDCs\n");
03152   (void) fprintf(vis_stderr, "    -O <dbg_out>\n");
03153   (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
03154   (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
03155   (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
03156   (void) fprintf(vis_stderr, "    -w <node file> \tSpecify variables controlled by system.\n");
03157   (void) fprintf(vis_stderr, "    <invar_file> The input file containing invariants to be checked.\n");
03158   (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
03159   (void) fprintf(vis_stderr, "    -I \tSwitch for Incremental SAT solver in PureSAT method abstraction refinement\n");
03160   McOptionsFree(options);
03161
03162   return NIL(McOptions_t);
03163 }
03164
03177 static void
03178 TimeOutHandle(void)
03179 {
03180   int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
03181
03182   if (seconds < mcTimeOut) {
03183     unsigned slack = (unsigned) (mcTimeOut - seconds);
03184     (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
03185     (void) alarm(slack);
03186   } else {
03187     longjmp(timeOutEnv, 1);
03188   }
03189 } /* TimeOutHandle */
03190
03191
03204 static int
03205 UpdateResultArray(mdd_t *reachableStates,
03206                   array_t *invarStatesArray,
03207                   int *resultArray)
03208 {
03209   int i;
03210   mdd_t *invariant;
03211   int fail = 0;
03212   arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
03213     if (invariant == NIL(mdd_t)) continue;
03214     if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
03215       fail = 1;
03216       resultArray[i] = 0;
03217     }
03218   }
03219   return fail;
03220 } /* end of UpdateResultArray */
03221
03222
03232 static void
03233 PrintInvPassFail(array_t *invarFormulaArray,
03234                  int *resultArray)
03235 {
03236   int i;
03237   Ctlp_Formula_t *formula;
03238   fprintf(vis_stdout, "\n# INV: Summary of invariant pass/fail\n");
03239   arrayForEachItem(Ctlp_Formula_t *, invarFormulaArray, i, formula) {
03240     if (resultArray[i]) {
03241       (void) fprintf(vis_stdout, "# INV: formula passed --- ");
03242       Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
03243       fprintf(vis_stdout, "\n");
03244     } else {
03245       (void) fprintf(vis_stdout, "# INV: formula failed --- ");
03246       Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
03247       fprintf(vis_stdout, "\n");
03248     }
03249   }
03250   return;
03251 } /* end of PrintInvPassFail */