mCRL2
Loading...
Searching...
No Matches
pbesabstract.h
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
12#ifndef MCRL2_PBES_TOOLS_PBESABSTRACT_H
13#define MCRL2_PBES_TOOLS_PBESABSTRACT_H
14
15#include "mcrl2/pbes/io.h"
16#include "mcrl2/pbes/abstract.h"
19
20namespace mcrl2 {
21
22namespace pbes_system {
23
24inline void pbesabstract(const std::string& input_filename,
25 const std::string& output_filename,
26 const utilities::file_format& input_format,
27 const utilities::file_format& output_format,
28 const std::string& parameter_selection,
29 bool value_true
30 )
31{
32 // load the pbes
33 pbes p;
34 load_pbes(p, input_filename, input_format);
35
36 // TODO: let pbesabstract handle ! and => properly
37 if (!is_normalized(p))
38 {
40 }
41
42 // run the algorithm
44 detail::pbes_parameter_map parameter_map = detail::parse_pbes_parameter_map(p, parameter_selection);
45 algorithm.run(p, parameter_map, value_true);
46
47 // save the result
48 save_pbes(p, output_filename, output_format);
49}
50
51} // namespace pbes_system
52
53} // namespace mcrl2
54
55#endif // MCRL2_PBES_TOOLS_PBESABSTRACT_H
The PBES abstract algorithm.
Algorithm class for the abstract algorithm.
Definition abstract.h:120
void run(pbes &p, const detail::pbes_parameter_map &parameter_map, bool value_true)
Runs the algorithm.
Definition abstract.h:126
parameterized boolean equation system
Definition pbes.h:58
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 &parameter_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.
Definition io.cpp:82
void save_pbes(const pbes &pbes, std::ostream &stream, utilities::file_format format=utilities::file_format())
Save a PBES in the format specified.
Definition io.cpp:49
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
add your file description here.
IO routines for boolean equation systems.
Normalization of pbes expressions.