Detailed Description

An automata representation of a TESLA assertion.

This representation can be either deterministic (for easy generation of instrumentation code) or non-deterministic (for easy creation and analysis).

An Automaton owns its consituent State objects; Transition ownership rests with the State objects.

Definition at line 74 of file Automaton.h.

#include "Automaton.h"

Inheritance diagram for tesla::Automaton:

Collaboration diagram for tesla::Automaton:

Public Types
enum	Type { Unlinked, Linked, Deterministic }
	Automata representations, in increasing order of realisability. More...

typedef llvm::SmallVector < State *, 10 >	StateVector

Public Member Functions
virtual	~Automaton ()

virtual bool	IsRealisable () const

size_t	ID () const

const AutomatonDescription &	getAssertion () const

const Usage *	Use () const

size_t	StateCount () const

size_t	TransitionCount () const

std::string	Name () const
	Short, unique name. More...

std::string	String () const
	Human-readable representation. More...

std::string	Dot () const
	GraphViz representation. More...

TransitionSets::const_iterator	begin () const
	Iterate over state transitions. More...

TransitionSets::const_iterator	end () const

Protected Member Functions
	Automaton (size_t id, const AutomatonDescription &, const Usage , llvm::StringRef Name, llvm::ArrayRef< State >, const TransitionSets &)

Protected Attributes
const size_t	id

const AutomatonDescription &	assertion
	Automaton states. More...

const Usage *	use
	How the automaton is used. More...

const std::string	name

StateVector	States

TransitionSets	Transitions

Friends
class	internal::DFABuilder

Member Typedef Documentation

typedef llvm::SmallVector<State*,10> tesla::Automaton::StateVector

Definition at line 92 of file Automaton.h.

Member Enumeration Documentation

enum tesla::Automaton::Type

Automata representations, in increasing order of realisability.

Enumerator

Unlinked

An NFA representation that includes sub-automata pseudo-transitions, e.g.

"transition from state 2 to state 8 via sub-automaton 'active_close'".

Linked

An NFA with realisable transitions.

Deterministic

A DFA that can actually be implemented as instrumentation.

Definition at line 78 of file Automaton.h.

             {
     Unlinked,
 
     Linked,
 
     Deterministic,
   };

Constructor & Destructor Documentation

virtual tesla::Automaton::~Automaton ( )

inlinevirtual

Definition at line 95 of file Automaton.h.

95 {}

tesla::Automaton::Automaton	(	size_t	id,
		const AutomatonDescription &	,
		const Usage *	,
		llvm::StringRef	Name,
		llvm::ArrayRef< State * >	,
		const TransitionSets &
	)

protected

Definition at line 131 of file Automaton.cpp.

References tesla::Usage::identifier, tesla::AutomatonDescription::identifier, and States.

   : id(id), assertion(A), use(Use), name(Name), Transitions(Transitions)
 {
   assert(!Use || A.identifier() == Use->identifier());
   States.insert(States.begin(), S.begin(), S.end());
 }

Member Function Documentation

TransitionSets::const_iterator tesla::Automaton::begin ( ) const

inline

Iterate over state transitions.

Definition at line 109 of file Automaton.h.

References Transitions.

109 { return Transitions.begin(); }

string tesla::Automaton::Dot ( ) const

GraphViz representation.

Definition at line 163 of file Automaton.cpp.

References Name(), States, and Transitions.

                             {
   stringstream ss;
   ss
     << "/*\n"
     << " * " << Name() << "\n"
     << " */\n"
     << "digraph automaton_" << id << " {\n"
     << "\tgraph [ truecolor=true, bgcolor=\"transparent\", dpi = 60 ];\n"
     << "\tnode ["
     << " shape = circle,"
     << " fontname = \"Monospace\","
     << " style = filled, fillcolor = \"white\""
     << "];\n"
     << "\tedge [ fontname = \"Monospace\" ];\n"
     << "\n"
     ;
 
   for (State *S : States) {
     ss << "\t" << S->Dot() << "\n";
   }
 
   int i = 0;
   for (auto EquivalenceClass : Transitions) {
     string color = ("\"/dark28/" + Twine(i++ % 8 + 1) + "\"").str();
     auto *Head = *EquivalenceClass.begin();
 
     ss
       << "\n\t/*\n"
       << "\t * " << Head->ShortLabel() << "\n"
       << "\t */\n"
       << "\tedge [ "
       << "color = " << color << ", "
       << "fontcolor = " << color << ",\n\t\t"
       << "label = \"" << Head->DotLabel();
 
     if (Head->RequiresInit())
       ss << "\\n&laquo;init&raquo;";
 
     if (Head->RequiresCleanup())
       ss << "\\n&laquo;cleanup&raquo;";
 
     ss
       << "\""
       << " ];\n";
 
     for (auto *T : EquivalenceClass)
       ss
         << "\t" << T->Source().ID() << " -> " << T->Destination().ID() << ";\n"
         ;
   }
 
   ss
     << "\n\t/*\n"
     << "\t * Footer:\n"
     << "\t */\n"
     << "\tfontname = \"Monospace\";\n"
     << "\tlabel = \"" << Name() << "\";\n"
     << "\tlabelloc = top;\n"
     << "\tlabeljust = left;\n"
     << "}";
 
   return ss.str();
 }

