symbolic_cuba: A symbolic version for context-unbounded analysis. More...

#include <cuba.hh>

Inheritance diagram for cuba::symbolic_cuba:

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

	~symbolic_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

symbolic_cuba: A symbolic version for context-unbounded analysis.

Constructor & Destructor Documentation

◆ symbolic_cuba()

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

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

Parameters

initl	initial global state
final	final global state
filename	the input CPDS

◆ ~symbolic_cuba()

cuba::symbolic_cuba::~symbolic_cuba ( )

destructor

Member Function Documentation

◆ context_unbounded_analysis()

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

virtual

The procedure of context-bounded analysis

Parameters

k_bound the upper bounds of contexts

step 1: set up the initial configurations

step 2: perform context-unbounded analysis

Implements cuba::base_cuba.

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

cuba.hh
scuba.cc