mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::detail Namespace Reference

Classes

struct  action_rename_actions
 
struct  add_capture_avoiding_replacement
 
struct  add_capture_avoiding_replacement_with_an_identifier_generator
 
struct  cache_equality
 
struct  cache_hash
 
struct  cheap_cache_key
 
class  Confluence_Checker
 
class  data_equation_argument_generator
 Fresh variable generator for the arguments of a function symbol. More...
 
struct  data_rewriter_builder
 
class  Disjointness_Checker
 
struct  if_rewrite_builder
 
class  Invariant_Checker
 
struct  is_singleton_sort
 Function object that checks if a sort is a singleton sort. Note that it is an approximation, meaning that in some cases it may return false whereas in reality the answer is true. More...
 
struct  is_stochastic_traverser
 
struct  is_trivial_summand
 Function object that checks if a summand has a false condition. More...
 
class  lps_algorithm
 Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::specification and lps::stochastic_specification. More...
 
struct  lps_command
 
struct  lps_rewriter_command
 PBES command that uses a rewrite strategy. More...
 
struct  lps_well_typed_checker
 Function object for applying a substitution to LPS data types. More...
 
struct  make_timed_lps_summand
 Adds a time parameter t to s if needed and returns the result. The time t is chosen such that it doesn't appear in context. More...
 
struct  multi_action_actions
 
struct  one_point_condition_rewrite_builder
 
struct  one_point_rule_rewrite_builder
 
class  pattern_match_unfolder
 Class for unfolding expressions f(a1,...,an) based on the pattern-matching rewrite rules that define f. More...
 
struct  printer
 
struct  remove_parameters_builder
 Traverser for removing parameters from LPS data types. These parameters can be either process parameters or free variables. Assignments to these parameters are removed as well. More...
 
struct  replace_constants_by_variables_builder
 
struct  replace_pattern_match_builder
 
class  specification_property_map
 Stores the following properties of a linear process specification: More...
 
class  ultimate_delay
 
class  unfold_data_manager
 

Functions

process::action_label rename_action_label (const process::action_label &act, const std::regex &matching_regex, const std::string &replacing_fmt)
 
data::data_expression make_and (const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3)
 
data::data_expression make_and (const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3, const data::data_expression &x4)
 
data::data_expression equal_to (const data::data_expression_list &x, const data::data_expression_list &y)
 
std::pair< std::size_t, std::size_t > make_sorted_pair (std::size_t i, std::size_t j)
 
data::data_expression make_forall_ (const data::data_expression &x)
 
process::action_label make_ctau_act_id ()
 Creates an identifier for the for the ctau action.
 
process::action make_ctau_action ()
 Creates the ctau action.
 
static data::mutable_map_substitution get_substitutions_from_assignments (const data::assignment_list &a_assignments)
 
static data::data_expression get_subst_equation_from_assignments (const data::variable_list &a_variables, data::assignment_list a_assignments_1, data::assignment_list a_assignments_2, data::mutable_map_substitution<> &a_substitutions_1, data::mutable_map_substitution<> &a_substitutions_2)
 
static data::data_expression get_equation_from_assignments (const data::variable_list &a_variables, data::assignment_list a_assignments_1, data::assignment_list a_assignments_2)
 
data::data_expression get_subst_equation_from_actions (const process::action_list &a_actions, data::mutable_map_substitution<> &a_substitutions)
 
static data::assignment_list get_full_assignment_list (data::assignment_list a_assignment_list, const data::variable_list &a_variables)
 
template<typename ActionSummand >
data::data_expression get_confluence_condition (const data::data_expression &a_invariant, const ActionSummand &a_summand_1, const ActionSummand &a_summand_2, const data::variable_list &a_variables, const char condition_type)
 
template<typename Specification >
bool has_ctau_action (const Specification &a_lps)
 
bool check_action_sorts (const process::action_list &actions, const std::set< data::sort_expression > &sorts)
 Returns true if the sorts of the given actions are contained in sorts.
 
bool check_action_labels (const process::action_list &actions, const std::set< process::action_label > &labels)
 Returns true if the labels of the given actions are contained in labels.
 
