Classes
class	algs

class	alphabet

class	cuba_exception
	customized exception More...

class	cuba_runtime_error
	customized runtime error class More...

class	debugger

class	explicit_state

class	explicit_state_tid

class	finite_automaton

class	fsa_transition

class	generator

class	logger

class	parser

class	prop

class	pushdown_automaton

class	sstack

class	store_automaton

class	symbolic_state

class	thread_state

class	thread_visible_state

class	transition

class	visible_state

Typedefs
using	size_n = ushort
	the size of threads

using	size_k = ushort
	the size of context switches

using	id_thread_state = uint
	thread id

using	id_thread = size_n

using	ctx_bound = size_k

using	concurrent_pushdown_automata = vector< pushdown_automaton >

using	stack_vec = vector< pda_stack >
	the set of stacks in CPDS

using	finite_machine = map< thread_visible_state, deque< transition< thread_visible_state, thread_visible_state > >>

using	concurrent_finite_machine = vector< finite_machine >
	Concurrent finite machine: a vector of finite state machine.

using	fsa_state = pda_state

using	fsa_state_set = set< fsa_state >
	a set of fsa_state

using	fsa_alpha = pda_alpha

using	fsa_alphabet = set< fsa_alpha >
	a set of fsa_alpha

using	fsa_delta = unordered_map< fsa_state, set< fsa_transition > >
	the data structure of FSA transitions

using	pda_state = uint
	define the control state of PDSs

using	pda_alpha = uint
	define the stack symbol of PDSs

using	pda_stack = sstack< pda_alpha >

using	id_action = uint

using	adj_list = map< thread_visible_state, deque< id_action > >

using	pda_action = transition< thread_visible_state, thread_state >

Enumerations
enum	sequence { CONVERGENT, DIVERGENT, REACHABLE, UNKNOWN }

enum	type_stack_operation { PUSH, POP, OVERWRITE }

enum	type_synchronization { FORK, NORM, BRCT }

enum	alignment { LEFTJUST, RIGHTJUST, CENTERED }

Functions
ostream &	operator<< (ostream &os, const visible_state &s)

bool	operator< (const visible_state &s1, const visible_state &s2)

bool	operator> (const visible_state &s1, const visible_state &s2)

bool	operator== (const visible_state &s1, const visible_state &s2)

bool	operator!= (const visible_state &s1, const visible_state &s2)

ostream &	operator<< (ostream &os, const explicit_state &c)

bool	operator< (const explicit_state &g1, const explicit_state &g2)

bool	operator> (const explicit_state &g1, const explicit_state &g2)

bool	operator== (const explicit_state &g1, const explicit_state &g2)

bool	operator!= (const explicit_state &g1, const explicit_state &g2)

ostream &	operator<< (ostream &os, const explicit_state_tid &c)

bool	operator< (const explicit_state_tid &g1, const explicit_state_tid &g2)

bool	operator> (const explicit_state_tid &g1, const explicit_state_tid &g2)

bool	operator== (const explicit_state_tid &g1, const explicit_state_tid &g2)

bool	operator!= (const explicit_state_tid &g1, const explicit_state_tid &g2)

ostream &	operator<< (ostream &os, const symbolic_state &c)

ostream &	operator<< (ostream &os, const fsa_transition &r)

bool	operator< (const fsa_transition &r1, const fsa_transition &r2)

bool	operator> (const fsa_transition &r1, const fsa_transition &r2)

bool	operator== (const fsa_transition &r1, const fsa_transition &r2)

bool	operator!= (const fsa_transition &r1, const fsa_transition &r2)

ostream &	operator<< (ostream &os, const finite_automaton &fsa)

ostream &	operator<< (ostream &os, const type_stack_operation &t)

ostream &	operator<< (ostream &os, const type_synchronization &t)

template<typename T1 , typename T2 >
ostream &	operator<< (ostream &os, const transition< T1, T2 > &r)

ostream &	operator<< (ostream &os, const thread_visible_state &t)

bool	operator< (const thread_visible_state &t1, const thread_visible_state &t2)

bool	operator> (const thread_visible_state &t1, const thread_visible_state &t2)

bool	operator== (const thread_visible_state &t1, const thread_visible_state &t2)

bool	operator!= (const thread_visible_state &t1, const thread_visible_state &t2)

template<typename T >
ostream &	operator<< (ostream &os, const sstack< T > &a)

template<typename T >
bool	operator< (const sstack< T > &a1, const sstack< T > &a2)

