NuSMV/code/nusmv/core/ltl/ltlInt.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/compile/symb_table/SymbLayer.h"
#include "nusmv/core/compile/symb_table/SymbType.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/fsm/bdd/BddFsm.h"
#include "nusmv/core/trace/TraceMgr.h"

Go to the source code of this file.

Enumerations
enum	LtlRewriteType { LTL_REWRITE_STANDARD, LTL_REWRITE_DEADLOCK_FREE }
	Internal header of the `ltl` package. More...
Functions
bdd_ptr	feasible (BddFsm_ptr fsm, BddEnc_ptr enc)
	Check for feasability.
node_ptr	Ltl_RewriteInput (SymbTable_ptr symb_table, node_ptr expr, SymbLayer_ptr layer, node_ptr init, node_ptr invar, node_ptr *trans, LtlRewriteType rewrite_type)
node_ptr	witness (BddFsm_ptr fsm, BddEnc_ptr enc, bdd_ptr feasible)
	Compute a withness of feasability.
Variables
cmp_struct_ptr	cmps
bdd_ptr	fair_states_bdd
node_ptr	fairness_constraints_bdd
FsmBuilder_ptr	global_fsm_builder
TraceMgr_ptr	global_trace_manager
bdd_ptr	init_bdd
bdd_ptr	invar_bdd
bdd_ptr	trans_bdd

Enumeration Type Documentation

enum LtlRewriteType

Internal header of the ltl package.

Author:: Marco Roveri

Todo:: : Missing description

Todo:: Missing synopsis

Todo:: Missing description

Enumerator:

LTL_REWRITE_STANDARD
LTL_REWRITE_DEADLOCK_FREE

Function Documentation

bdd_ptr feasible	(	BddFsm_ptr	fsm,
		BddEnc_ptr	enc
	)

Check for feasability.

Checks whether the model has a fair path and returns the initial state of the path.

node_ptr Ltl_RewriteInput	(	SymbTable_ptr	symb_table,
		node_ptr	expr,
		SymbLayer_ptr	layer,
		node_ptr *	init,
		node_ptr *	invar,
		node_ptr *	trans,
		LtlRewriteType	rewrite_type
	)