A very simple reachability analysis program. More...

#include "cuddInt.h"
#include "ntr.h"

Include dependency graph for ntr.c:

Macros
#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. More...

NtrPartTR *	Ntr_buildTR (DdManager dd, BnetNetwork net, NtrOptions *option, int image)
	Builds the transition relation for a network. More...

void	Ntr_freeTR (DdManager dd, NtrPartTR TR)
	Frees the transition relation for a network. More...

NtrPartTR *	Ntr_cloneTR (NtrPartTR *TR)
	Makes a copy of a transition relation. More...

int	Ntr_Trav (DdManager dd, BnetNetwork net, NtrOptions *option)
	Poor man's traversal procedure. More...

int	Ntr_SCC (DdManager dd, BnetNetwork net, NtrOptions *option)
	Computes the SCCs of the STG. More...

int	Ntr_ClosureTrav (DdManager dd, BnetNetwork net, NtrOptions *option)
	Transitive closure traversal procedure. More...

DdNode *	Ntr_TransitiveClosure (DdManager dd, NtrPartTR TR, NtrOptions *option)
	Builds the transitive closure of a transition relation. More...

DdNode *	Ntr_initState (DdManager dd, BnetNetwork net, NtrOptions *option)
	Builds the BDD of the initial state(s). More...

DdNode *	Ntr_getStateCube (DdManager dd, BnetNetwork net, char *filename, int pr)
	Reads a state cube from a file or creates a random one. More...

int	Ntr_Envelope (DdManager dd, NtrPartTR TR, FILE dfp, NtrOptions option)
	Poor man's outer envelope computation. More...

int	Ntr_maxflow (DdManager dd, BnetNetwork net, NtrOptions *option)
	Maximum 0-1 flow between source and sink states. More...

static DdNode *	makecube (DdManager dd, DdNode *x, int n)
	Builds a positive cube of all the variables in x. More...

static void	ntrInitializeCount (BnetNetwork net, NtrOptions option)
	Initializes the count fields used to drop DDs. More...

static void	ntrCountDFS (BnetNetwork net, BnetNode node)
	Does a DFS from a node setting the count field. More...

static DdNode *	ntrImage (DdManager dd, NtrPartTR TR, DdNode from, NtrOptions option)
	Computes the image of a set given a transition relation. More...

static DdNode *	ntrPreimage (DdManager dd, NtrPartTR T, DdNode *from)
	Computes the preimage of a set given a transition relation. More...

static DdNode *	ntrChooseFrom (DdManager dd, DdNode neW, DdNode reached, NtrOptions option)
	Chooses the initial states for a BFS step. More...

static DdNode *	ntrUpdateReached (DdManager dd, DdNode oldreached, DdNode *to)
	Updates the reached states after a traversal step. More...

static int	ntrLatchDependencies (DdManager dd, DdNode reached, BnetNetwork net, NtrOptions option)
	Analyzes the reached states after traversal to find dependent latches. More...

static NtrPartTR *	ntrEliminateDependencies (DdManager dd, NtrPartTR TR, DdNode *states, NtrOptions option)
	Eliminates dependent variables from a transition relation. More...

static int	ntrUpdateQuantificationSchedule (DdManager dd, NtrPartTR T)
	Updates the quantification schedule of a transition relation. More...

static int	ntrSignatureCompare (int ptrX, int ptrY)
	Comparison function used by qsort. More...

static int	ntrSignatureCompare2 (int ptrX, int ptrY)
	Comparison function used by qsort. More...

static int	ntrPartCompare (int ptrX, int ptrY)
	Comparison function used by qsort. More...

static char **	ntrAllocMatrix (int nrows, int ncols)
	Allocates a matrix of char's. More...

static void	ntrFreeMatrix (char **matrix)
	Frees a matrix of char's. More...

static void	ntrPermuteParts (DdNode a, DdNode b, int comesFrom, int goesTo, int size)
	Sorts parts according to given permutation. More...

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 BnetNetwork *	staticNet

static DdNode **	staticPart

Detailed Description

A very simple reachability analysis program.

Author: Fabio Somenzi

Copyright

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

◆ makecube()

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

◆ Ntr_buildDDs()

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

◆ Ntr_buildTR()

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

◆ Ntr_cloneTR()

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

◆ Ntr_ClosureTrav()

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

◆ Ntr_Envelope()

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

◆ Ntr_freeTR()

void Ntr_freeTR	(	DdManager *	dd,
		NtrPartTR *	TR
	)

Frees the transition relation for a network.

Side effects None

◆ Ntr_getStateCube()

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

◆ Ntr_initState()

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

◆ Ntr_maxflow()

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.

◆ Ntr_SCC()

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

◆ Ntr_TransitiveClosure()

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

◆ Ntr_Trav()

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

◆ ntrAllocMatrix()

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

◆ ntrChooseFrom()

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

◆ ntrCountDFS()

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

◆ ntrEliminateDependencies()

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

◆ ntrFreeMatrix()

static void ntrFreeMatrix ( char ** matrix )

static

Frees a matrix of char's.

Side effects None

◆ ntrImage()

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

◆ ntrInitializeCount()

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.

◆ ntrLatchDependencies()

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

◆ ntrPartCompare()

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

◆ ntrPermuteParts()

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.

◆ ntrPreimage()

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

◆ ntrSignatureCompare()

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

◆ ntrSignatureCompare2()

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

◆ ntrUpdateQuantificationSchedule()

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

◆ ntrUpdateReached()

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

◆ onames

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

static

names of functions to be dumped

◆ signatures

double* signatures

static

signatures for all variables

◆ staticNet

BnetNetwork* staticNet

static

pointer to network used by qsort comparison function

◆ staticPart

DdNode** staticPart

static

pointer to parts used by qsort comparison function

Macros

Functions

Variables

Detailed Description

Function Documentation

◆ makecube()

◆ Ntr_buildDDs()

◆ Ntr_buildTR()

◆ Ntr_cloneTR()

◆ Ntr_ClosureTrav()

◆ Ntr_Envelope()

◆ Ntr_freeTR()

◆ Ntr_getStateCube()

◆ Ntr_initState()

◆ Ntr_maxflow()

◆ Ntr_SCC()

◆ Ntr_TransitiveClosure()

◆ Ntr_Trav()

◆ ntrAllocMatrix()

◆ ntrChooseFrom()

◆ ntrCountDFS()

◆ ntrEliminateDependencies()

◆ ntrFreeMatrix()

◆ ntrImage()

◆ ntrInitializeCount()

◆ ntrLatchDependencies()

◆ ntrPartCompare()

◆ ntrPermuteParts()

◆ ntrPreimage()

◆ ntrSignatureCompare()

◆ ntrSignatureCompare2()

◆ ntrUpdateQuantificationSchedule()

◆ ntrUpdateReached()

Variable Documentation

◆ onames

◆ signatures

◆ staticNet

◆ staticPart