Partitions the system into environment and IUT according to TRON assumptions. More...

#include <signalflow.h>

Inheritance diagram for UTAP::Partitioner:

Collaboration diagram for UTAP::Partitioner:

[legend]

Public Member Functions
	Partitioner (const char *_title, TimedAutomataSystem &ta)

	~Partitioner ()

int	partition (const strs_t &inputs, const strs_t &outputs)

int	partition (std::istream &ioinfo)

void	printForDot (std::ostream &os, bool ranked, bool erd, bool cEdged) override
	Print I/O information in DOT format into given output stream. More...

void	printViolation (const proc_t process, const char variable)

void	fillWithEnvProcs (strs_t &procs)

void	fillWithIUTProcs (strs_t &procs)

Public Member Functions inherited from UTAP::SignalFlow
	SignalFlow (const char *_title, TimedAutomataSystem &ta)
	Analyse the system and extract I/O information: More...

void	setVerbose (int verbose)

virtual	~SignalFlow ()
	All strings are from TASystem (don't dispose TASystem before SignalFlow). More...

void	printForTron (std::ostream &os)
	Print I/O information in TRON format into given output stream. More...

int32_t	visitEmptyStatement (EmptyStatement *stat) override
	System visitor pattern extracts read/write information from UCode. More...

int32_t	visitExprStatement (ExprStatement *stat) override

int32_t	visitForStatement (ForStatement *stat) override

int32_t	visitIterationStatement (IterationStatement *stat) override

int32_t	visitWhileStatement (WhileStatement *stat) override

int32_t	visitDoWhileStatement (DoWhileStatement *stat) override

int32_t	visitBlockStatement (BlockStatement *stat) override

int32_t	visitSwitchStatement (SwitchStatement *stat) override

int32_t	visitCaseStatement (CaseStatement *stat) override

int32_t	visitDefaultStatement (DefaultStatement *stat) override

int32_t	visitIfStatement (IfStatement *stat) override

int32_t	visitBreakStatement (BreakStatement *stat) override

int32_t	visitContinueStatement (ContinueStatement *stat) override

int32_t	visitReturnStatement (ReturnStatement *stat) override

int32_t	visitAssertStatement (UTAP::AssertStatement *stat) override

Public Member Functions inherited from UTAP::StatementVisitor
virtual	~StatementVisitor ()

Protected Member Functions
void	addProcs (const strs_t &chans, const str2procs_t &index, procs_t &result, procs_t &exclude)
	Adds processes to the result which use the channels from chans list according to index. More...

void	addIntChans (const procs_t &procs, strs_t &result, strs_t &exclude)
	Takes the internal channels of each process from procs list and adds them to the result list. More...

void	addIntVars (const procs_t &procs, strs_t &result, strs_t &exclude)
	Takes the variables of each process from procs list and adds them to the result list. More...

void	addProcsByVars (const strs_t &vars, procs_t &procs, procs_t &exclude)
	Take all variables and add all accessing processes to the list. More...

Protected Member Functions inherited from UTAP::SignalFlow
bool	checkParams (const symbol_t &s)

void	addChan (const std::string &, strs_t &, str2procs_t &)

void	addVar (const symbol_t &, str2strs_t &, str2procs_t &)

void	visitProcess (instance_t &)

void	visitExpression (const expression_t &)

void	pushIO ()

void	popIO ()

virtual void	printProcsForDot (std::ostream &os, bool erd)

virtual void	printVarsForDot (std::ostream &os, bool ranked, bool erd)

virtual void	printVarsWriteForDot (std::ostream &os)

virtual void	printVarsReadForDot (std::ostream &os)

virtual void	printChansOnEdgesForDot (std::ostream &os)

virtual void	printChansSeparateForDot (std::ostream &os, bool ranked, bool erd)

Protected Attributes
procs_t	procsEnv

procs_t	procsIUT

procs_t	procsBad

strs_t	chansIntEnv

strs_t	chansIntIUT

strs_t	observable

strs_t	chansBad

strs_t	varsEnv

strs_t	varsIUT

strs_t	varsBad

strs_t	chansInp

strs_t	chansOut

const char *	rule

Protected Attributes inherited from UTAP::SignalFlow
int	verbosity

const char *	title

procs_t	procs

str2procs_t	receivers

str2procs_t	transmitters

strs_t	processes

strs_t	channels

strs_t	variables

proc_t *	cTA

instance_t *	cP

const char *	cChan

std::string	chanString

bool	inp

bool	out

bool	sync

bool	paramsExpanded

std::stack< std::pair< bool, bool > >	ioStack

std::stack< exprref_t >	refparams

std::stack< exprref_t >	valparams

Additional Inherited Members
Public Types inherited from UTAP::SignalFlow
typedef std::set< const char *, const less_str >	strs_t

typedef std::map< const proc_t *, strs_t >	proc2strs_t

typedef std::map< const char *, strs_t >	str2strs_t

typedef std::set< proc_t * >	procs_t

typedef std::map< const char *, procs_t, less_str >	str2procs_t

typedef std::map< const symbol_t, expression_t >	exprref_t

Detailed Description

Partitions the system into environment and IUT according to TRON assumptions.

inputs/outputs are channel names. Environment processes shout on inputs and listens to outputs, while IUT processes shout on outputs and listen to inputs. There are additional rules to complete the partitioning (to cathegorize the internal processes): 1) channels, that are not declared as inputs/outputs, are non-observable, called internal. 2) internal channel belongs to environment (IUT) if it is used by environment (IUT) process (respectively). Model is inconsistent and cannot be partitioned if the internal channel is used by both environment and IUT. 3) process belongs to environment (IUT) if it uses the internal environment (IUT) channel (respectively). 4) variable belongs to environment (IUT) if it is accessed by environment (IUT) process without observable input/output channel synchronization. Variable is not cathegorized (can be either) if accessed consistently only during observable input/output channel synchronization. 5) process belongs to environment (IUT) if accesses environment (IUT) variable (respectively) without observable channel synchronization. Returns: 0 if partitioning was consistent and complete, 1 if partitioning was consistent but incomplete (some proc/chan is free) 2 if partitioning was inconsistent (some proc/chan/var is both Env and IUT)

