nanotrav/ntr.c File Reference

A very simple reachability analysis program. More...

#include "cuddInt.h"
#include "ntr.h"
Include dependency graph for ntr.c:

Defines

#define NTR_MAX_DEP_SIZE   20

Functions

int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2)
 Builds DDs for a network outputs and next state functions.
NtrPartTRNtr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image)
 Builds the transition relation for a network.
void Ntr_freeTR (DdManager *dd, NtrPartTR *TR)
 Frees the transition relation for a network.
NtrPartTRNtr_cloneTR (NtrPartTR *TR)
 Makes a copy of a transition relation.
int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Poor man's traversal procedure.
int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Computes the SCCs of the STG.
int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Transitive closure traversal procedure.
DdNodeNtr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option)
 Builds the transitive closure of a transition relation.
DdNodeNtr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Builds the BDD of the initial state(s).
DdNodeNtr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr)
 Reads a state cube from a file or creates a random one.
int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option)
 Poor man's outer envelope computation.
int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Maximum 0-1 flow between source and sink states.
static DdNodemakecube (DdManager *dd, DdNode **x, int n)
 Builds a positive cube of all the variables in x.
static void ntrInitializeCount (BnetNetwork *net, NtrOptions *option)
 Initializes the count fields used to drop DDs.
static void ntrCountDFS (BnetNetwork *net, BnetNode *node)
 Does a DFS from a node setting the count field.
static DdNodentrImage (DdManager *dd, NtrPartTR *TR, DdNode *from, NtrOptions *option)
 Computes the image of a set given a transition relation.
static DdNodentrPreimage (DdManager *dd, NtrPartTR *T, DdNode *from)
 Computes the preimage of a set given a transition relation.
static DdNodentrChooseFrom (DdManager *dd, DdNode *neW, DdNode *reached, NtrOptions *option)
 Chooses the initial states for a BFS step.
static DdNodentrUpdateReached (DdManager *dd, DdNode *oldreached, DdNode *to)
 Updates the reached states after a traversal step.
static int ntrLatchDependencies (DdManager *dd, DdNode *reached, BnetNetwork *net, NtrOptions *option)
 Analyzes the reached states after traversal to find dependent latches.
static NtrPartTRntrEliminateDependencies (DdManager *dd, NtrPartTR *TR, DdNode **states, NtrOptions *option)
 Eliminates dependent variables from a transition relation.
static int ntrUpdateQuantificationSchedule (DdManager *dd, NtrPartTR *T)
 Updates the quantification schedule of a transition relation.
static int ntrSignatureCompare (int *ptrX, int *ptrY)
 Comparison function used by qsort.
static int ntrSignatureCompare2 (int *ptrX, int *ptrY)
 Comparison function used by qsort.
static int ntrPartCompare (int *ptrX, int *ptrY)
 Comparison function used by qsort.
static char ** ntrAllocMatrix (int nrows, int ncols)
 Allocates a matrix of char's.
static void ntrFreeMatrix (char **matrix)
 Frees a matrix of char's.
static void ntrPermuteParts (DdNode **a, DdNode **b, int *comesFrom, int *goesTo, int size)
 Sorts parts according to given permutation.
static void ntrIncreaseRef (void *e, void *arg)
 Calls Cudd_Ref on its first argument.
static void ntrDecreaseRef (void *e, void *arg)
 Calls Cudd_RecursiveDeref on its first argument.

Variables

static char const * onames [] = {"T", "R"}
static double * signatures
static BnetNetworkstaticNet
static DdNode ** staticPart

Detailed Description

A very simple reachability analysis program.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


Function Documentation

static DdNode* makecube ( DdManager dd,
DdNode **  x,
int  n 
) [static]

Builds a positive cube of all the variables in x.

Returns:
a BDD for the cube if successful; NULL otherwise.
Side effects
None
int Ntr_buildDDs ( BnetNetwork net,
DdManager dd,
NtrOptions option,
BnetNetwork net2 
)

