cuba::base_cuba Class Reference

#include <cuba.hh>

Inheritance diagram for cuba::base_cuba:

Public Member Functions
	base_cuba (const string &initl, const string &final, const string &filename)
virtual void	context_unbounded_analysis (const size_k k_bound=0)=0

Protected Attributes
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

base_cuba: the base class for context-unbounded analysis. Classes symbolic_cuba and explicit_cuba are inherited from it.

Constructor & Destructor Documentation

base_cuba()

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

Constructor Set up the initial global state, target state, concurrent pushdown system and the overapproximation of reachable top configurations.

Parameters

initl	initial global state
final	target visible state
filename	input CPDs

Member Data Documentation

reachable_T

vector<vector<bool> > cuba::base_cuba::reachable_T

protected

used for marking the set of reachable thread states, only supporting parameterized system for now

---

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

• cuba.hh
• cuba.cc