template<typename T >
bool	operator> (const sstack< T > &a1, const sstack< T > &a2)

template<typename T >
bool	operator== (const sstack< T > &a1, const sstack< T > &a2)

template<typename T >
bool	operator!= (const sstack< T > &a1, const sstack< T > &a2)

ostream &	operator<< (ostream &os, const thread_state &c)

bool	operator< (const thread_state &c1, const thread_state &c2)

bool	operator> (const thread_state &c1, const thread_state &c2)

bool	operator== (const thread_state &c1, const thread_state &c2)

bool	operator!= (const thread_state &c1, const thread_state &c2)

ostream &	operator<< (ostream &os, const pushdown_automaton &PDA)

Detailed Description

state.cc

Date: : Aug 27, 2016

Author: : TODO

Finite-state automaton

Date: : Sep 15, 2016

Author: : TODO

generator.cc

Date: : Jan 19, 2018

Author: : TODO

generator.hh

Date: : Jan 19, 2018

Author: : TODO

PDS parser

Date: : Aug 30, 2016

Author: : TODO

PDS parser

Date: : Jan 1, 2018

Author: : TODO

Pushdown automaton

Date: : Sep 15, 2016

Author: : TODO

prop.cc

Date: : Aug 29, 2016

Author: : TODO

prop.hh This is a property class

Date: Aug 29, 2016

Author: TODO

utilities.cc

Date: Aug 29, 2016

Author: TODO

utilities.hh

Date: Aug 29, 2016

Author: TODO

Typedef Documentation

◆ concurrent_pushdown_automata

using ruba::concurrent_pushdown_automata = typedef vector<pushdown_automaton>

concurrent pushdown automaton

◆ finite_machine

using ruba::finite_machine = typedef map<thread_visible_state, deque<transition<thread_visible_state, thread_visible_state> >>

A finite machine: used for overapproximate reachable visible states. We definite a finite state machine in the form of adjacency list.

◆ id_action

using ruba::id_action = typedef uint

PART 3. The definition of a sequential pushdown automaton

define the transition ID

◆ pda_stack

using ruba::pda_stack = typedef sstack<pda_alpha>

Definition of the stack for a PDA

Enumeration Type Documentation

◆ sequence

enum ruba::sequence

strong

The result data structure of observation sequences

◆ type_stack_operation

enum ruba::type_stack_operation

strong

define the type of stack operations: PUSH : push an element to the stack POP : pop an element from the stack OVERWRITE: overwrite the top element of the stack

◆ type_synchronization

enum ruba::type_synchronization

strong

define type of thread state transitions FORK: spawn a new thread NORM: the normal thread state transitions BRCT: the broadcast transitions

Function Documentation

◆ operator!=() [1/7]

bool ruba::operator!=	(	const fsa_transition &	r1,
		const fsa_transition &	r2
	)

inline

overloading operator !=

Parameters

r1
r2

Returns: bool

◆ operator!=() [2/7]

bool ruba::operator!=	(	const visible_state &	s1,
		const visible_state &	s2
	)

inline

overloading operator !=, return true if s1 != s2 and false otherwise

Parameters

s1	a visible state
s2	a visible state

Returns: bool

◆ operator!=() [3/7]

bool ruba::operator!=	(	const explicit_state &	g1,
		const explicit_state &	g2
	)

inline

overloading the operator !=

Parameters

g1
g2

Returns: bool

◆ operator!=() [4/7]

bool ruba::operator!=	(	const thread_visible_state &	t1,
		const thread_visible_state &	t2
	)

inline

overloading operator !=

Parameters

t1
t2

Returns: bool

◆ operator!=() [5/7]

bool ruba::operator!=	(	const explicit_state_tid &	g1,
		const explicit_state_tid &	g2
	)

inline

overloading the operator !=, return true if g1 != g2 and false otherwise

Parameters

g1
g2

Returns: bool

◆ operator!=() [6/7]

template<typename T >

bool ruba::operator!=	(	const sstack< T > &	a1,
		const sstack< T > &	a2
	)

inline

overloading operator !=

Parameters

a1
a2

Returns: bool

◆ operator!=() [7/7]

bool ruba::operator!=	(	const thread_state &	c1,
		const thread_state &	c2
	)

inline

overloading operator !=

Parameters

c1
c2

Returns: bool

◆ operator<() [1/7]

bool ruba::operator<	(	const fsa_transition &	r1,
		const fsa_transition &	r2
	)

inline

overloading operator <

Parameters

r1
r2

Returns: bool

◆ operator<() [2/7]

