explicit_cuba: An explicit version for context-unbounded analysis. More...

#include <cuba.hh>

Inheritance diagram for cuba::explicit_cuba:

Public Member Functions
	explicit_cuba (const string &initl, const string &final, const string &filename)

virtual	~explicit_cuba ()

virtual void	context_unbounded_analysis (const size_k k_bound=0)

Public Member Functions inherited from cuba::base_cuba
	base_cuba (const string &initl, const string &final, const string &filename)

Additional Inherited Members
Protected Attributes inherited from cuba::base_cuba
bool	reachable

explicit_state	initl_c
	explicit initial state

visible_state	final_c
	explicit target state

concurrent_pushdown_automata	CPDA
	concurrent pushdown system

vector< set< visible_state > >	generators
	generators: used for determining the convergence

vector< vector< bool > >	reachable_T

Detailed Description

explicit_cuba: An explicit version for context-unbounded analysis.

Constructor & Destructor Documentation

◆ explicit_cuba()

cuba::explicit_cuba::explicit_cuba	(	const string &	initl,
		const string &	final,
		const string &	filename
	)

Constructor for explicit version of CUBA; calling base_cuba Set up the initial global state, target state, concurrent pushdown system and the overapproximation of reachable top states.

Parameters

initl	initial global state
final	final global state
filename	input CPDs

◆ ~explicit_cuba()

cuba::explicit_cuba::~explicit_cuba ( )

virtual

destructor

Member Function Documentation

◆ context_unbounded_analysis()

void cuba::explicit_cuba::context_unbounded_analysis ( const size_k k_bound = 0 )

virtual

The procedure of context-bounded analysis

Parameters

k	the number of context switches

Implements cuba::base_cuba.

The documentation for this class was generated from the following files:

cuba.hh
ecuba.cc