mCRL2
Loading...
Searching...
No Matches
specification.h File Reference

The class specification. More...

Go to the source code of this file.

Classes

class  mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >
 
class  mcrl2::lps::specification
 Linear process specification. More...
 

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::lps
 The main namespace for the LPS library.
 

Functions

template<typename Object >
bool mcrl2::lps::check_well_typedness (const Object &o)
 
template<typename LinearProcess , typename InitialProcessExpression >
atermpp::aterm mcrl2::lps::specification_to_aterm (const specification_base< LinearProcess, InitialProcessExpression > &spec)
 Conversion to aterm.
 
void mcrl2::lps::complete_data_specification (specification &spec)
 Adds all sorts that appear in the process of l to the data specification of l.
 
bool mcrl2::lps::check_well_typedness (const specification &x)
 
void mcrl2::lps::normalize_sorts (lps::specification &x, const data::sort_specification &sortspec)
 
bool mcrl2::lps::is_specification (const atermpp::aterm &x)
 Test for a specification expression.
 
std::string mcrl2::lps::pp (const specification &x)
 
std::ostream & mcrl2::lps::operator<< (std::ostream &out, const specification &x)
 
std::string mcrl2::lps::pp_with_summand_numbers (const specification &x)
 
std::set< data::sort_expressionmcrl2::lps::find_sort_expressions (const lps::specification &x)
 
std::set< data::variablemcrl2::lps::find_all_variables (const lps::specification &x)
 
std::set< data::variablemcrl2::lps::find_free_variables (const lps::specification &x)
 
std::set< data::function_symbolmcrl2::lps::find_function_symbols (const lps::specification &x)
 
std::set< core::identifier_stringmcrl2::lps::find_identifiers (const lps::specification &x)
 
std::set< process::action_labelmcrl2::lps::find_action_labels (const lps::specification &x)
 
bool mcrl2::lps::operator== (const specification &spec1, const specification &spec2)
 Equality operator.
 
bool mcrl2::lps::operator!= (const specification &spec1, const specification &spec2)
 Inequality operator.
 

Detailed Description

The class specification.

Definition in file specification.h.