src/ltl/ltl.c File Reference

#include "ltlInt.h"
#include <errno.h>

Include dependency graph for ltl.c:

Go to the source code of this file.

Functions
static int	CommandLtlMc (Hrc_Manager_t **hmgr, int argc, char **argv)
static int	CommandLtl2Aut (Hrc_Manager_t **hmgr, int argc, char **argv)
static LtlMcOption_t *	ParseLtlMcOptions (int argc, char **argv)
static LtlMcOption_t *	ParseLtlTestOptions (int argc, char **argv)
static boolean	LtlMcAtomicFormulaCheckSemantics (Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed)
static void	TimeOutHandle (void)
static void	ShuffleMddIdsToTop (mdd_manager *mddManager, array_t *mddIdArray)
void	Ltl_Init (void)
void	Ltl_End (void)
Ltl_Automaton_t *	Ltl_McFormulaToAutomaton (Ntk_Network_t *network, Ctlsp_Formula_t *Formula, int options_algorithm, int options_rewriting, int options_prunefair, int options_iocompatible, int options_directsim, int options_reversesim, int options_directsimMaximize, int options_verbosity, int checkSemantics)
Hrc_Manager_t *	Ltl_McAutomatonToNetwork (Ntk_Network_t *designNetwork, Ltl_Automaton_t *automaton, int verbosity)
boolean	Ltl_FormulaStaticSemanticCheckOnNetwork (Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed)
Ltl_Automaton_t *	LtlMcFormulaToAutomaton (Ntk_Network_t *network, Ctlsp_Formula_t *Formula, LtlMcOption_t *options, int checkSemantics)
void	LtlFsmLoadFairness (Fsm_Fsm_t *compFsm, Fsm_Fairness_t *designFairness, int NumberOfFairSets, int *AutomatonStrength)
LtlMcOption_t *	LtlMcOptionAlloc (void)
void	LtlMcOptionFree (LtlMcOption_t *result)
Variables
static char rcsid[]	UNUSED = "$Id: ltl.c,v 1.74 2009/04/11 01:41:30 fabio Exp $"
static jmp_buf	timeOutEnv

---

Function Documentation

static int CommandLtl2Aut	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

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

Synopsis [Translate LTL formulae given in file into Buechi automata]

CommandName [ltl_to_aut]

CommandSynopsis [translate LTL formulae into Buechi automata]

CommandArguments [ \[-f <ltl_file>\] \[-m <algorithm>\] \[-o <output_file>\] \[-t <output_format>\] \[-w\] \[-b\] \[-p\] \[-d\] \[-r\] \[-i\] \[-M\] \[-v <verbosity>\] \[-h\] ]

CommandDescription [Translate the given LTL formulae into Buechi automata, and output the automaton into a file.

The translation algorithms are the same as the one used in ltl_model_check . However, more flexible combination of the options can be used with this command.

The automaton can be displayed on the screen and written into a file. The format of the output can be dot, blifmv, verilog and smv.

Command options:

-f <ltl_file>

The input file containing LTL formulae.

-m <algorithm>

Specify the algorithm used in LTL formula -> Buechi automaton translation algorithm.

algorithm must be one of the following:

0: GPVW.

1: GPVW+.

2: LTL2AUT.

3: WRING (default).

-o <output_file>

Write the automata into this file.

-t <output_format>

Specify the output format of the automata.

output_format must be one of the following:

0: dot.

1: blif_mv.

2: verilog.

3: all of the formats above (default).

-w

Rewriting the formula before translation.

-b

Boolean minimization during the translation.

-p

Pruning the fair states in the Buechi automaton.

-d

Direct-simulation minimization of the Buechi automaton.

-r

Reverse-simulation minimization of the Buechi automaton.

-i

Minimization based ont the I/O structural information.

-M

Maximize (adding arcs to) Buechi automaton using Direct Simulation.

-v <verbosity_level>

Specify verbosity level. It must be one of the following: 0,1,2,3.

-h

Print the command usage.

]

SideEffects []

Definition at line 1361 of file ltl.c.

{
  array_t        *ltlArray;
  Ctlsp_Formula_t        *ltlFormula;
  LtlTableau_t           *tableau;
  Ltl_Automaton_t        *automaton;
  int            i;
  LtlMcOption_t *options;
  int            verbosity = 0;   /* verbosity level */
  int            algorithm = 0;   /* translation algorithm */
  int            rewriting = 0;   /* simplify Formula by rewriting */
  int            booleanmin = 0;  /* boolean minimization */
  int            prunefair = 0;   /* prune fairness */
  int            iocompatible = 0;/* simplify by io-compatible */
  int            directsim = 0;   /* simplify by Direct simulation */
  int            reversesim = 0;  /* simplify by reverse simulation */
  int            directsimMaximize = 0;   /* simplify by Direct simulation */
  Ntk_Network_t  *network;
  char  *tmpString;
  long           beginTime, finalTime;


  if (!(options = ParseLtlTestOptions(argc, argv))) {
    return 1;
  }
  rewriting = options->rewriting;
  verbosity = options->verbosity;
  algorithm = options->algorithm;
  booleanmin = options->booleanmin;
  prunefair = options->prunefair;
  iocompatible = options->iocompatible;
  directsim = options->directsim;
  reversesim = options->reversesim;
  directsimMaximize = options->directsimMaximize;

  beginTime = util_cpu_time();
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /* Parse the LTL Formulae */
  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (ltlArray != NIL(array_t)) {
    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
    Ctlsp_FormulaArrayFree(ltlArray);
    ltlArray = tmpArray;
  }
  if (ltlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ltl_to_aut error: error in parsing formulas file\n");
    LtlMcOptionFree(options);
    return 1;
  }

  /* For each LTL formula, build a Buechi automaton ... */
  for (i=0; i<array_n(ltlArray); i++) {
    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);
    tmpString = Ctlsp_FormulaConvertToString(ltlFormula);

    /* expand the abbreaviations */
    ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(ltlFormula);
    fprintf(vis_stdout, "\nFormula: %s\n", tmpString);

    /* 1) Simplify the formula by 'Rewriting' */
    if (rewriting) {
      Ctlsp_Formula_t *tmpF = ltlFormula;
      ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
      tmpString = Ctlsp_FormulaConvertToString(ltlFormula);
      Ctlsp_FormulaFree(tmpF);
    }

    /* create the alph_beta table */
    tableau = LtlTableauGenerateTableau(ltlFormula);
    tableau->verbosity = verbosity;
    tableau->algorithm = algorithm;
    tableau->booleanmin = booleanmin;
    /* print out the tableau rules */
    if (verbosity >= McVerbosityMax_c)
      LtlTableauPrint(vis_stdout, tableau);

    /* 2) create the automaton */
    automaton = LtlAutomatonGeneration(tableau);
    automaton->name = tmpString;

    /* 3) minimize the automaton by Pruning fairness */
    if (prunefair) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
    }

    /* 4) minimize the automaton by I/O compatible and dominance */
    if (iocompatible) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nIOC-Minimization:\n");
      }
      while(Ltl_AutomatonMinimizeByIOCompatible(automaton, verbosity));
    }

    /* 5) minimize the automaton by Direct Simulation */
    if (directsim) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nDirSim-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByDirectSimulation(automaton, verbosity);
    }

    /* 6) minimize the automaton by Reverse Simulation */
    if (reversesim) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nRevSim-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByReverseSimulation(automaton, verbosity);
    }

    /* 7/3) minimize the automaton by Pruning fairness */
    if (prunefair) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
    }

    /* 8) add arcs by Direct Simulation, to reduce counter-example length */
    if (directsimMaximize) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
      }
      Ltl_AutomatonMaximizeByDirectSimulation(automaton, verbosity);
    }

    /* print out the Buechi automaton */
    Ltl_AutomatonPrint(automaton, verbosity+1);

    /* write the automaton in a file in the proper format */
    if (options->outputfilename) {
      FILE *fp;
      fp = Cmd_FileOpen( options->outputfilename, (char *)((i==0)?"w":"a"),
                         NIL(char *), 0);
      if (options->outputformat == Aut2File_DOT_c)
        Ltl_AutomatonToDot(fp, automaton, 0);
      else if (options->outputformat == Aut2File_BLIFMV_c)
        Ltl_AutomatonToBlifMv(fp, network, automaton);
      else if (options->outputformat == Aut2File_VERILOG_c)
        Ltl_AutomatonToVerilog(fp, network, automaton);
      else {
        Ltl_AutomatonToDot(fp, automaton, 0);
        Ltl_AutomatonToBlifMv(fp, network, automaton);
        Ltl_AutomatonToVerilog(fp, network, automaton);
      }
      fclose(fp);
    }

    /* Clean-ups: the current formula*/
    Ltl_AutomatonFree((gGeneric) automaton);
    LtlTableauFree(tableau);
    Ctlsp_FormulaFree(ltlFormula);
  }

  /* Clean-ups */
  Ctlsp_FormulaArrayFree(ltlArray);
  LtlMcOptionFree(options);

  finalTime = util_cpu_time();
  fprintf(vis_stdout, "# LTL_TO_AUT time: %10g\n",
          (double)(finalTime-beginTime)/1000.0);

  return 0;             /* normal exit */
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandLtlMc	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