Builds DDs for a network outputs and next state functions.

The method is really brain-dead, but it is very simple. Some inputs to the network may be shared with another network whose DDs have already been built. In this case we want to share the DDs as well.

Returns:
1 in case of success; 0 otherwise.
Side effects
the dd fields of the network nodes are modified. Uses the count fields of the nodes.
Parameters:
net network for which DDs are to be built
dd DD manager
option option structure
net2 companion network with which inputs may be shared
NtrPartTR* Ntr_buildTR ( DdManager dd,
BnetNetwork net,
NtrOptions option,
int  image 
)

Builds the transition relation for a network.

Returns:
a pointer to the transition relation structure if successful; NULL otherwise.
Side effects
None
Parameters:
dd manager
net network
option options
image image type: monolithic ...
NtrPartTR* Ntr_cloneTR ( NtrPartTR TR  ) 

Makes a copy of a transition relation.

Returns:
a pointer to the copy if successful; NULL otherwise.
Side effects
None
See also:
Ntr_buildTR Ntr_freeTR
int Ntr_ClosureTrav ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Transitive closure traversal procedure.

Traversal procedure based on the transitive closure of the transition relation.

Returns:
1 in case of success; 0 otherwise.
Side effects
None
See also:
Ntr_Trav
Parameters:
dd DD manager
net network
option options
int Ntr_Envelope ( DdManager dd,
NtrPartTR TR,
FILE *  dfp,
NtrOptions option 
)

Poor man's outer envelope computation.

Based on the monolithic transition relation.

Returns:
1 in case of success; 0 otherwise.
Side effects
None
Parameters:
dd DD manager
TR transition relation
dfp pointer to file for DD dump
option program options
void Ntr_freeTR ( DdManager dd,
NtrPartTR TR 
)

Frees the transition relation for a network.

Side effects
None
DdNode* Ntr_getStateCube ( DdManager dd,
BnetNetwork net,
char *  filename,
int  pr 
)

Reads a state cube from a file or creates a random one.

Returns:
a pointer to the BDD of the sink nodes if successful; NULL otherwise.
Side effects
None
DdNode* Ntr_initState ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Builds the BDD of the initial state(s).

Returns:
a BDD if successful; NULL otherwise.
Side effects
None
int Ntr_maxflow ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Maximum 0-1 flow between source and sink states.

Returns:
1 in case of success; 0 otherwise.
Side effects
Creates two new sets of variables.
int Ntr_SCC ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Computes the SCCs of the STG.

Computes the strongly connected components of the state transition graph. Only the first 10 SCCs are computed.

Returns:
1 in case of success; 0 otherwise.
Side effects
None
See also:
Ntr_Trav
Parameters:
dd DD manager
net network
option options
DdNode* Ntr_TransitiveClosure ( DdManager dd,
NtrPartTR TR,
NtrOptions option 
)

Builds the transitive closure of a transition relation.

Uses a simple squaring algorithm.

Returns:
a BDD if successful; NULL otherwise.
Side effects
None
int Ntr_Trav ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Poor man's traversal procedure.

Based on the monolithic transition relation.

Returns:
1 in case of success; 0 otherwise.
Side effects
None
See also:
Ntr_ClosureTrav
Parameters:
dd DD manager
net network
option options
static char** ntrAllocMatrix ( int  nrows,
int  ncols 
) [static]

Allocates a matrix of char's.

Returns:
a pointer to the matrix if successful; NULL otherwise.
Side effects
None
static DdNode* ntrChooseFrom ( DdManager dd,
DdNode neW,
DdNode reached,
NtrOptions option 
) [static]

Chooses the initial states for a BFS step.

The reference count of the result is already incremented.

Returns:
a pointer to the chose set if successful; NULL otherwise.
Side effects
none
See also:
Ntr_Trav
static void ntrCountDFS ( BnetNetwork net,
BnetNode node 
) [static]

