12#ifndef MCRL2_PBES_TOOLS_PBESABSTRACT_H
13#define MCRL2_PBES_TOOLS_PBESABSTRACT_H
22namespace pbes_system {
25 const std::string& output_filename,
28 const std::string& parameter_selection,
34 load_pbes(p, input_filename, input_format);
45 algorithm.
run(p, parameter_map, value_true);
48 save_pbes(p, output_filename, output_format);
The PBES abstract algorithm.
Algorithm class for the abstract algorithm.
void run(pbes &p, const detail::pbes_parameter_map ¶meter_map, bool value_true)
Runs the algorithm.
parameterized boolean equation system
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
std::map< core::identifier_string, std::vector< data::variable > > pbes_parameter_map
Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
pbes_parameter_map parse_pbes_parameter_map(const pbes &p, const std::string &text)
Parses parameter selection for finite pbesinst algorithm.
void pbesabstract(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string ¶meter_selection, bool value_true)
void load_pbes(pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &source="")
Load a PBES from file.
void save_pbes(const pbes &pbes, std::ostream &stream, utilities::file_format format=utilities::file_format())
Save a PBES in the format specified.
bool is_normalized(const T &x)
Checks if a pbes expression is normalized.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
IO routines for boolean equation systems.
Normalization of pbes expressions.