AutomaticStart

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

Synopsis [Check LTL formulae given in file are modeled by flattened network]

CommandName [ltl_model_check]

CommandSynopsis [perform LTL model checking on a flattened network]

CommandArguments [ \[-a <ltl2aut_algorithm>\] \[-b\] \[-d <dbg_level>\] \[-f <dbg_file>\] \[-h\] \[-i\] \[-m\] \[-s\] \[-t <time_out_period>\]\[-v <verbosity_level>\] \[-A <le_method>\] \[-D <dc_level>\] \[-L <lockstep_mode>\] \[-S <schedule>\] \[-F\] \[-X\] \[-Y\] \[-M\] <ltl_file>] \[-Z\]

CommandDescription [Performs LTL model checking on a flattened network. Before calling this command, the user should have initialized the design by calling the command init_verify. Regardless of the options, no 'false positives' or 'false negatives' will occur: the result is correct for the given circuit.

Properties to be verified should be provided as LTL formulae in the file ltl_file. Note that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of LTL formulas, see the VIS CTL and LTL syntax manual.

A formula passes iff it is true for all initial states of the system. Therefore, in the presence of multiple initial states, if a formula fails, the negation of the formula may also fail.

If a formula does not pass, a (potentially partial) proof of failure (referred to as a debug trace) is demonstrated. Fair paths are represented by a finite sequence of states (the stem) leading to a fair cycle, i.e. a cycle on which there is a state from each fairness condition. Whether demostrate the proof or not can be specified (see option -d).

Command options:

-a <ltl2aut_algorithm>

Specify the algorithm used in LTL formula -> Buechi automaton translation.

ltl2aut_algorithm must be one of the following:

0: GPVW.

1: GPVW+.

2: LTL2AUT.

3: WRING (default).

-b

Use boolean minimization during the LTL to Automaton translation.

-d <dbg_level>

Specify whether to demonstrate a counter-example when the system fails a formula being checked.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Generate a counter-example (a path to a fair cycle).

-f <dbg_file>

Write the debugger output to dbg_file.

-h

Print the command usage.

-i

Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.

-m

Pipe debugger output through the UNIX utility more.

-t <timeOutPeriod>

Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-s

Print debug output in the format accepted by the simulate command.

-v <verbosity_level>

Specify verbosity level. This sets the amount of feedback on CPU usage and code status.

verbosity_level must be one of the following:

0: No feedback provided. This is the default.

1: Feedback on code location.

2: Feedback on code location and CPU usage.

-A <le_method>

Specify whether the compositional SCC analysis algorithm, Divide and Compose (DnC), is enabled for language emptiness checking. The DnC algorithm first enumerates fair SCCs in an over-approximated abstract model, and then successively refines them in the more concrete models. Since non-fair SCCs can be ignored in the more concrete models, a potentially large part of the state space are pruned away early on when the computations are cheap.

le_method must be one of the following:

0 : no use of Divide and Compose (Default).

1 : use Divide and Compose.

-D <dc_level>

Specify extent to which don't cares are used to simplify MDDs in model checking. Don't cares are minterms on which the value taken by functions does not affect the computation; potentially, these minterms can be used to simplify MDDs and reduce the time taken to perform model checking.

dc_level must be one of the following:

0 : No don't cares are used.

1 : Use unreachable states as don't cares. This is the default.

2 : Use unreachable states as don't cares and in the EU computation, use 'frontiers' for image computation.

3 : First compute an overapproximation of the reachable states (ARDC), and use that as the cares set. Use `frontiers' for image computation. For help on controlling options for ARDC, look up help on the command: print_ardc_options. Refer to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD December 1996: one is for State Space Decomposition and the other is for Approximate FSM Traversal.

-S <schedule>

Specify schedule for GSH algorithm, which generalizes the Emerson-Lei algorithm and is used to compute greatest fixpoints. The choice of schedule affects the sequence in which EX and EU operators are applied. It makes a difference only when fairness constraints are specified.

<schedule> must be one of the following:

EL : EU and EX operators strictly alternate. This is the default.

EL1 : EX is applied once for every application of all EUs.

EL2 : EX is applied repeatedly after each application of all EUs.

budget : a hybrid of EL and EL2

random : enabled operators are applied in (pseudo-)random order.

off : GSH is disabled, and the old algorithm is used instead. The old algorithm uses the EL , but the termination checks are less sophisticated than in GSH.

-F

Use forward analysis in the computation of the greatest fixpoint. This option is incompatible with -d 1 or higher and can only be used with -D 1.

-L <lockstep_mode>

Use the lockstep algorithm, which is based on fair SCC enumeration.

<lockstep_mode> must be one of the following:

off : Lockstep is disabled. This is the default. Language emptiness is checked by computing a hull of the fair SCCs.

on : Lockstep is enabled.

all : Lockstep is enabled; all fair SCCs are enumerated instead of terminating as soon as one is found. This can be used to study the SCCs of a graph, but it is slower than the default option.

n : (n is a positive integer). Lockstep is enabled and up to n fair SCCs are enumerated. This is less expensive than all , but still less efficient than on , even when n = 1 .

-X

Disable strength reduction (use different decision procedures for strong, weak, and terminal automaton). Strength reduction is the default. Refer to Bloem, Ravi, Somenzi, "Efficient Decision Procedures for LTL Model Checking," CAV99.

-Y

Disable incremental construction of the partition for (MxA). Instead, build a new partition from the scratch. Incremental construction of the partition is the default.

-Z

Add arcs into the Buechi automaton by direct simulation relation, to heuristically reduce the length of shortest counter-example in model checking. Refer to Awedh and Somenze, "Proving More Properties with Bounded Model Checking," CAV04.

-M

Maximize (adding arcs to) Buechi automaton using Direct Simulation.

<ltl_file>

File containing LTL formulas to be model checked.

Related "set" options:

ltl_change_bracket <yes/no>

Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names, therefore CTL* parser does the same thing. However, in some cases a user does not want to change node names in CTL* parsing. Then, use this set option by giving "no". Default is "yes".

See also commands : model_check, approximate_model_check, incremental_ctl_verification ]

Description [First, the LTL formula is parsed and translated into a Buechi automaton (minimization techniques can by applied during the process).

Then, the Buechi Automaton is translated into a Hrc_Node in a newly created Hrc_Manager. flatten_hierarchy/static_order are used to obtain the automaton Network. In this process the same mddManager (as that of the design network) is used.

Now we need to compose the (M x A). We choose to append the automaton network to the design network. Partition is updated (or regenerated) for the composed network.

A new FSM is created and the fairness are loaded in it. The fairness constraints comes from both the design network and the automaton network. Finally we use Mc_FsmCheckLanguageEmptiness() to do the language emptiness checking. "Strength Reduction Technique" -- using different decision procedures for strong, weak, and terminal automaon -- is used.

After the model check, we free everything we created in this command: partition for (MxA), the new FSM, newly-created network nodes, the automaton network as well as the automaton Hrc_Manager.

If necessary, the result mdd (which is the bad state -- a state that leads to a fair path) can be saved. (for example, in the CTL* model checker).]

SideEffects []

Definition at line 866 of file ltl.c.

{
  array_t *ltlArray;
  LtlMcOption_t *options;
  Ctlsp_Formula_t *ltlFormula;
  Ltl_Automaton_t *automaton;
  LtlTableau_t *tableau;
  Hrc_Manager_t *buechiHrcMgr;
  Hrc_Node_t *designNode;
  Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
  Fsm_Fsm_t *compFsm = NIL(Fsm_Fsm_t);
  Ntk_Network_t *designNetwork,*buechiNetwork = NIL(Ntk_Network_t);
  Ntk_Node_t *node1, *node2;
  array_t *modelCareStatesArray;
  lsGen lsgen2;
  lsList nodeList;
  graph_t *partition, *save_partition;
  mdd_t *fairInitStates, *modelCareStates, *mddOne;
  char *designModelName, *name1;
  int i;
  long startLtlMcTime, endLtlMcTime;
  static int timeOutPeriod = 0;

  Img_ResetNumberOfImageComputation(Img_Both_c);

  if (!(options = ParseLtlMcOptions(argc, argv))) {
    return 1;
  }
  timeOutPeriod = options->timeOutPeriod;

  if (options->dbgLevel != 0 && options->direction == McFwd_c) {
    (void) fprintf(vis_stderr, "** ltl_mc error: -d is incompatible with -F\n");
    LtlMcOptionFree(options);
    return 1;
  }
  if (options->dcLevel !=  McDcLevelRch_c && options->direction == McFwd_c) {
    (void) fprintf(vis_stderr, "** ltl_mc error: -F can only be used with -D1\n");
    LtlMcOptionFree(options);
    return 1;
  }

  /* 'designFsm' and 'designNetwork' are for the model */
  designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (designFsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }
  designNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /* Parse LTL formulae */
  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (ltlArray != NIL(array_t)) {
    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
    Ctlsp_FormulaArrayFree(ltlArray);
    ltlArray = tmpArray;
  }
  if (ltlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ltl_mc error: error in parsing formulas from file\n");
    LtlMcOptionFree(options);
    return 1;
  }
  /* Semantic Check of the Ltl formula array on the network */
  arrayForEachItem(Ctlsp_Formula_t *, ltlArray, i, ltlFormula) {
    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(ltlFormula,
                                                 designNetwork, 1)) {
      fprintf(vis_stderr,
              "ltl_mc error: formula semantic check on design fails:\n%s\n",
              error_string());
      Ctlsp_FormulaArrayFree(ltlArray);
      LtlMcOptionFree(options);
      return 1;
    }
  }

  /* Set time out processing (if timeOutPeriod is set) */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "# LTL_MC: Ltl modelchecking - timeout occurred after %d seconds.\n", timeOutPeriod);
      (void) fprintf(vis_stdout, "# LTL_MC: data may be corrupted.\n");
      if (options->verbosity > McVerbosityNone_c) {
        (void) fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c), Img_GetNumberOfImageComputation(Img_Backward_c));
      }
      alarm(0);
      return 1;
    }
  }
  startLtlMcTime = util_cpu_time();

  mddOne = mdd_one(Ntk_NetworkReadMddManager(designNetwork));

  /* Start LTL model checking for each formula */
  for (i=0; i<array_n(ltlArray); i++) {
    st_table *tbl;
    array_t *mddIds;
    lsList rootList;
    int NumberOfFairSet, AutomatonStrength;
    long initialTime, finalTime; /* for checking each formula */
    int nImgComps, nPreComps;

    /* stats */
    if (options->verbosity > McVerbosityNone_c) {
      initialTime = util_cpu_time();
      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
    } else {
      /* to remove uninitialized variable warning */
      initialTime = 0;
      nImgComps = 0;
      nPreComps = 0;
    }
    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);

    /*---------------------------------------------------------------------
     * 1) create the Buechi Automaton/Network/Mdd_Order/Partition in a new
     * Hrc_Manager. It shares nothing with the Design but the mddManager.
     *--------------------------------------------------------------------*/
    automaton = LtlMcFormulaToAutomaton(designNetwork, ltlFormula, options, 1);
    assert(automaton != NIL(Ltl_Automaton_t));

    if (options->noStrengthReduction)
      AutomatonStrength = Mc_Aut_Strong_c /*2*/;
    else
      AutomatonStrength = Ltl_AutomatonGetStrength(automaton);

    /* add arcs by Direct Simulation, to reduce the counter-example length */
    if (options->directsimMaximize) {
#ifdef DEBUG_LTLMC
      if (options->verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, options->verbosity);
        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
      }
#endif
      Ltl_AutomatonMaximizeByDirectSimulation(automaton, options->verbosity);
    }
    NumberOfFairSet = lsLength(automaton->Fair);
    buechiHrcMgr = Ltl_McAutomatonToNetwork(designNetwork, automaton,
                                            options->verbosity);
    assert(buechiHrcMgr != NIL(Hrc_Manager_t));
    tableau = automaton->tableau;
    Ltl_AutomatonFree((gGeneric) automaton);
    LtlTableauFree(tableau);
    buechiNetwork =  Ntk_HrcManagerReadCurrentNetwork(buechiHrcMgr);

    /*---------------------------------------------------------------------
     * 2) build (M x A) by attaching buechiNetwork(A) to designNetwork(M).
     * The result network M x A (designNetwork) shares some data with the
     * buechiNetwork (Variables, and Tables). The newly created nodes in
     * designNetwork retain their MddId in buechiNetwork
     *--------------------------------------------------------------------*/
    /* 2-a) Retrieve the Model (in the default hrc_manager) */
    designNode = Hrc_ManagerReadCurrentNode(*hmgr);
    designModelName = Hrc_NodeReadModelName(designNode);
    /* 2-b) Attach buechiNetwork to designNetwork */
    tbl = st_init_table(strcmp, st_strhash);
    Ntk_NetworkAppendNetwork(designNetwork, buechiNetwork, tbl);
    st_free_table(tbl);

    /* Here we have the choice of incrementally build the partition,
     * or build it from scratch. In both cases, the original partition
     * will be saved (and restored later)
     */
    if (!options->noIncrementalPartition) {
      rootList = lsCreate();
      mddIds = array_alloc(int, 2);
      /* 2-c) Assign MddId to the newly-created nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (!Ntk_NodeTestIsPrimaryInput(node2)) {
          name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
          node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
          Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
          if (!strcmp(name1, "state$AUT$NTK2"))
            array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
          else if (!strcmp(name1, "state$AUT$NS$NTK2"))
            array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
          else if (!strcmp(name1, "selector$AUT$NTK2"))
            array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
          FREE(name1);
          if (Ntk_NodeTestIsCombOutput(node1))
            lsNewEnd(rootList, (lsGeneric)node1, (lsHandle *)0);
        }
      }
      /* move the automaton variables to the top most -- this is believed
       * to be an optimal ordering */
      if (!options->noShuffleToTop)
        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
      array_free(mddIds);

      /* 2-d) Create the Partition information for (M x A) */
      save_partition = Part_NetworkReadPartition(designNetwork);
      partition = Part_PartitionDuplicate(save_partition);
      Part_UpdatePartitionFrontier(designNetwork, partition, rootList,
                                   (lsList)0, mddOne);
      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                             (void *)partition);
      lsDestroy(rootList, (void (*)(lsGeneric))0);

    }else {
      mddIds = array_alloc(int, 2);
      /* 2-c) Assign MddId to the newly-created nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
        if (!strcmp(name1, "state$AUT$NTK2"))
          array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
        else if (!strcmp(name1, "state$AUT$NS$NTK2"))
          array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
        else if (!strcmp(name1, "selector$AUT$NTK2"))
          array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
        FREE(name1);
      }
      /* move the automaton variables to the top most. This might be the
       * best BDD variable ordering for (M x A)! */
      if (!options->noShuffleToTop)
        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
      array_free(mddIds);

      /* 2-d) Create the Partition information for (M x A) */
      nodeList = lsCreate();
      partition = Part_NetworkCreatePartition(designNetwork,
                                              designNode,
                                              designModelName,
                                              (lsList)0,
                                              (lsList)0,
                                              NIL(mdd_t),
                                              Part_Default_c,
                                              nodeList,
                                              FALSE, 0, 0);
      save_partition = Part_NetworkReadPartition(designNetwork);
      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                             (void *)partition);

      lsDestroy(nodeList, (void (*)(lsGeneric))0);
    }

    /*---------------------------------------------------------------------
     * 3) Create the FSM for (M x A) and load Fairness constraints
     *--------------------------------------------------------------------*/
    /* try to get a reduced Fsm (w.r.t. each individual property) first */
    {
      array_t *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
      Ctlp_Formula_t *ctlF = Ctlp_FormulaCreate(Ctlp_ID_c,
                                                util_strsav("state$AUT$NTK2"),
                                                util_strsav("Trap"));
      array_insert(Ctlp_Formula_t *, ctlArray, 0, ctlF);
      compFsm = Mc_ConstructReducedFsm(designNetwork, ctlArray);
      Ctlp_FormulaFree(ctlF);
      array_free(ctlArray);
      if (compFsm == NIL(Fsm_Fsm_t))
        compFsm = Fsm_FsmCreateFromNetworkWithPartition(designNetwork,
                                                        NIL(graph_t));
    }
    /* merge fairnesses from outside and those from the automaton ... */
    LtlFsmLoadFairness(compFsm, Fsm_FsmReadFairnessConstraint(designFsm),
                       NumberOfFairSet, &AutomatonStrength);


    /*---------------------------------------------------------------------
     * 4) Language emptiness checking (store result if necessary)
     *--------------------------------------------------------------------*/
    if (options->dcLevel == McDcLevelArdc_c) {
      Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
      array_t *tmpArray;
      long startRchTime;
      Fsm_ArdcGetDefaultOptions(ardcOptions);
      startRchTime = util_cpu_time();
      tmpArray =
        Fsm_ArdcComputeOverApproximateReachableStates(compFsm, 0,
                                                      options->verbosity,
                                                      0, 0, 0, 0, 0, 0,
                                                      ardcOptions);
      modelCareStatesArray = mdd_array_duplicate(tmpArray);
      FREE(ardcOptions);
      if (options->verbosity > McVerbosityNone_c)
        Fsm_ArdcPrintReachabilityResults(compFsm,
                                         util_cpu_time() - startRchTime);
    }else if (options->dcLevel >= McDcLevelRch_c) {
      long startRchTime;
      startRchTime = util_cpu_time();
      modelCareStates =
        Fsm_FsmComputeReachableStates(compFsm, 0, options->verbosity, 0, 0,
                                      (options->lockstep != MC_LOCKSTEP_OFF),
                                      0, 0, Fsm_Rch_Default_c, 0, 0,
                                      NIL(array_t), FALSE, NIL(array_t));
      if (options->verbosity > McVerbosityNone_c) {
        Fsm_FsmReachabilityPrintResults(compFsm,
                                        util_cpu_time() - startRchTime,
                                        Fsm_Rch_Default_c);
      }
      modelCareStatesArray = array_alloc(mdd_t *, 0);
      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
    } else {
      modelCareStates = mdd_one(Fsm_FsmReadMddManager(compFsm));
      modelCareStatesArray = array_alloc(mdd_t *, 0);
      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
    }
    /*
    Fsm_MinimizeTransitionRelationWithReachabilityInfo(compFsm,
                                                       Img_Backward_c,
                                                       options->verbosity > 1);
    */

    /* language emptiness checking */
    fairInitStates = Mc_FsmCheckLanguageEmptiness(compFsm,
                                                  modelCareStatesArray,
                                                  (Mc_AutStrength_t) AutomatonStrength,
                                                  options->leMethod,
                                                  options->dcLevel,
                                                  options->dbgLevel,
                                                  options->printInputs,
                                                  options->verbosity,
                                                  options->schedule,
                                                  options->direction,
                                                  options->lockstep,
                                                  options->debugFile,
                                                  options->useMore,
                                                  options->simValue,
                                                  "LTL_MC");
    mdd_array_free(modelCareStatesArray);

    if (fairInitStates)
      mdd_free(fairInitStates);

    /*---------------------------------------------------------------------
     * 5) Remove 'A' from designNetwork (M x A), which contains 3 steps:
     * a) free compFsm/partition
     * b) remove newly-created nodes from designNetwork;
     * c) destory buechiHrcMgr (buechiNetwork)
     *--------------------------------------------------------------------*/
    Ntk_NetworkAddApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                           (void *)save_partition);
    Fsm_FsmFree(compFsm);
    {
      int tmpi, tmpj;
      Ntk_Node_t *node3, *node4;
      /* first, remove the newly-added A nodes ('xxxlabel$AUT$NTK2') from the
       * fanout list of the M nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (strstr(Ntk_NodeReadName(node2), "label$AUT") == NULL)
          continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        FREE(name1);
        assert(node1);
        Ntk_NodeForEachFanin(node1, tmpi, node3) {
          array_t *oldFanouts = Ntk_NodeReadFanouts(node3);
          array_t *newFanouts;
          if (oldFanouts != NIL(array_t)) {
            newFanouts = array_alloc(Ntk_Node_t *, 0);
            arrayForEachItem(Ntk_Node_t *, oldFanouts, tmpj, node4) {
              if (node4 != node1)
                array_insert_last(Ntk_Node_t *, newFanouts, node4);
            }
            Ntk_NodeSetFanouts(node3, newFanouts);
          }
        }
      }
      /* Now we can safely remove all the newly-added A nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        FREE(name1);
        Ntk_NodeRemoveFromNetwork(designNetwork, node1, 1, 1, 0);
        Ntk_NodeFree(node1);
      }
    }
    Ntk_NetworkSetMddManager(buechiNetwork, (mdd_manager *)0);
    Hrc_ManagerFree(buechiHrcMgr);

    if (options->verbosity > McVerbosityNone_c) {
      finalTime = util_cpu_time();
      fprintf(vis_stdout, "-- ltl_mc time = %10g\n",
        (double)(finalTime - initialTime) / 1000.0);
      fprintf(vis_stdout,
              "-- %d image computations and %d preimage computations\n",
              Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
              Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
    }
  }

  /* Print stats if verbose. */
  endLtlMcTime = util_cpu_time();
  if (options->verbosity > McVerbosityNone_c) {
    fprintf(vis_stdout, "-- total ltl_mc time: %10g\n",
            (double)(endLtlMcTime-startLtlMcTime)/1000.0);
    fprintf(vis_stdout,
            "-- total %d image computations and %d preimage computations\n",
            Img_GetNumberOfImageComputation(Img_Forward_c),
            Img_GetNumberOfImageComputation(Img_Backward_c));
  }

  /* Clean-ups */
  Ctlsp_FormulaArrayFree(ltlArray);
  LtlMcOptionFree(options);
  mdd_free(mddOne);

  alarm(0);
  return 0;             /* normal exit */
}

Here is the caller graph for this function:

void Ltl_End

(

void

)

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

Synopsis [Ends the Ltl package.]

SideEffects []

SeeAlso [Ltl_Init]

Definition at line 100 of file ltl.c.

{
}

Here is the caller graph for this function:

boolean Ltl_FormulaStaticSemanticCheckOnNetwork	(	Ctlsp_Formula_t *	formula,
		Ntk_Network_t *	network,
		boolean	inputsAllowed
	)

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

Synopsis [Perform static semantic check of ltl formula on network.]

Description [Perform static semantic check of ltl formula on network. Specifically, given an atomic formula of the form LHS=RHS, check that the LHS is the name of a latch/wire in the network, and that RHS is of appropriate type (enum/integer) and is lies in the range of the latch/wire values. If LHS is a wire, and inputsAllowed is false, check to see that the algebraic support of the wire consists of only latches and constants.]

SideEffects []

Definition at line 251 of file ltl.c.

{
  boolean lCheck;
  boolean rCheck;
  Ctlsp_Formula_t *leftChild;
  Ctlsp_Formula_t *rightChild;

  if(formula == NIL(Ctlsp_Formula_t)){
    return TRUE;
  }

  if(Ctlsp_FormulaReadType(formula) == Ctlsp_ID_c){
    return LtlMcAtomicFormulaCheckSemantics(formula, network, inputsAllowed);
  }

  leftChild = Ctlsp_FormulaReadLeftChild(formula);
  rightChild = Ctlsp_FormulaReadRightChild(formula);

  lCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
                                                   inputsAllowed);
  if(!lCheck)
    return FALSE;

  rCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
                                                   inputsAllowed);
  if (!rCheck)
    return FALSE;

  return TRUE;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Ltl_Init

(

void

)

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

Synopsis [Initializes the Ltl package.]

SideEffects []

SeeAlso [Ltl_End]

Definition at line 75 of file ltl.c.

{
  /* LTL model checking. Before using this command, the design must be read
   * and 'init_verify' has been executed.
   */
  Cmd_CommandAdd("ltl_model_check", CommandLtlMc,  0);

  /* Test the LTL->Buechi Automaton Translator, may or may not need to read
   * the design. But If the design is read, the semantic of the formula
   * will be checked on the model before translation
   */
  Cmd_CommandAdd("ltl_to_aut", CommandLtl2Aut, 0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Hrc_Manager_t* Ltl_McAutomatonToNetwork	(	Ntk_Network_t *	designNetwork,
		Ltl_Automaton_t *	automaton,
		int	verbosity
	)

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

Synopsis [Translate the Buechi automaton into a network.]

Description [A new Hrc_Manager_t is created, in which the network will be stored. The translation goes as the following:

1) translate the Buechi automaton into a temp file (in blifmv format); 2) read in the temp file (into the new hrcMgr) by default blifmv parser 3) flatten_hierarchy to get the network ]

SideEffects [The returned Hrc_Manager_t should be freed by the caller.]

SeeAlso []

Definition at line 176 of file ltl.c.

{
  FILE *fp;
  Hrc_Manager_t *buechiHrcMgr;
  Hrc_Node_t    *buechiHrcNode;
  Ntk_Network_t *buechiNetwork;
  int flag;

  /* 1) translate the automaton to a temporary blif_mv file */
  fp = tmpfile();
  if (fp == NIL(FILE)) {
    fail("Aut->Ntk: can't open temp file");
  }
#ifdef DEBUG_LTLMC
  if (verbosity >= 2) {
    fprintf(vis_stdout, "\nPrint the automaton Blif_Mv file:\n");
    flag = Ltl_AutomatonToBlifMv(vis_stdout, designNetwork, automaton);
    fprintf(vis_stdout, "\n");
    fflush(vis_stdout);
  }
#endif
  flag = Ltl_AutomatonToBlifMv(fp, designNetwork, automaton);
  if (!flag) {
    return NIL(Hrc_Manager_t);
  }

  /* 2) read and parse the tmp blifmv file */
  rewind(fp);
  error_init();
  buechiHrcMgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), 0, 0, 0);
  fclose(fp);
  if (buechiHrcMgr == NIL(Hrc_Manager_t))
    fail(error_string());

  /* 3) flatten_hierarchy */
  buechiHrcNode = Hrc_ManagerReadCurrentNode(buechiHrcMgr);
  buechiNetwork = Ntk_HrcNodeConvertToNetwork(buechiHrcNode, TRUE, (lsList)0);
  Hrc_NodeAddApplInfo(buechiHrcNode, NTK_HRC_NODE_APPL_KEY,
                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
                      (Hrc_ApplInfoChangeFn) NULL,
                      (void *) buechiNetwork);

  /* 4) static_order (!!! using the default mddManager) */
  Ntk_NetworkSetMddManager(buechiNetwork,
                           Ntk_NetworkReadMddManager(designNetwork));
  Ord_NetworkOrderVariables(buechiNetwork,
                            Ord_RootsByDefault_c,
                            Ord_NodesByDefault_c,
                            FALSE,
                            Ord_InputAndLatch_c,
                            Ord_Unassigned_c,
                            (lsList)NULL,
                            0);

  return buechiHrcMgr;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ltl_Automaton_t* Ltl_McFormulaToAutomaton	(	Ntk_Network_t *	network,
		Ctlsp_Formula_t *	Formula,
		int	options_algorithm,
		int	options_rewriting,
		int	options_prunefair,
		int	options_iocompatible,
		int	options_directsim,
		int	options_reversesim,
		int	options_directsimMaximize,
		int	options_verbosity,
		int	checkSemantics
	)

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

Synopsis [Translate the LTL formula into a Buechi automaton.]

Description [The wrapper of LtlMcFormulaToAutomaton.]

SideEffects [The returned automaton should be freed by the caller.]

SeeAlso [LtlMcFormulaToAutomaton]

Definition at line 117 of file ltl.c.

{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  Ltl_Automaton_t *aut;

  options->algorithm = (Ltl2AutAlgorithm) options_algorithm;
  if (options_algorithm == Ltl2Aut_WRING_c) {
    options->rewriting = 1;
    options->prunefair = 1;
    options->iocompatible = 1;
    options->directsim = 1;
    options->reversesim = 1;
  }else {
    options->rewriting = options_rewriting;
    options->prunefair = options_prunefair;
    options->iocompatible = options_iocompatible;
    options->directsim = options_directsim;
    options->reversesim = options_reversesim;
  }
  options->directsimMaximize = options_directsimMaximize;
  options->verbosity = (Mc_VerbosityLevel) options_verbosity;

  aut = LtlMcFormulaToAutomaton(network, Formula, options, checkSemantics);

  LtlMcOptionFree(options);

  return aut;
}

Here is the call graph for this function:

void LtlFsmLoadFairness	(	Fsm_Fsm_t *	compFsm,
		Fsm_Fairness_t *	designFairness,
		int	NumberOfFairSets,
		int *	AutomatonStrength
	)

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

Synopsis [Load the Fairness Constraint for the compFsm.]

Description [The fairness constraint comes from two places: 1) the fairness constraints on the model (designFairness); 2) the fairsets from the Buechi automaton (the LTL formula). AutomatonStrength is unchanged unless there are external fairness and the automaton is terminal (in which case the strength is assumed to be "1-weak".]

SideEffects [*AutomatonStrength might be changed.]

Definition at line 460 of file ltl.c.

{
  array_t *fairformulaArray;
  Ctlp_Formula_t *F;
  int j;

  /* The fairness constraint on the model (before ltl_model_check is invoked)
   * should be Buechi fairness
   */
  if (!Fsm_FairnessTestIsBuchi(designFairness)) {
    fprintf(vis_stderr, "ltl_mc error: Can not handle non-Buchi Fairness \n");
    assert(0);
  }

  /* store the new fairness constraint (for compFsm) */
  fairformulaArray = array_alloc(Ctlp_Formula_t *, 0);

  /* copy the fairness constraints from the automaton */
  if (*AutomatonStrength == Mc_Aut_Strong_c/*2*/) {
    if (NumberOfFairSets > 0) {
      for (j=0; j<NumberOfFairSets; j++) {
        char tmpstr[30];
        sprintf(tmpstr, "fair%d$AUT$NTK2", j+1);
        F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav(tmpstr),
                               (void *)util_strsav("1"));
        array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
      }
    }else {
      F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav("fair1$AUT$NTK2"),
                             (void *)util_strsav("1"));
      array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
    }
  }

  /* copy the fairness constraints on the model */
  for (j=0; j<Fsm_FairnessReadNumConjunctsOfDisjunct(designFairness, 0); j++) {
    F = Fsm_FairnessReadFinallyInfFormula(designFairness, 0, j);
    if (array_n(fairformulaArray) && Ctlp_FormulaReadType(F) == Ctlp_TRUE_c)
      continue;
    array_insert_last(Ctlp_Formula_t *,fairformulaArray, Ctlp_FormulaDup(F));
  }

  /* this is a conservative conclusion ! */
  if (*AutomatonStrength == Mc_Aut_Terminal_c /*0*/) {
    F = array_fetch(Ctlp_Formula_t *, fairformulaArray, 0);
    if (array_n(fairformulaArray) > 1 ||
        Ctlp_FormulaReadType(F) != Ctlp_TRUE_c) {
      *AutomatonStrength = Mc_Aut_Weak_c /*1*/;
    }
  }

  /* update the fairness constraints on 'compFsm' */
  Fsm_FsmFairnessUpdate(compFsm, fairformulaArray);

  array_free(fairformulaArray);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static boolean LtlMcAtomicFormulaCheckSemantics	(	Ctlsp_Formula_t *	formula,
		Ntk_Network_t *	network,
		boolean	inputsAllowed
	)		[static]

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

Synopsis [Perform simple static semantic checks on formula.]

SideEffects []

SeeAlso [Ltl_FormulaStaticSemanticCheckOnNetwork]

Definition at line 1883 of file ltl.c.

{
  char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
  char *nodeValueString = Ctlsp_FormulaReadValueName( formula );
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );

  Var_Variable_t *nodeVar;
  int nodeValue;

  if ( !node ) {
    error_append("Could not find node corresponding to the name\n\t- ");
    error_append( nodeNameString );
    return FALSE;
  }

  nodeVar = Ntk_NodeReadVariable( node );
  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
    if ( nodeValue == -1 ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }
  else {
    int check;

    check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
    if( check==0 ) {
      error_append("Value in the RHS is illegal\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if( check==1 ) {
      error_append("Value in the RHS is out of range of int\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }

  if(!inputsAllowed){
    boolean coverSupport;
    lsGen tmpGen;
    Ntk_Node_t *tmpNode;
    st_table *supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
    array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);

    array_insert_last( Ntk_Node_t *, thisNodeArray, node );
    Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
      if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
        st_insert(supportNodes,  tmpNode, NIL(char));
      }
    }

    coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
                                                            thisNodeArray,
                                                            supportNodes);
    array_free(thisNodeArray);
    st_free_table(supportNodes);

    if ( coverSupport == FALSE ) {
      char *tmpString =
        util_strcat3( "\nNode ", nodeNameString,
                      " is not driven only by latches and constants.\n");
      error_append(tmpString);
      return FALSE;
    }
  }

  return TRUE;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ltl_Automaton_t* LtlMcFormulaToAutomaton	(	Ntk_Network_t *	network,
		Ctlsp_Formula_t *	Formula,
		LtlMcOption_t *	options,
		int	checkSemantics
	)

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

Synopsis [Translate the LTL formula to a Buechi automaton.]

Description [State-of-the-art Optiomization/Minimization is used to shrink the size of the automaton: 1) Rewriting the Formula (before translation) 2) Boolean Minimization (during translation) 3) Automaton Minimization (after translation)

• prune fair states
• simulation-based minimization (io/direct/reverse)

For more information, refer to: Fabio Somenzi and Roderick Bloem,"Efficient Buechi Automaton from LTL Formula," CAV'00.

Before translation, the sementics of the formula is checked on the model. In the case it fails, a NIL pointer will be returned.]

SideEffects [The returned automaton should be freed by the caller.]

SeeAlso []

Definition at line 315 of file ltl.c.

{

  char *tmpString;
  Ctlsp_Formula_t *ltlFormula, *negFormula;
  LtlTableau_t *tableau;
  Ltl_Automaton_t *automaton;

  /* check the semantic of the formula on the given network */
  if (checkSemantics && network != NIL(Ntk_Network_t)) {
    if (!network) {
      fprintf(vis_stderr,
              "ltl_mc error: empty network. use flatten_hierarchy\n");
      return NIL(Ltl_Automaton_t);
    }
    error_init();
    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(Formula, network, 1)) {
      fprintf(vis_stderr,
              "ltl_mc error: formula semantic check on design fails:\n%s\n",
              error_string());
      return NIL(Ltl_Automaton_t);
    }
  }

  /* print out the given LTL formula */
  fprintf(vis_stdout, "Formula: ");
  Ctlsp_FormulaPrint(vis_stdout, Formula);
  fprintf(vis_stdout, "\n");

  /* Negate Formula and Expand the abbreaviations */
  negFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, Formula, NIL(Ctlsp_Formula_t));
  ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negFormula);
  tmpString = Ctlsp_FormulaConvertToString(negFormula);
  FREE(negFormula);
#ifdef DEBUG_LTLMC
  if (options->verbosity)
    fprintf(vis_stdout, "\nNegation Print: %s\n", tmpString);
#endif

  /* 1) Simplify the formula by 'Rewriting' */
  if (options->rewriting) {
    Ctlsp_Formula_t *tmpF = ltlFormula;
    ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
    Ctlsp_FormulaFree(tmpF);
  }

  /* create the alph_beta table */
  tableau = LtlTableauGenerateTableau(ltlFormula);
  tableau->verbosity = options->verbosity;
  tableau->algorithm = options->algorithm;
  tableau->booleanmin = options->booleanmin;
#ifdef DEBUG_LTLMC
  /* print out the tableau rules */
  if (options->verbosity > 1)
    LtlTableauPrint(vis_stdout, tableau);
#endif

  /* we dont' need this formula any more */
  Ctlsp_FormulaFree(ltlFormula);


  /* 2) create the automaton */
  automaton = LtlAutomatonGeneration(tableau);
  automaton->name = tmpString;

  /* 3-1) minimize the automaton by Pruning fairness */
  if (options->prunefair) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
  }

  /* 3-2) minimize the automaton by I/O compatible and dominance */
  if (options->iocompatible) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nIOC-Minimization:\n");
    }
#endif
    while(Ltl_AutomatonMinimizeByIOCompatible(automaton,options->verbosity));
  }

  /* 3-3) minimize the automaton by Direct Simulation */
  if (options->directsim) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nDirSim-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByDirectSimulation(automaton, options->verbosity);
  }

  /* 3-4) minimize the automaton by Direct Simulation */
  if (options->reversesim) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nRevSim-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByReverseSimulation(automaton, options->verbosity);
  }

  /* 3-5) minimize the automaton by Pruning fairness */
  if (options->prunefair) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
  }
  /* print out the Buechi automaton */
  if (options->verbosity) {
    Ltl_AutomatonPrint(automaton, options->verbosity);
  }

  return automaton;
}

Here is the call graph for this function:

Here is the caller graph for this function:

LtlMcOption_t* LtlMcOptionAlloc

(

void

)

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

Synopsis [Alloc Memory for LtlMcOption_t.]

SideEffects []

SeeAlso []

Definition at line 530 of file ltl.c.

{
  LtlMcOption_t *result = ALLOC(LtlMcOption_t, 1);
  if (result == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);
  memset(result, 0, sizeof(LtlMcOption_t));

  result->algorithm = Ltl2Aut_WRING_c;
  result->schedule = McGSH_EL_c;
  result->lockstep = MC_LOCKSTEP_OFF;
  result->outputformat = Aut2File_ALL_c;

  return result;
}

Here is the caller graph for this function:

void LtlMcOptionFree

(

LtlMcOption_t *

result

)

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

Synopsis [Free LtlMcOption_t, and close the ltl formula file.]

SideEffects []

SeeAlso []

Definition at line 554 of file ltl.c.

{
  if (result->ltlFile)
    fclose(result->ltlFile);

  if (result->debugFile)
    fclose(result->debugFile);

  if (result->outputfilename)
    FREE(result->outputfilename);

  FREE(result);
}

Here is the caller graph for this function:

static LtlMcOption_t * ParseLtlMcOptions	(	int	argc,
		char **	argv
	)		[static]

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

Synopsis [Parse the user input for command "ltl_model_check."]

Description []

SideEffects []

Definition at line 1550 of file ltl.c.

{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  char *ltlFileName = (char *)0;
  char *debugOutName = (char *)0;
  Mc_GSHScheduleType schedule = McGSH_EL_c;
  Mc_FwdBwdAnalysis direction = McBwd_c;
  int lockstep = MC_LOCKSTEP_OFF;
  int c;

  if (options == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);
  options->leMethod = Mc_Le_Default_c;
  options->dcLevel = McDcLevelRch_c;
  options->noStrengthReduction = 0;
  options->noIncrementalPartition = 0;

  /* Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "a:bd:f:t:A:D:v:S:L:FhimsXYM")) != EOF) {
    switch(c) {
    case 'a':
      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
      if (options->algorithm < 0 || options->algorithm > 3)
        goto usage;
      break;
    case 'b':
      options->booleanmin = 1;
      break;
    case 'd':
      options->dbgLevel = (LtlMcDbgLevel) atoi(util_optarg);
      break;
    case 'f':
      debugOutName = util_strsav(util_optarg);
      break;
    case 't':
      options->timeOutPeriod = atoi(util_optarg);
      break;
    case 'A':
      options->leMethod = (Mc_LeMethod_t) atoi(util_optarg);
      break;
    case 'D':
      options->dcLevel = (Mc_DcLevel) atoi(util_optarg);
      break;
    case 'v':
      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'S' :
      schedule = Mc_StringConvertToScheduleType(util_optarg);
      break;
    case 'L' :
      lockstep = Mc_StringConvertToLockstepMode(util_optarg);
      break;
    case 'F' :
      direction = McFwd_c;
      break;
    case 'i':
      options->printInputs = 1;
      break;
    case 'm':
      options->useMore = TRUE;
      break;
    case 's' :
      options->simValue = TRUE;
      break;
    case 'X':
      options->noStrengthReduction = 1;
      break;
    case 'Y':
      options->noIncrementalPartition = 1;
      break;
    case 'Z':
      options->noShuffleToTop = 1;
      break;
    case 'M':
      options->directsimMaximize = 1;
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
    }
  }
  if (options->algorithm == Ltl2Aut_WRING_c) {
    options->rewriting =    TRUE;
    options->prunefair =    TRUE;
    options->directsim =    TRUE;
    options->reversesim =   TRUE;
    options->iocompatible = TRUE;
  }

  if (schedule == McGSH_Unassigned_c) {
    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
    goto usage;
  } else {
    options->schedule = schedule;
  }
  if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
    (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
    goto usage;
  } else {
    options->lockstep = lockstep;
  }
  options->direction = direction;

  /* Open the ltl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** ltl_mc error: file containing ltl formulae not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** ltl_mc error: too many arguments\n");
    goto usage;
  }
  ltlFileName = util_strsav(argv[util_optind]);

  /* Read LTL Formulae */
  if (!ltlFileName)
    goto usage;
  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  if (options->ltlFile == NIL(FILE)) {
    (void) fprintf(vis_stdout,  "** ltl_mc error: error in opening file %s\n", ltlFileName);
    FREE(ltlFileName);
    LtlMcOptionFree(options);
    return NIL(LtlMcOption_t);
  }
  FREE(ltlFileName);

  if (debugOutName != NIL(char)) {
    options->debugFile = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
    if (options->debugFile == NIL(FILE)) {
      (void) fprintf(vis_stdout,"** ltl_mc error: error in opening file %s\n", debugOutName);
      FREE(debugOutName);
      LtlMcOptionFree(options);
      return NIL(LtlMcOption_t);
    }
    FREE(debugOutName);
  }

  return options;

 usage:
  (void) fprintf(vis_stderr, "usage: ltl_model_check [-a ltl2aut_algorithm][-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A le_method][-D dc_level][-L lockstep_mode][-S schedule][-F][-X][-Y][-M] <ltl_file>\n");
  (void) fprintf(vis_stderr, "    -a <ltl2aut_algorithm>\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 0 => GPVW\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 1 => GPVW+\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 2 => LTL2AUT\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 3 => WRING (Default)\n");
  (void) fprintf(vis_stderr, "    -b \tUse boolean minimization in automaton generation\n");
  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
  (void) fprintf(vis_stderr, "        debug_level = 1 => automatic debugging\n");
  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "    -m \tPipe debugger output through the UNIX utility more.\n");
  (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
  (void) fprintf(vis_stderr, "    -t <period> time out period\n");
  (void) fprintf(vis_stderr, "    -A <le_method>\n");
  (void) fprintf(vis_stderr, "        le_method = 0 => no use of Divide and Compose (Default)\n");
  (void) fprintf(vis_stderr, "        le_method = 1 => use Divide and Compose\n");
  (void) fprintf(vis_stderr, "    -D <dc_level>\n");
  (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
  (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
  (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");

  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
  (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
  (void) fprintf(vis_stderr, "    -L <lockstep_mode>\n");
  (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");
  (void) fprintf(vis_stderr, "    -S <schedule>\n");
  (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
  (void) fprintf(vis_stderr, "    -F \tUse forward analysis in fixpoint computation.\n");
  (void) fprintf(vis_stderr, "    -X \tDisable strength reduction (using different decision procedure \n");
  (void) fprintf(vis_stderr, "       \tfor strong, weak, terminal automaton).\n");
  (void) fprintf(vis_stderr, "    -Y \tDisable incremental partition of the composed system (M x A).\n");
  (void) fprintf(vis_stderr, "    -Z \tAdd arcs into the Buechi automaton by direct simulation relation.\n");

  (void) fprintf(vis_stderr, "    -M \tAdd arcs to the automaton to reduce counter-example length.\n");
  (void) fprintf(vis_stderr, "    <ltl_file> The input file containing LTL formulae to be checked.\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");

  LtlMcOptionFree(options);
  return NIL(LtlMcOption_t);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static LtlMcOption_t * ParseLtlTestOptions	(	int	argc,
		char **	argv
	)		[static]

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

Synopsis [Parse the user input for command "ltl_to_aut".]

Description []

SideEffects []

Definition at line 1755 of file ltl.c.

{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  char *ltlFileName = (char *)0;
  int c;

  if (options == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "wbpdMrif:m:v:o:t:h")) != EOF) {
    switch(c) {
    case 'w':
      options->rewriting = 1;
      break;
    case 'b':
      options->booleanmin = 1;
      break;
    case 'p':
      options->prunefair = 1;
      break;
    case 'd':
      options->directsim = 1;
      break;
    case 'M':
      options->directsimMaximize = 1;
      break;
    case 'r':
      options->reversesim = 1;
      break;
    case 'i':
      options->iocompatible = 1;
      break;
    case 'f':
      ltlFileName = util_strsav(util_optarg);
      break;
    case 'm':
      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
      break;
    case 'v':
      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'o':
      options->outputfilename = util_strsav(util_optarg);
      break;
    case 't':
      options->outputformat = (Aut2FileType) atoi(util_optarg);
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
    }
  }

  /* 'Wring' is equivalent to
  *    LTL2AUT +
  *    rewriting +
  *    prunefair + directsim + reversesim + iocompatible
  */
  if (options->algorithm ==3) {
    options->rewriting = 1;
    options->prunefair = 1;
    options->directsim = 1;
    options->reversesim = 1;
    options->iocompatible = 1;
  }

  /* Read LTL Formulae */
  if (!ltlFileName)
    goto usage;

  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  FREE(ltlFileName);
  if (options->ltlFile == NIL(FILE)) {
    (void) fprintf(vis_stdout,  "** ltl_to_aut error: error in opening file %s\n", ltlFileName);
    LtlMcOptionFree(options);
    return NIL(LtlMcOption_t);
  }

  return options;

  usage:
  (void) fprintf(vis_stderr, "usage: ltl_to_aut <-f ltl_file> [-m algorithm] [-o output_file] [-t output_format] [-w] [-b] [-p] [-d] [-r] [-i] [-M] [-v verbosity_level] [-h]\n");
  (void) fprintf(vis_stderr, "    -f <ltl_file>\n");
  (void) fprintf(vis_stderr, "       The input file containing LTL formulae\n");
  (void) fprintf(vis_stderr, "    -m <algorithm>\n");
  (void) fprintf(vis_stderr, "        algorithm = 0 => GPVW\n");
  (void) fprintf(vis_stderr, "        algorithm = 1 => GPVW+\n");
  (void) fprintf(vis_stderr, "        algorithm = 2 => LTL2AUT\n");
  (void) fprintf(vis_stderr, "        algorithm = 3 => Wring (default)\n");
  (void) fprintf(vis_stderr, "    -o <output_file>\n");
  (void) fprintf(vis_stderr, "       Write the automata to output_file\n");
  (void) fprintf(vis_stderr, "    -t <output_format>\n");
  (void) fprintf(vis_stderr, "        output_format = 0 => dot\n");
  (void) fprintf(vis_stderr, "        output_format = 1 => blif_mv\n");
  (void) fprintf(vis_stderr, "        output_format = 2 => verilog\n");
  (void) fprintf(vis_stderr, "        output_format = 3 => all (default)\n");
  (void) fprintf(vis_stderr, "    -w \tRewriting the formula\n");
  (void) fprintf(vis_stderr, "    -b \tBoolean minimization \n");
  (void) fprintf(vis_stderr, "    -p \tPruning the fairness\n");
  (void) fprintf(vis_stderr, "    -d \tDirect-simulation minimization\n");
  (void) fprintf(vis_stderr, "    -r \tReverse-simulation minimization\n");
  (void) fprintf(vis_stderr, "    -i \tI/O compatible minimization\n");
  (void) fprintf(vis_stderr, "    -M \tAdd arcs by direct-simulation to reduce the counter-example length\n");
  (void) fprintf(vis_stderr, "    -v <verbosity>\n");
  (void) fprintf(vis_stderr, "       \tVerbosity can be 0,1,2,3\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");

  LtlMcOptionFree(options);
  return NIL(LtlMcOption_t);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void ShuffleMddIdsToTop	(	mdd_manager *	mddManager,
		array_t *	mddIdArray
	)		[static]

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

Synopsis [Move the mdd variables to the top most.]

Description [This function is called to move the automaton variables to the top most. This is believed to be the best variable ordering for the composed system (M x A). The variable corresponding to the first item in mddIdArray will be the top most.]

SideEffects []

Definition at line 2002 of file ltl.c.

{
  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
  int *invPermArray = ALLOC(int, bdd_num_vars(mddManager));
  int invPermIndex, i, j, bvarId, mddId, result;
  st_table *stored = st_init_table(st_ptrcmp, st_ptrhash);
  mvar_type mvar;

  /* put mddId on the top most */
  invPermIndex = 0;
  arrayForEachItem(int, mddIdArray, j, mddId) {
    if (mddId == 0) continue;
    mvar = array_fetch(mvar_type, mvar_list, mddId);
    for (i = 0; i<mvar.encode_length; i++) {
      bvarId = mdd_ret_bvar_id(&mvar, i);
      invPermArray[invPermIndex++] = bvarId;
      st_insert(stored, (char *) (long) bvarId, (char *)0);
    }
  }
  /* shift every one else down */
  for (i = 0; (unsigned) i< bdd_num_vars(mddManager); i++) {
    bvarId = bdd_get_id_from_level(mddManager, i);
    if (!st_is_member(stored, (char *) (long) bvarId)) {
      invPermArray[invPermIndex++] = bvarId;
    }
  }
  /* call bdd_shuffle */
  result = bdd_shuffle_heap(mddManager, invPermArray);
#ifdef DEBUG_LTLMC
  if (result)
    fprintf(vis_stdout, "\nShuffle automaton vars to the top: success!\n");
  else
    fprintf(vis_stdout, "\nShuffle automaton vars to the top: failure!\n");
#endif

  /* Clean up */
  st_free_table(stored);
  FREE(invPermArray);
}

Here is the caller graph for this function:

static void TimeOutHandle

(

void

)

[static]

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

Synopsis [Handle function for timeout.]

Description [This function is called when the process receives a signal of type alarm. Since alarm is set with elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire later and check if the CPU limit has been reached.]

SideEffects []

Definition at line 1984 of file ltl.c.

{
  longjmp(timeOutEnv, 1);
}

Here is the caller graph for this function:

---

Variable Documentation

jmp_buf timeOutEnv [static]

Definition at line 37 of file ltl.c.

char rcsid [] UNUSED = "$Id: ltl.c,v 1.74 2009/04/11 01:41:30 fabio Exp $" [static]

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

FileName [ltl.c]

PackageName [ltl]

Synopsis [LTL model checking.]

Author [Chao Wang <chao.wang@colorado.EDU>]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 20 of file ltl.c.