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

#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Enumerations
enum	GenWffOperator {   GWO_None, GWO_Globally, GWO_Future, GWO_Until,   GWO_Releases, GWO_Historically, GWO_Once, GWO_Since,   GWO_Triggered }
	Module header for bmcTest. More...
Functions
int	Bmc_Test_test_tableau (NuSMVEnv_ptr env, node_ptr wff, GenWffOperator wff_operator, int max_depth, int max_conns, boolean usePastOperators, boolean crossComparison, int k, int l)
	The first time Bmc_Test_test_tableau is called in the current session this function creates a smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file.

---

Enumeration Type Documentation

enum GenWffOperator

Module header for bmcTest.

Author:

Michele Dorigatti

Todo:

: Missing description

Enumerator:

GWO_None
GWO_Globally
GWO_Future
GWO_Until
GWO_Releases
GWO_Historically
GWO_Once
GWO_Since
GWO_Triggered

---

Function Documentation

int Bmc_Test_test_tableau	(	NuSMVEnv_ptr	env,
		node_ptr	wff,
		GenWffOperator	wff_operator,
		int	max_depth,
		int	max_conns,
		boolean	usePastOperators,
		boolean	crossComparison,
		int	k,
		int	l
	)

The first time Bmc_Test_test_tableau is called in the current session this function creates a smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file.

AutomaticStart

BMC_ALL_LOOPS is not supported