bool check_action_label_sorts (const process::action_label_list &action_labels, const std::set< data::sort_expression > &sorts)
 Returns true if the sorts of the given action labels are contained in sorts.
 
template<typename Specification >
void replace_global_variables (Specification &lpsspec, const data::mutable_map_substitution<> &sigma)
 Applies a global variable substitution to an LPS.
 
template<typename Specification >
data::mutable_map_substitution instantiate_global_variables (Specification &lpsspec)
 Eliminates the global variables of an LPS, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
 
template<class LINEAR_PROCESS >
void make_timed_lps (LINEAR_PROCESS &lps, const std::set< core::identifier_string > &context, typename std::enable_if< std::is_same< LINEAR_PROCESS, linear_process >::value||std::is_same< LINEAR_PROCESS, stochastic_linear_process >::value >::type *=nullptr)
 Adds time parameters to the lps if needed and returns the result. The times are chosen such that they don't appear in context.
 
bool match_selection (const data::variable &v, const std::string &name, const std::string &type, const data::data_specification &data_spec)
 Returns true if the selection name:type matches with the variable v.
 
template<typename OutputIterator >
std::vector< data::variablefind_matching_parameters (const data::variable_list &params, const data::data_specification &dataspec, const std::vector< std::pair< std::string, std::string > > &selections, OutputIterator o)
 Find parameter declarations that match a given string.
 
std::vector< data::variableparse_lps_parameter_selection (const data::variable_list &params, const data::data_specification &dataspec, const std::string &text)
 Parses parameter selection for finite pbesinst algorithm.
 
std::string ABP_SPECIFICATION ()
 
std::string DINING3_SPECIFICATION ()
 
std::string ONE_BIT_SLIDING_WINDOW_SPECIFICATION ()
 
std::string LINEAR_ABP_SPECIFICATION ()
 
ultimate_delay combine_ultimate_delays (const ultimate_delay &delay1, const ultimate_delay &delay2)
 Returns the conjunction of the two delay conditions and the join of the variables, where the variables in delay2 are renamed to avoid conflict with those in delay1.

 
template<typename T >
bool is_well_typed (const T &x)
 Checks well typedness of an LPS object.
 
template<typename T >
bool check_well_typedness (const T &x)
 Checks well typedness of an LPS object, and will print error messages to stderr.
 
template<typename Summand >
Summand make_action_summand (const data::variable_list &, const data::data_expression &, const multi_action &, const data::assignment_list &, const stochastic_distribution &)
 
template<>
action_summand make_action_summand< action_summand > (const data::variable_list &summation_variables, const data::data_expression &condition, const multi_action &a, const data::assignment_list &assignments, const stochastic_distribution &distribution)
 
data::data_expression unfold_pattern_matching (const data::data_expression &x, pattern_match_unfolder &unfolder)
 
void collect_transition_variables (const action_summand &s, std::set< data::variable > &result)
 
void collect_transition_variables (const stochastic_action_summand &s, std::set< data::variable > &result)
 
void collect_transition_variables (const deadlock_summand &s, std::set< data::variable > &result)
 
process::untyped_multi_action parse_multi_action_new (const std::string &text)
 