bool ruba::operator<	(	const visible_state &	s1,
		const visible_state &	s2
	)

inline

overloading operator <, return true if s1 < s2 and false otherwise

Parameters

s1	a visible state
s2	a visible state

Returns: bool

◆ operator<() [3/7]

bool ruba::operator<	(	const explicit_state &	g1,
		const explicit_state &	g2
	)

inline

overloading the operator <

Parameters

g1
g2

Returns: bool

◆ operator<() [4/7]

bool ruba::operator<	(	const thread_visible_state &	t1,
		const thread_visible_state &	t2
	)

inline

overloading operator <

Parameters

t1
t2

Returns: bool

◆ operator<() [5/7]

bool ruba::operator<	(	const explicit_state_tid &	g1,
		const explicit_state_tid &	g2
	)

inline

overloading the operator <, return true if g1 < g2 and false otherwise

Parameters

g1
g2

Returns: bool

◆ operator<() [6/7]

template<typename T >

bool ruba::operator<	(	const sstack< T > &	a1,
		const sstack< T > &	a2
	)

inline

overloading operator <

Parameters

a1
a2

Returns: bool

◆ operator<() [7/7]

bool ruba::operator<	(	const thread_state &	c1,
		const thread_state &	c2
	)

inline

overloading operator <

Parameters

c1
c2

Returns: bool

◆ operator<<() [1/13]

ostream& ruba::operator<<	(	ostream &	os,
		const type_stack_operation &	t
	)

inline

overloading operator <<

Parameters

os
t

Returns: ostream

◆ operator<<() [2/13]

ostream& ruba::operator<<	(	ostream &	os,
		const fsa_transition &	r
	)

inline

overloading operator <<

Parameters

os
r

Returns: ostream

◆ operator<<() [3/13]

ostream& ruba::operator<<	(	ostream &	os,
		const visible_state &	s
	)

inline

overloading operator << to print a visible state

Parameters

os	an output stream
s	a visible state

Returns: a reference to output stream

◆ operator<<() [4/13]

ostream& ruba::operator<<	(	ostream &	os,
		const type_synchronization &	t
	)

inline

overloading operator <<

Parameters

os
t

Returns: ostream

◆ operator<<() [5/13]

template<typename T1 , typename T2 >

ostream& ruba::operator<<	(	ostream &	os,
		const transition< T1, T2 > &	r
	)

inline

overloading the operator <<

Parameters

os
r

Returns: ostream

◆ operator<<() [6/13]

ostream& ruba::operator<<	(	ostream &	os,
		const explicit_state &	c
	)

inline

overloading operator <<: print a configuration of the CPDS

Parameters

os	an output
c

Returns: ostream

◆ operator<<() [7/13]

ostream& ruba::operator<<	(	ostream &	os,
		const finite_automaton &	fsa
	)

inline

overloading operator <<

Parameters

os
fsa

Returns: ostream

◆ operator<<() [8/13]

ostream& ruba::operator<<	(	ostream &	os,
		const thread_visible_state &	t
	)

inline

overloading operator <<

Parameters

os
s

Returns: ostream

◆ operator<<() [9/13]

ostream& ruba::operator<<	(	ostream &	os,
		const explicit_state_tid &	c
	)

inline

overloading operator <<: print a configuration of the CPDS

Parameters

os	an output stream
c	an explicit_state_id

Returns: ostream

◆ operator<<() [10/13]

template<typename T >

ostream& ruba::operator<<	(	ostream &	os,
		const sstack< T > &	a
	)

inline

overloading operator <<: ostream

Parameters

os
a

Returns: ostream

◆ operator<<() [11/13]

ostream& ruba::operator<<	(	ostream &	os,
		const symbolic_state &	c
	)

inline

overloading operator << to print a symbolic state

Parameters

os	an output stream
c	a symbolic state

Returns: ostream

◆ operator<<() [12/13]

ostream& ruba::operator<<	(	ostream &	os,
		const thread_state &	c
	)

inline

overloading operator <<: print thread configuration

Parameters

out
c

Returns: ostream

◆ operator<<() [13/13]

ostream& ruba::operator<<	(	ostream &	os,
		const pushdown_automaton &	PDA
	)

inline

overloading operator <<: print a PDA

Parameters

os
PDA

Returns: ostream

◆ operator==() [1/7]

bool ruba::operator==	(	const fsa_transition &	r1,
		const fsa_transition &	r2
	)

inline

overloading operator ==

Parameters

r1
r2

Returns: bool

◆ operator==() [2/7]

