mCRL2
Loading...
Searching...
No Matches
pbesstategraph.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_PBESSTATEGRAPH_H
13#define MCRL2_PBES_TOOLS_PBESSTATEGRAPH_H
14
16#include "mcrl2/pbes/io.h"
17
18namespace mcrl2 {
19
20namespace pbes_system {
21
22void pbesstategraph(const std::string& input_filename,
23 const std::string& output_filename,
24 const utilities::file_format& input_format,
25 const utilities::file_format& output_format,
26 const pbesstategraph_options& options)
27{
28 pbes p;
29 load_pbes(p, input_filename, input_format);
30
31 stategraph(p, options);
32
33 save_pbes(p, output_filename, output_format, false);
34 if (!p.is_well_typed())
35 {
36 mCRL2log(log::error) << "pbesstategraph error: not well typed!" << std::endl;
37 mCRL2log(log::error) << pp(p) << std::endl;
38 }
39}
40
41} // namespace pbes_system
42
43} // namespace mcrl2
44
45#endif // MCRL2_PBES_TOOLS_PBESSTATEGRAPH_H
parameterized boolean equation system
Definition pbes.h:58
bool is_well_typed() const
Checks if the PBES is well typed.
Definition pbes.h:267
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
void stategraph(pbes &p, const pbesstategraph_options &options)
Apply the stategraph algorithm.
Definition stategraph.h:26
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 pbesstategraph(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const pbesstategraph_options &options)
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
std::string pp(const fixpoint_symbol &x)
Definition pbes.cpp:37
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
IO routines for boolean equation systems.
add your file description here.