multi_action complete_multi_action (process::untyped_multi_action &x, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
 
multi_action complete_multi_action (process::untyped_multi_action &x, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
 
action_rename_specification parse_action_rename_specification_new (const std::string &text)
 
void complete_action_rename_specification (action_rename_specification &x, const lps::stochastic_specification &spec)
 
std::size_t greatest_common_divisor (std::size_t x, std::size_t y)
 
void remove_common_divisor (std::size_t &enumerator, std::size_t &denominator)
 
template<typename VariableContainer >
std::set< core::identifier_stringvariable_names (const VariableContainer &vars)
 
template<typename VariableContainer >
std::set< core::identifier_stringvariable_name_clashes (const VariableContainer &vars, const std::set< core::identifier_string > &w)
 
void resolve_summand_variable_name_clashes (action_summand &summand, const std::set< core::identifier_string > &process_parameter_names, data::set_identifier_generator &generator)
 
void resolve_summand_variable_name_clashes (deadlock_summand &summand, const std::set< core::identifier_string > &process_parameter_names, data::set_identifier_generator &generator)
 
void resolve_summand_variable_name_clashes (stochastic_action_summand &summand, const std::set< core::identifier_string > &process_parameter_names, data::set_identifier_generator &generator)
 
void find_equality_conjuncts (const data::data_expression &x, std::map< data::variable, data::data_expression > &result)
 
template<>
stochastic_action_summand make_action_summand< stochastic_action_summand > (const data::variable_list &summation_variables, const data::data_expression &condition, const multi_action &a, const data::assignment_list &assignments, const stochastic_distribution &distribution)
 
stochastic_action_summand_vector convert_action_summands (const action_summand_vector &action_summands)
 
template<class INITIALIZER >
INITIALIZER make_process_initializer (const data::data_expression_list &expressions, const INITIALIZER &init)
 
template<>
process_initializer make_process_initializer (const data::data_expression_list &expressions, const process_initializer &)
 
template<>
stochastic_process_initializer make_process_initializer (const data::data_expression_list &expressions, const stochastic_process_initializer &init)
 
std::string NO_DEADLOCK ()
 
std::string NO_LIVELOCK ()
 

Function Documentation

◆ ABP_SPECIFICATION()

std::string mcrl2::lps::detail::ABP_SPECIFICATION ( )
inline

Definition at line 24 of file test_input.h.

◆ check_action_label_sorts()

bool mcrl2::lps::detail::check_action_label_sorts ( const process::action_label_list action_labels,
const std::set< data::sort_expression > &  sorts 
)
inline

Returns true if the sorts of the given action labels are contained in sorts.

Parameters
action_labelsA sequence of action labels
sortsA set of sort expressions
Returns
True if the sorts of the given action labels are contained in sorts.

Definition at line 70 of file action_utility.h.

◆ check_action_labels()

bool mcrl2::lps::detail::check_action_labels ( const process::action_list actions,
const std::set< process::action_label > &  labels 
)
inline

Returns true if the labels of the given actions are contained in labels.

Parameters
actionsA sequence of actions
labelsA set of action labels
Returns
True if the labels of the given actions are contained in labels.

Definition at line 52 of file action_utility.h.

◆ check_action_sorts()

bool mcrl2::lps::detail::check_action_sorts ( const process::action_list actions,
const std::set< data::sort_expression > &  sorts 
)
inline

Returns true if the sorts of the given actions are contained in sorts.

Parameters
actionsA sequence of actions
sortsA set of sort expressions
Returns
True if the sorts of the given actions are contained in sorts.

Definition at line 32 of file action_utility.h.

◆ check_well_typedness()

template<typename T >
bool mcrl2::lps::detail::check_well_typedness ( const T &  x)

Checks well typedness of an LPS object, and will print error messages to stderr.

Definition at line 395 of file is_well_typed.h.

◆ collect_transition_variables() [1/3]

void mcrl2::lps::detail::collect_transition_variables ( const action_summand s,
std::set< data::variable > &  result 
)
inline

Definition at line 29 of file parelm.h.

◆ collect_transition_variables() [2/3]

void mcrl2::lps::detail::collect_transition_variables ( const deadlock_summand s,
std::set< data::variable > &  result 
)
inline

Definition at line 49 of file parelm.h.

◆ collect_transition_variables() [3/3]

void mcrl2::lps::detail::collect_transition_variables ( const stochastic_action_summand s,
std::set< data::variable > &  result 
)
inline

Definition at line 41 of file parelm.h.

◆ combine_ultimate_delays()

ultimate_delay mcrl2::lps::detail::combine_ultimate_delays ( const ultimate_delay delay1,
const ultimate_delay delay2 
)

Returns the conjunction of the two delay conditions and the join of the variables, where the variables in delay2 are renamed to avoid conflict with those in delay1.

◆ complete_action_rename_specification()

void mcrl2::lps::detail::complete_action_rename_specification ( action_rename_specification x,
const lps::stochastic_specification spec 
)

Definition at line 150 of file lps.cpp.

◆ complete_multi_action() [1/2]

multi_action mcrl2::lps::detail::complete_multi_action ( process::untyped_multi_action x,
const process::action_label_list action_decls,
const data::data_specification data_spec = data::detail::default_specification() 
)

Definition at line 132 of file lps.cpp.

◆ complete_multi_action() [2/2]

multi_action mcrl2::lps::detail::complete_multi_action ( process::untyped_multi_action x,
multi_action_type_checker typechecker,
const data::data_specification data_spec = data::detail::default_specification() 
)

Definition at line 124 of file lps.cpp.

◆ convert_action_summands()

stochastic_action_summand_vector mcrl2::lps::detail::convert_action_summands ( const action_summand_vector action_summands)
inline

Definition at line 38 of file stochastic_linear_process.h.

◆ DINING3_SPECIFICATION()

std::string mcrl2::lps::detail::DINING3_SPECIFICATION ( )
inline

Definition at line 69 of file test_input.h.

◆ equal_to()

data::data_expression mcrl2::lps::detail::equal_to ( const data::data_expression_list x,
const data::data_expression_list y 
)
inline

Definition at line 42 of file confluence.h.

◆ find_equality_conjuncts()

void mcrl2::lps::detail::find_equality_conjuncts ( const data::data_expression x,
std::map< data::variable, data::data_expression > &  result 
)

Definition at line 30 of file one_point_condition_rewrite.h.

◆ find_matching_parameters()

template<typename OutputIterator >
std::vector< data::variable > mcrl2::lps::detail::find_matching_parameters ( const data::variable_list params,
const data::data_specification dataspec,
const std::vector< std::pair< std::string, std::string > > &  selections,
OutputIterator  o 
)
inline

Find parameter declarations that match a given string.

Definition at line 36 of file parameter_selection.h.

◆ get_confluence_condition()

template<typename ActionSummand >
data::data_expression mcrl2::lps::detail::get_confluence_condition ( const data::data_expression a_invariant,
const ActionSummand &  a_summand_1,
const ActionSummand &  a_summand_2,
const data::variable_list a_variables,
const char  condition_type 
)

Definition at line 448 of file confluence_checker.h.

◆ get_equation_from_assignments()

static data::data_expression mcrl2::lps::detail::get_equation_from_assignments ( const data::variable_list a_variables,
data::assignment_list  a_assignments_1,
data::assignment_list  a_assignments_2 
)
inlinestatic

Definition at line 351 of file confluence_checker.h.

◆ get_full_assignment_list()

static data::assignment_list mcrl2::lps::detail::get_full_assignment_list ( data::assignment_list  a_assignment_list,
const data::variable_list a_variables 
)
inlinestatic

Definition at line 414 of file confluence_checker.h.

◆ get_subst_equation_from_actions()

data::data_expression mcrl2::lps::detail::get_subst_equation_from_actions ( const process::action_list a_actions,
data::mutable_map_substitution<> &  a_substitutions 
)
inline

Definition at line 394 of file confluence_checker.h.

◆ get_subst_equation_from_assignments()

static data::data_expression mcrl2::lps::detail::get_subst_equation_from_assignments ( const data::variable_list a_variables,
data::assignment_list  a_assignments_1,
data::assignment_list  a_assignments_2,
data::mutable_map_substitution<> &  a_substitutions_1,
data::mutable_map_substitution<> &  a_substitutions_2 
)
inlinestatic

Definition at line 284 of file confluence_checker.h.

◆ get_substitutions_from_assignments()

static data::mutable_map_substitution mcrl2::lps::detail::get_substitutions_from_assignments ( const data::assignment_list a_assignments)
inlinestatic

Definition at line 271 of file confluence_checker.h.

◆ greatest_common_divisor()

std::size_t mcrl2::lps::detail::greatest_common_divisor ( std::size_t  x,
std::size_t  y 
)
inline

Definition at line 108 of file probabilistic_data_expression.h.

◆ has_ctau_action()

template<typename Specification >
bool mcrl2::lps::detail::has_ctau_action ( const Specification &  a_lps)

Definition at line 563 of file confluence_checker.h.

◆ instantiate_global_variables()

template<typename Specification >
data::mutable_map_substitution mcrl2::lps::detail::instantiate_global_variables ( Specification &  lpsspec)

Eliminates the global variables of an LPS, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

Definition at line 40 of file instantiate_global_variables.h.

◆ is_well_typed()

template<typename T >
bool mcrl2::lps::detail::is_well_typed ( const T &  x)

Checks well typedness of an LPS object.

Definition at line 387 of file is_well_typed.h.

◆ LINEAR_ABP_SPECIFICATION()

std::string mcrl2::lps::detail::LINEAR_ABP_SPECIFICATION ( )
inline

Definition at line 175 of file test_input.h.

◆ make_action_summand()

template<typename Summand >
Summand mcrl2::lps::detail::make_action_summand ( const data::variable_list ,
const data::data_expression ,
const multi_action ,
const data::assignment_list ,
const stochastic_distribution  
)

Definition at line 30 of file linear_process.h.

◆ make_action_summand< action_summand >()

template<>
action_summand mcrl2::lps::detail::make_action_summand< action_summand > ( const data::variable_list summation_variables,
const data::data_expression condition,
const multi_action a,
const data::assignment_list assignments,
const stochastic_distribution distribution 
)
inline

Definition at line 42 of file linear_process.h.

◆ make_action_summand< stochastic_action_summand >()

template<>
stochastic_action_summand mcrl2::lps::detail::make_action_summand< stochastic_action_summand > ( const data::variable_list summation_variables,
const data::data_expression condition,
const multi_action a,
const data::assignment_list assignments,
const stochastic_distribution distribution 
)
inline

Definition at line 27 of file stochastic_linear_process.h.

◆ make_and() [1/2]

data::data_expression mcrl2::lps::detail::make_and ( const data::data_expression x1,
const data::data_expression x2,
const data::data_expression x3 
)
inline

Definition at line 30 of file confluence.h.

◆ make_and() [2/2]

data::data_expression mcrl2::lps::detail::make_and ( const data::data_expression x1,
const data::data_expression x2,
const data::data_expression x3,
const data::data_expression x4 
)
inline

Definition at line 36 of file confluence.h.

◆ make_ctau_act_id()

process::action_label mcrl2::lps::detail::make_ctau_act_id ( )
inline

Creates an identifier for the for the ctau action.

Definition at line 136 of file confluence_checker.h.

◆ make_ctau_action()

process::action mcrl2::lps::detail::make_ctau_action ( )
inline

Creates the ctau action.

Definition at line 148 of file confluence_checker.h.

◆ make_forall_()

data::data_expression mcrl2::lps::detail::make_forall_ ( const data::data_expression x)
inline

Definition at line 61 of file confluence.h.

◆ make_process_initializer() [1/3]

template<class INITIALIZER >
INITIALIZER mcrl2::lps::detail::make_process_initializer ( const data::data_expression_list expressions,
const INITIALIZER &  init 
)

◆ make_process_initializer() [2/3]

template<>
process_initializer mcrl2::lps::detail::make_process_initializer ( const data::data_expression_list expressions,
const process_initializer  
)

Definition at line 31 of file untime.h.

◆ make_process_initializer() [3/3]

template<>
stochastic_process_initializer mcrl2::lps::detail::make_process_initializer ( const data::data_expression_list expressions,
const stochastic_process_initializer init 
)

Definition at line 37 of file untime.h.

◆ make_sorted_pair()

std::pair< std::size_t, std::size_t > mcrl2::lps::detail::make_sorted_pair ( std::size_t  i,
std::size_t  j 
)
inline

Definition at line 55 of file confluence.h.

◆ make_timed_lps()

template<class LINEAR_PROCESS >
void mcrl2::lps::detail::make_timed_lps ( LINEAR_PROCESS &  lps,
const std::set< core::identifier_string > &  context,
typename std::enable_if< std::is_same< LINEAR_PROCESS, linear_process >::value||std::is_same< LINEAR_PROCESS, stochastic_linear_process >::value >::type *  = nullptr 
)

Adds time parameters to the lps if needed and returns the result. The times are chosen such that they don't appear in context.

Parameters
lpsA linear process
contextA term
Returns
A timed linear process

Definition at line 72 of file make_timed_lps.h.

◆ match_selection()

bool mcrl2::lps::detail::match_selection ( const data::variable v,
const std::string &  name,
const std::string &  type,
const data::data_specification data_spec 
)
inline

Returns true if the selection name:type matches with the variable v.

Definition at line 24 of file parameter_selection.h.

◆ NO_DEADLOCK()

std::string mcrl2::lps::detail::NO_DEADLOCK ( )
inline

Definition at line 24 of file test_input.h.

◆ NO_LIVELOCK()

std::string mcrl2::lps::detail::NO_LIVELOCK ( )
inline

Definition at line 30 of file test_input.h.

◆ ONE_BIT_SLIDING_WINDOW_SPECIFICATION()

std::string mcrl2::lps::detail::ONE_BIT_SLIDING_WINDOW_SPECIFICATION ( )
inline

Definition at line 107 of file test_input.h.

◆ parse_action_rename_specification_new()

action_rename_specification mcrl2::lps::detail::parse_action_rename_specification_new ( const std::string &  text)

Definition at line 140 of file lps.cpp.

◆ parse_lps_parameter_selection()

std::vector< data::variable > mcrl2::lps::detail::parse_lps_parameter_selection ( const data::variable_list params,
const data::data_specification dataspec,
const std::string &  text 
)
inline

Parses parameter selection for finite pbesinst algorithm.

Definition at line 59 of file parameter_selection.h.

◆ parse_multi_action_new()

process::untyped_multi_action mcrl2::lps::detail::parse_multi_action_new ( const std::string &  text)

Definition at line 114 of file lps.cpp.

◆ remove_common_divisor()

void mcrl2::lps::detail::remove_common_divisor ( std::size_t &  enumerator,
std::size_t &  denominator 
)
inline

Definition at line 127 of file probabilistic_data_expression.h.

◆ rename_action_label()

process::action_label mcrl2::lps::detail::rename_action_label ( const process::action_label act,
const std::regex &  matching_regex,
const std::string &  replacing_fmt 
)
inline

Definition at line 775 of file action_rename.h.

◆ replace_global_variables()

template<typename Specification >
void mcrl2::lps::detail::replace_global_variables ( Specification &  lpsspec,
const data::mutable_map_substitution<> &  sigma 
)

Applies a global variable substitution to an LPS.

Definition at line 29 of file instantiate_global_variables.h.

◆ resolve_summand_variable_name_clashes() [1/3]

void mcrl2::lps::detail::resolve_summand_variable_name_clashes ( action_summand summand,
const std::set< core::identifier_string > &  process_parameter_names,
data::set_identifier_generator generator 
)
inline

Definition at line 51 of file resolve_name_clashes.h.

◆ resolve_summand_variable_name_clashes() [2/3]

void mcrl2::lps::detail::resolve_summand_variable_name_clashes ( deadlock_summand summand,
const std::set< core::identifier_string > &  process_parameter_names,
data::set_identifier_generator generator 
)
inline

Definition at line 72 of file resolve_name_clashes.h.

◆ resolve_summand_variable_name_clashes() [3/3]

void mcrl2::lps::detail::resolve_summand_variable_name_clashes ( stochastic_action_summand summand,
const std::set< core::identifier_string > &  process_parameter_names,
data::set_identifier_generator generator 
)
inline

Definition at line 93 of file resolve_name_clashes.h.

◆ unfold_pattern_matching()

data::data_expression mcrl2::lps::detail::unfold_pattern_matching ( const data::data_expression x,
pattern_match_unfolder unfolder 
)
inline

Definition at line 561 of file lpsparunfoldlib.h.

◆ variable_name_clashes()

template<typename VariableContainer >
std::set< core::identifier_string > mcrl2::lps::detail::variable_name_clashes ( const VariableContainer &  vars,
const std::set< core::identifier_string > &  w 
)

Definition at line 37 of file resolve_name_clashes.h.

◆ variable_names()

template<typename VariableContainer >
std::set< core::identifier_string > mcrl2::lps::detail::variable_names ( const VariableContainer &  vars)

Definition at line 25 of file resolve_name_clashes.h.