bool ruba::operator==	(	const visible_state &	s1,
		const visible_state &	s2
	)

inline

overloading operator ==, return true if s1 == s2 and false otherwise

Parameters

s1	a visible state
s2	a visible state

Returns: bool

◆ operator==() [3/7]

bool ruba::operator==	(	const explicit_state &	g1,
		const explicit_state &	g2
	)

inline

overloading the operator ==

Parameters

g1
g2

Returns: bool

◆ operator==() [4/7]

bool ruba::operator==	(	const thread_visible_state &	t1,
		const thread_visible_state &	t2
	)

inline

overloading operator ==

Parameters

t1
t2

Returns: bool

◆ operator==() [5/7]

bool ruba::operator==	(	const explicit_state_tid &	g1,
		const explicit_state_tid &	g2
	)

inline

overloading the operator ==, return true if g1 == g2 and false otherwise

Parameters

g1
g2

Returns: bool

◆ operator==() [6/7]

template<typename T >

bool ruba::operator==	(	const sstack< T > &	a1,
		const sstack< T > &	a2
	)

inline

overloading operator ==

Parameters

a1
a2

Returns: bool

◆ operator==() [7/7]

bool ruba::operator==	(	const thread_state &	c1,
		const thread_state &	c2
	)

inline

overloading operator ==

Parameters

c1
c2

Returns: bool

◆ operator>() [1/7]

bool ruba::operator>	(	const fsa_transition &	r1,
		const fsa_transition &	r2
	)

inline

overloading operator >

Parameters

r1
r2

Returns: bool

◆ operator>() [2/7]

bool ruba::operator>	(	const visible_state &	s1,
		const visible_state &	s2
	)

inline

overloading operator >, return true if s1 > s2 and false otherwise

Parameters

s1	a visible state
s2	a visible state

Returns: bool

◆ operator>() [3/7]

bool ruba::operator>	(	const explicit_state &	g1,
		const explicit_state &	g2
	)

inline

overloading the operator >

Parameters

g1
g2

Returns: bool

◆ operator>() [4/7]

bool ruba::operator>	(	const thread_visible_state &	t1,
		const thread_visible_state &	t2
	)

inline

overloading operator >

Parameters

t1
t2

Returns: bool

◆ operator>() [5/7]

bool ruba::operator>	(	const explicit_state_tid &	g1,
		const explicit_state_tid &	g2
	)

inline

overloading the operator >, return true if g1 > g2 and false otherwise

Parameters

g1
g2

Returns: bool

◆ operator>() [6/7]

template<typename T >

bool ruba::operator>	(	const sstack< T > &	a1,
		const sstack< T > &	a2
	)

inline

overloading operator >

Parameters

a1
a2

Returns: bool

◆ operator>() [7/7]

bool ruba::operator>	(	const thread_state &	c1,
		const thread_state &	c2
	)

inline

overloading operator >

Parameters

c1
c2

Returns: bool

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ concurrent_pushdown_automata

◆ finite_machine

◆ id_action

◆ pda_stack

Enumeration Type Documentation

◆ sequence

◆ type_stack_operation

◆ type_synchronization

Function Documentation

◆ operator!=() [1/7]

◆ operator!=() [2/7]

◆ operator!=() [3/7]

◆ operator!=() [4/7]

◆ operator!=() [5/7]

◆ operator!=() [6/7]

◆ operator!=() [7/7]

◆ operator<() [1/7]

◆ operator<() [2/7]

◆ operator<() [3/7]

◆ operator<() [4/7]

◆ operator<() [5/7]

◆ operator<() [6/7]

◆ operator<() [7/7]

◆ operator<<() [1/13]

◆ operator<<() [2/13]

◆ operator<<() [3/13]

◆ operator<<() [4/13]

◆ operator<<() [5/13]

◆ operator<<() [6/13]

◆ operator<<() [7/13]

◆ operator<<() [8/13]

◆ operator<<() [9/13]

◆ operator<<() [10/13]

◆ operator<<() [11/13]

◆ operator<<() [12/13]

◆ operator<<() [13/13]

◆ operator==() [1/7]

◆ operator==() [2/7]

◆ operator==() [3/7]

◆ operator==() [4/7]

◆ operator==() [5/7]

◆ operator==() [6/7]

◆ operator==() [7/7]

◆ operator>() [1/7]

◆ operator>() [2/7]

◆ operator>() [3/7]

◆ operator>() [4/7]

◆ operator>() [5/7]

◆ operator>() [6/7]

◆ operator>() [7/7]