NuSMV/code/nusmv/core/wff/wff.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/wff/wffRewrite.h"
#include "nusmv/core/wff/ExprMgr.h"

Go to the source code of this file.

Functions
int	Wff_get_depth (const NuSMVEnv_ptr env, node_ptr ltl_wff)
	Returns the modal depth of the given formula.
boolean	Wff_is_propositional (SymbTable_ptr symb_table, node_ptr wff, node_ptr context, boolean is_next_allowed)
	True if wff is a propositional formula.
node_ptr	Wff_make_and (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an and WFF.
node_ptr	Wff_make_eventually (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes an eventually WFF.
node_ptr	Wff_make_falsity (NodeMgr_ptr nodemgr)
	Makes a false WFF.
node_ptr	Wff_make_globally (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes a globally WFF.
node_ptr	Wff_make_historically (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes a historically WFF.
node_ptr	Wff_make_iff (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an iff WFF.
node_ptr	Wff_make_implies (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an implies WFF.
node_ptr	Wff_make_next (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes a next WFF.
node_ptr	Wff_make_not (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes a not WFF.
node_ptr	Wff_make_once (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes an once WFF.
node_ptr	Wff_make_opnext (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes an op_next WFF.
node_ptr	Wff_make_opnext_times (NodeMgr_ptr nodemgr, node_ptr arg, int x)
	Applies op_next x times.
node_ptr	Wff_make_opnotprecnot (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes an op_next WFF.
node_ptr	Wff_make_opprec (NodeMgr_ptr nodemgr, node_ptr arg)
	Makes an op_next WFF.
node_ptr	Wff_make_or (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an or WFF.
node_ptr	Wff_make_releases (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes a releases WFF.
node_ptr	Wff_make_since (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an since WFF.
node_ptr	Wff_make_triggered (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes a triggered WFF.
node_ptr	Wff_make_truth (NodeMgr_ptr nodemgr)
	Makes a truth WFF.
node_ptr	Wff_make_until (NodeMgr_ptr nodemgr, node_ptr arg1, node_ptr arg2)
	Makes an until WFF.
void	wff_pkg_init (const NuSMVEnv_ptr env)
	Public interface for Well-Formed-Formula manipulation.
void	wff_pkg_quit (const NuSMVEnv_ptr env)
	Deinitializes the wff package.

---

Function Documentation

int Wff_get_depth	(	const NuSMVEnv_ptr	env,
		node_ptr	ltl_wff
	)

Returns the modal depth of the given formula.

Returns 0 for propositional formulae, 1 or more for temporal formulae

none

boolean Wff_is_propositional	(	SymbTable_ptr	symb_table,
		node_ptr	wff,
		node_ptr	context,
		boolean	is_next_allowed
	)

True if wff is a propositional formula.

Here, propositional means: without temporal operators boolean

The allowance of next is controlled by a flag.

node_ptr Wff_make_and	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an and WFF.

node hash may change

node_ptr Wff_make_eventually	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes an eventually WFF.

node hash may change

node_ptr Wff_make_falsity

(

NodeMgr_ptr

nodemgr

)

Makes a false WFF.

node hash may change

node_ptr Wff_make_globally	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes a globally WFF.

node hash may change

node_ptr Wff_make_historically	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes a historically WFF.

node hash may change

node_ptr Wff_make_iff	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an iff WFF.

node hash may change

node_ptr Wff_make_implies	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an implies WFF.

node hash may change

node_ptr Wff_make_next	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes a next WFF.

node hash may change

node_ptr Wff_make_not	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes a not WFF.

node hash may change

node_ptr Wff_make_once	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes an once WFF.

node hash may change

node_ptr Wff_make_opnext	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes an op_next WFF.

node hash may change

node_ptr Wff_make_opnext_times	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg,
		int	x
	)

Applies op_next x times.

node hash may change

node_ptr Wff_make_opnotprecnot	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes an op_next WFF.

node hash may change

node_ptr Wff_make_opprec	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg
	)

Makes an op_next WFF.

node hash may change

node_ptr Wff_make_or	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an or WFF.

node hash may change

node_ptr Wff_make_releases	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes a releases WFF.

node hash may change

node_ptr Wff_make_since	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an since WFF.

node hash may change

node_ptr Wff_make_triggered	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes a triggered WFF.

node hash may change

node_ptr Wff_make_truth

(

NodeMgr_ptr

nodemgr

)

Makes a truth WFF.

node hash may change

node_ptr Wff_make_until	(	NodeMgr_ptr	nodemgr,
		node_ptr	arg1,
		node_ptr	arg2
	)

Makes an until WFF.

node hash may change

void wff_pkg_init

(

const NuSMVEnv_ptr

env

)

Public interface for Well-Formed-Formula manipulation.

Author:

Alessandro Mariotti

Todo:

: Missing description

Initializes the wff package

See also:

wff_pkg_quit

void wff_pkg_quit

(

const NuSMVEnv_ptr

env

)

Deinitializes the wff package.

See also:

wff_pkg_init