Definition at line 228 of file signalflow.h.

Constructor & Destructor Documentation

◆ Partitioner()

UTAP::Partitioner::Partitioner	(	const char *	_title,
		TimedAutomataSystem &	ta
	)

inline

Definition at line 246 of file signalflow.h.

References UTAP::SignalFlow::printForDot(), and UTAP::SignalFlow::procs.

Here is the call graph for this function:

◆ ~Partitioner()

Partitioner::~Partitioner ( )

Definition at line 797 of file signalflow.cpp.

References free().

Here is the call graph for this function:

Member Function Documentation

◆ addIntChans()

void Partitioner::addIntChans	(	const procs_t &	procs,
		strs_t &	result,
		strs_t &	exclude
	)

protected

Takes the internal channels of each process from procs list and adds them to the result list.

Reports inconcistency if channel is in the exclude list.

Definition at line 850 of file signalflow.cpp.

References UTAP::SignalFlow::verbosity.

◆ addIntVars()

void Partitioner::addIntVars	(	const procs_t &	procs,
		strs_t &	result,
		strs_t &	exclude
	)

protected

Takes the variables of each process from procs list and adds them to the result list.

Reports inconcistency if variable is in the exclude list.

Definition at line 896 of file signalflow.cpp.

References UTAP::SignalFlow::verbosity.

◆ addProcs()

void Partitioner::addProcs	(	const strs_t &	chans,
		const str2procs_t &	index,
		procs_t &	result,
		procs_t &	exclude
	)

protected

Adds processes to the result which use the channels from chans list according to index.

Reports inconsistency if some process happens to be in exclude list.

Definition at line 817 of file signalflow.cpp.

References UTAP::SignalFlow::verbosity.

◆ addProcsByVars()

void Partitioner::addProcsByVars	(	const strs_t &	vars,
		procs_t &	procs,
		procs_t &	exclude
	)

protected

Take all variables and add all accessing processes to the list.

Report inconcistencies if process happens to be in exclude list.

Definition at line 945 of file signalflow.cpp.

References UTAP::SignalFlow::receivers, UTAP::SignalFlow::transmitters, and UTAP::SignalFlow::verbosity.

◆ fillWithEnvProcs()