Here is the call graph for this function:

TransitionSets::const_iterator tesla::Automaton::end ( ) const

inline

Definition at line 110 of file Automaton.h.

References Transitions.

110 { return Transitions.end(); }

const AutomatonDescription& tesla::Automaton::getAssertion ( ) const

inline

Definition at line 99 of file Automaton.h.

References assertion.

Referenced by tesla::FieldInstrumentation::AppendInstrumentation(), tesla::FnInstrumentation::AppendInstrumentation(), and tesla::internal::DFABuilder::ConstructDFA().

99 { return assertion; }

Here is the caller graph for this function:

size_t tesla::Automaton::ID ( ) const

inline

Definition at line 98 of file Automaton.h.

References id.

Referenced by tesla::FieldInstrumentation::AppendInstrumentation(), tesla::FnInstrumentation::AppendInstrumentation(), and tesla::internal::DFABuilder::ConstructDFA().

98 { return id; }

Here is the caller graph for this function:

bool tesla::Automaton::IsRealisable ( ) const

virtual

Reimplemented in tesla::DFA.

Definition at line 140 of file Automaton.cpp.

References Transitions.

                                    {
   for (auto i : Transitions)
     for (const Transition *T : i)
       if (!T->IsRealisable())
         return false;
 
   return true;
 }

std::string tesla::Automaton::Name ( ) const

inline

Short, unique name.

Definition at line 104 of file Automaton.h.

References name.

Referenced by tesla::FieldInstrumentation::AppendInstrumentation(), tesla::FnInstrumentation::AppendInstrumentation(), tesla::internal::DFABuilder::ConstructDFA(), Dot(), and String().

Here is the caller graph for this function:

size_t tesla::Automaton::StateCount ( ) const

inline

Definition at line 101 of file Automaton.h.

References States.

101 { return States.size(); }

string tesla::Automaton::String ( ) const

Human-readable representation.

Definition at line 149 of file Automaton.cpp.

References Name(), and States.

Referenced by tesla::FieldInstrumentation::AppendInstrumentation(), tesla::FnInstrumentation::AppendInstrumentation(), tesla::internal::DFABuilder::ConstructDFA(), and main().

                                {
   stringstream ss;
   ss << "automaton '" << Name() << "' {\n";
 
   for (State *S : States) {
     assert(S != NULL);
     ss << "\t" << S->String() << "\n";
   }
 
   ss << "}";
 
   return ss.str();
 }

Here is the call graph for this function:

Here is the caller graph for this function:

size_t tesla::Automaton::TransitionCount ( ) const

inline

Definition at line 102 of file Automaton.h.

References Transitions.

102 { return Transitions.size(); }

const Usage* tesla::Automaton::Use ( ) const

inline

Definition at line 100 of file Automaton.h.

References use.

Referenced by tesla::internal::DFABuilder::ConstructDFA().

100 { return use; }

Here is the caller graph for this function:

Friends And Related Function Documentation

friend class internal::DFABuilder

friend

Definition at line 75 of file Automaton.h.

Member Data Documentation

const AutomatonDescription& tesla::Automaton::assertion

protected

Automaton states.

Definition at line 118 of file Automaton.h.

Referenced by getAssertion(), and tesla::NFA::Link().

const size_t tesla::Automaton::id

protected

Definition at line 117 of file Automaton.h.

Referenced by ID().

const std::string tesla::Automaton::name

protected

Definition at line 120 of file Automaton.h.

Referenced by Name().

StateVector tesla::Automaton::States

protected

Definition at line 122 of file Automaton.h.

Referenced by Automaton(), tesla::internal::DFABuilder::ConstructDFA(), Dot(), StateCount(), and String().

TransitionSets tesla::Automaton::Transitions

protected

Definition at line 123 of file Automaton.h.

Referenced by begin(), Dot(), end(), IsRealisable(), and TransitionCount().

const Usage* tesla::Automaton::use

protected

How the automaton is used.

Definition at line 119 of file Automaton.h.

Referenced by tesla::NFA::Link(), and Use().

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

tesla/common/Automaton.h
tesla/common/Automaton.cpp

Computer Laboratory

Detailed Description

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Friends

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation