mCRL2
Loading...
Searching...
No Matches
algorithms.cpp
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
17
18namespace mcrl2
19{
20
21namespace pbes_system
22{
23
24namespace algorithms {
25
26void remove_parameters(pbes& x, const std::set<data::variable>& to_be_removed)
27{
28 pbes_system::remove_parameters(x, to_be_removed);
29}
30
31void remove_parameters(pbes& x, const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed)
32{
33 pbes_system::remove_parameters(x, to_be_removed);
34}
35
37{
38 try
39 {
41 }
42 catch (const mcrl2::runtime_error&)
43 {
44 throw mcrl2::runtime_error("The PBES is not monotonic!");
45 }
46}
47
48bool is_normalized(const pbes& x)
49{
51}
52
53void pbesinst_finite(pbes& p, data::rewrite_strategy rewrite_strategy, const std::string& finite_parameter_selection)
54{
55 pbes_system::pbesinst_finite(p, rewrite_strategy, finite_parameter_selection);
56}
57
58std::string print_removed_equations(const std::vector<propositional_variable>& removed)
59{
61}
62
63std::vector<propositional_variable> remove_unreachable_variables(pbes& p)
64{
66}
67
68std::set<data::variable> significant_variables(const pbes_expression& x)
69{
71}
72
73} // namespace algorithms
74
75} // namespace pbes_system
76
77} // namespace mcrl2
78
Term containing a string.
parameterized boolean equation system
Definition pbes.h:58
Standard exception class for reporting runtime errors.
Definition exception.h:27
rewrite_strategy
The strategy of the rewriter.
std::set< data::variable > significant_variables(const pbes_expression &x)
Returns the significant variables of a pbes expression.
void remove_parameters(pbes &x, const std::set< data::variable > &to_be_removed)
Removes parameters from propositional variable instantiations in a pbes expression.
void pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
Apply finite instantiation to the given PBES.
bool is_normalized(const pbes &x)
Checks if a PBEs is normalized.
std::vector< propositional_variable > remove_unreachable_variables(pbes &p)
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
std::string print_removed_equations(const std::vector< propositional_variable > &removed)
Print removed equations.
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
std::string print_removed_equations(const std::vector< propositional_variable > &removed)
T remove_parameters(const T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Removes parameters from propositional variable instantiations in a pbes expression.
void pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
std::set< data::variable > significant_variables(const pbes_expression &x)
void normalize(T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
The function normalize brings (embedded) pbes expressions into positive normal form,...
Definition normalize.h:177
std::vector< propositional_variable > remove_unreachable_variables(pbes &p)
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
bool is_normalized(const T &x)
Checks if a pbes expression is normalized.
Definition normalize.h:166
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Normalization of pbes expressions.
add your file description here.
Functions for removing insignificant parameters from pbes types.
add your file description here.
add your file description here.