NuSMV/code/nusmv/core/bmc/bmcCheck.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"

Go to the source code of this file.

Typedefs
typedef int(*	BMC_PF_MATCH )(const NuSMVEnv_ptr, node_ptr, int, void *)
	Interface for module Check.
typedef void(*	BMC_PF_MATCH_ANSWER )(const NuSMVEnv_ptr, node_ptr, int, void *)
Functions
node_ptr	Bmc_CheckFairnessListForPropositionalFormulae (const NuSMVEnv_ptr env, node_ptr wffList)
	Helper function to simplify calling to 'bmc_check_wff_list' for searching of propositional wff only. Returns a new list of wffs which contains legal wffs only.
int	Bmc_WffListMatchProperty (const NuSMVEnv_ptr env, node_ptr wffList, BMC_PF_MATCH pCheck, void *pCheckOptArgument, int iMaxMatches, unsigned int *aiMatchedIndexes, BMC_PF_MATCH_ANSWER pAnswer, void *pAnswerOptArgument)
	For each element belonging to a given list of wffs, calls the given matching function. If function matches, calls given answering function.

---

Typedef Documentation

typedef int(* BMC_PF_MATCH)(const NuSMVEnv_ptr, node_ptr, int, void *)

Interface for module Check.

Author:

Roberto Cavada Contains function definition for propositional wff checking

Todo:

Missing synopsis

Todo:

Missing description

typedef void(* BMC_PF_MATCH_ANSWER)(const NuSMVEnv_ptr, node_ptr, int, void *)

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

node_ptr Bmc_CheckFairnessListForPropositionalFormulae	(	const NuSMVEnv_ptr	env,
		node_ptr	wffList
	)

Helper function to simplify calling to 'bmc_check_wff_list' for searching of propositional wff only. Returns a new list of wffs which contains legal wffs only.

AutomaticStart

See also:

bmc_check_wff_list

int Bmc_WffListMatchProperty	(	const NuSMVEnv_ptr	env,
		node_ptr	wffList,
		BMC_PF_MATCH	pCheck,
		void *	pCheckOptArgument,
		int	iMaxMatches,
		unsigned int *	aiMatchedIndexes,
		BMC_PF_MATCH_ANSWER	pAnswer,
		void *	pAnswerOptArgument
	)

For each element belonging to a given list of wffs, calls the given matching function. If function matches, calls given answering function.

This is a generic searching function for a property across a list of wffs. Please note that searching is specific for a list of wffs, but the searching semantic and behaviour are generic and customizable.
Searching may be stopped after the Nth match, or can be continued till all list elements have been checked (specify -1 in this case). In any case searching cannot be carried out over the MAX_MATCHES value.

Arguments:

Parameter name	Description
wffList	A list of wffs to iterate in
pCheck	Pointer to matching function. The checking function type is BMC_PF_MATCH, and has three parameters: wff the formula to check for index index of wff into list pOpt generic pointer to custom structure (optional)
pCheckOptArgument	Argument passed to pCheck (specify NULL if you do not use it.)
iMaxMatches	Maximum number of matching to be found before return. This must be less of MAX_MATCHES. Specify -1 to iterate across the entire list.
aiMatchedIndexes	Optional int array which will contain all match indexes. Specify NULL if you do not need this functionality. Array size must be less of MAX_MATCHES.
pAnswer	Pointer to answer function of type BMC_PF_MATCH_ANSWER. This function is called everytime a match is found. Specify NULL if you do not need for this functionality. The answer function has the following prototype: void answer(node_ptr wff, int index, void* pOpt) where: wff the formula that matches the criteria index is the index of wff into the list pOpt pointer to generic & customizable structure (see pAnswerOptArgument below) pAnswerOptArgument optional parameter for pAnswer function, in order to ensure more flexibility. Specify NULL if you do not need for this functionality.)

Given aiMatchedIndexes array changes if at least one match has found out