NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauLTLformula.h File Reference

#include "nusmv/core/fsm/be/BeFsm.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/node/node.h"

Go to the source code of this file.

Functions
be_ptr	BmcInt_SBMCTableau_GetAtTime (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int time, const int k, const int l)
	Public interface for SBMC tableau-related functionalities.

---

Function Documentation

be_ptr BmcInt_SBMCTableau_GetAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	time,
		const int	k,
		const int	l
	)

Public interface for SBMC tableau-related functionalities.

Author:

Timo Latvala, Marco Roveri

Todo:

: Missing description

AutomaticStart

Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by \[k, l\] The function generates the necessary auxilliary predicates (loop, atmostonce) and calls on get_f_at_time to generate the tableau for the ltl formula.

See also:

AtMostOnce, Loop, get_f_at_time