Does a DFS from a node setting the count field.

Side effects
Changes the count and visited fields of the nodes it visits.
See also:
ntrLevelDFS
static NtrPartTR* ntrEliminateDependencies ( DdManager dd,
NtrPartTR TR,
DdNode **  states,
NtrOptions option 
) [static]

Eliminates dependent variables from a transition relation.

Returns:
a simplified copy of the given transition relation if successful; NULL otherwise.
Side effects
The modified set of states is returned as a side effect.
See also:
ntrImage
static void ntrFreeMatrix ( char **  matrix  )  [static]

Frees a matrix of char's.

Side effects
None
static DdNode* ntrImage ( DdManager dd,
NtrPartTR TR,
DdNode from,
NtrOptions option 
) [static]

Computes the image of a set given a transition relation.

The image is returned in terms of the present state variables; its reference count is already increased.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Ntr_Trav
static void ntrInitializeCount ( BnetNetwork net,
NtrOptions option 
) [static]

Initializes the count fields used to drop DDs.

Before actually building the BDDs, we perform a DFS from the outputs to initialize the count fields of the nodes. The initial value of the count field will normally coincide with the fanout of the node. However, if there are nodes with no path to any primary output or next state variable, then the initial value of count for some nodes will be less than the fanout. For primary outputs and next state functions we add 1, so that we will never try to free their DDs. The count fields of the nodes that are not reachable from the outputs are set to -1.

Side effects
Changes the count fields of the network nodes. Uses the visited fields.
static int ntrLatchDependencies ( DdManager dd,
DdNode reached,
BnetNetwork net,
NtrOptions option 
) [static]

Analyzes the reached states after traversal to find dependent latches.

The algorithm is greedy and determines a local optimum, not a global one.

Returns:
the number of latches that can be eliminated because they are stuck at a constant value or are dependent on others if successful; -1 otherwise.
See also:
Ntr_Trav
static int ntrPartCompare ( int *  ptrX,
int *  ptrY 
) [static]

Comparison function used by qsort.

Used to order the parts according to their BDD addresses.

Side effects
None
static void ntrPermuteParts ( DdNode **  a,
DdNode **  b,
int *  comesFrom,
int *  goesTo,
int  size 
) [static]

Sorts parts according to given permutation.

Side effects
The permutation arrays are turned into the identity permutations.
static DdNode* ntrPreimage ( DdManager dd,
NtrPartTR T,
DdNode from 
) [static]

Computes the preimage of a set given a transition relation.

The preimage is returned in terms of the next state variables; its reference count is already increased.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
ntrImage Ntr_SCC
static int ntrSignatureCompare ( int *  ptrX,
int *  ptrY 
) [static]

Comparison function used by qsort.

Used to order the variables according to their signatures.

Side effects
None
static int ntrSignatureCompare2 ( int *  ptrX,
int *  ptrY 
) [static]

Comparison function used by qsort.

Used to order the variables according to their signatures.

Side effects
None
static int ntrUpdateQuantificationSchedule ( DdManager dd,
NtrPartTR T 
) [static]

Updates the quantification schedule of a transition relation.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
ntrEliminateDependencies
static DdNode* ntrUpdateReached ( DdManager dd,
DdNode oldreached,
DdNode to 
) [static]

Updates the reached states after a traversal step.

The reference count of the result is already incremented.

Returns:
a pointer to the new reached set if successful; NULL otherwise.
Side effects
The old reached set is dereferenced.
See also:
Ntr_Trav
Parameters:
dd manager
oldreached old reached state set
to result of last image computation

Variable Documentation

char const* onames[] = {"T", "R"} [static]

names of functions to be dumped

double* signatures [static]

signatures for all variables

pointer to network used by qsort comparison function

DdNode** staticPart [static]

pointer to parts used by qsort comparison function

 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1