void Partitioner::fillWithEnvProcs ( strs_t & procs )

Definition at line 1507 of file signalflow.cpp.

◆ fillWithIUTProcs()

void Partitioner::fillWithIUTProcs ( strs_t & procs )

Definition at line 1513 of file signalflow.cpp.

◆ partition() [1/2]

int Partitioner::partition	(	const strs_t &	inputs,
		const strs_t &	outputs
	)

Definition at line 1071 of file signalflow.cpp.

References free(), UTAP::SignalFlow::procs, UTAP::SignalFlow::receivers, UTAP::SignalFlow::transmitters, and UTAP::SignalFlow::verbosity.

Referenced by get_token(), and main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ partition() [2/2]

int UTAP::Partitioner::partition ( std::istream & ioinfo )

◆ printForDot()

void Partitioner::printForDot	(	std::ostream &	os,
		bool	ranked,
		bool	erd,
		bool	cEdged
	)

overridevirtual

Print I/O information in DOT format into given output stream.

ranked – puts oposite "ranks" on variables and channels erd – puts boxes and diamonds rather than (compact) ellipses. cEdged – channels are printed on edges rather than separate nodes.

Reimplemented from UTAP::SignalFlow.

Definition at line 1213 of file signalflow.cpp.

References BADSTYLE, ch, UTAP::SignalFlow::channels, ENVSTYLE, IUTSTYLE, MEDSTYLE, UTAP::SignalFlow::processes, UTAP::SignalFlow::procs, UTAP::SignalFlow::receivers, set_remove(), UTAP::SignalFlow::title, UTAP::SignalFlow::transmitters, and UTAP::SignalFlow::variables.

Here is the call graph for this function:

◆ printViolation()

void Partitioner::printViolation	(	const proc_t *	process,
		const char *	variable
	)

inline

Definition at line 805 of file signalflow.cpp.

References UTAP::SignalFlow::proc_t::name, and UTAP::SignalFlow::verbosity.

Member Data Documentation

◆ chansBad

strs_t UTAP::Partitioner::chansBad

protected

Definition at line 232 of file signalflow.h.

◆ chansInp

strs_t UTAP::Partitioner::chansInp

protected

Definition at line 234 of file signalflow.h.

◆ chansIntEnv

strs_t UTAP::Partitioner::chansIntEnv

protected

Definition at line 232 of file signalflow.h.

◆ chansIntIUT

strs_t UTAP::Partitioner::chansIntIUT

protected

Definition at line 232 of file signalflow.h.

◆ chansOut

strs_t UTAP::Partitioner::chansOut

protected

Definition at line 234 of file signalflow.h.

◆ observable

strs_t UTAP::Partitioner::observable

protected

Definition at line 232 of file signalflow.h.

◆ procsBad

procs_t UTAP::Partitioner::procsBad

protected

Definition at line 231 of file signalflow.h.

◆ procsEnv

procs_t UTAP::Partitioner::procsEnv

protected

Definition at line 231 of file signalflow.h.

◆ procsIUT

procs_t UTAP::Partitioner::procsIUT

protected

Definition at line 231 of file signalflow.h.

◆ rule

const char* UTAP::Partitioner::rule

protected

Definition at line 235 of file signalflow.h.

◆ varsBad

strs_t UTAP::Partitioner::varsBad

protected

Definition at line 233 of file signalflow.h.

◆ varsEnv

strs_t UTAP::Partitioner::varsEnv

protected

Definition at line 233 of file signalflow.h.

◆ varsIUT

strs_t UTAP::Partitioner::varsIUT

protected

Definition at line 233 of file signalflow.h.

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

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Partitioner()

◆ ~Partitioner()

Member Function Documentation

◆ addIntChans()

◆ addIntVars()

◆ addProcs()

◆ addProcsByVars()

◆ fillWithEnvProcs()

◆ fillWithIUTProcs()

◆ partition() [1/2]

◆ partition() [2/2]

◆ printForDot()

◆ printViolation()

Member Data Documentation

◆ chansBad

◆ chansInp

◆ chansIntEnv

◆ chansIntIUT

◆ chansOut

◆ observable

◆ procsBad

◆ procsEnv

◆ procsIUT

◆ rule

◆ varsBad

◆ varsEnv

◆ varsIUT