mCRL2
Loading...
Searching...
No Matches
pbespp.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_PBESPP_H
13#define MCRL2_PBES_TOOLS_PBESPP_H
14
15#include "mcrl2/pbes/io.h"
17
18namespace mcrl2 {
19
20namespace pbes_system {
21
22void pbespp(const std::string& input_filename,
23 const std::string& output_filename,
24 const utilities::file_format& input_format,
26 bool use_pfnf_printer
27 )
28{
29 pbes p;
30 load_pbes(p, input_filename, input_format);
31
32 mCRL2log(log::verbose) << "printing PBES from "
33 << (input_filename.empty()?"standard input":input_filename)
34 << " to " << (output_filename.empty()?"standard output":output_filename)
35 << " in the " << core::pp_format_to_string(format) << " format" << std::endl;
36
37 if (output_filename.empty())
38 {
39 if (format == core::print_internal)
40 {
41 std::cout << pbes_to_aterm(p);
42 }
43 else if(use_pfnf_printer && detail::is_pfnf(p))
44 {
45 std::cout << pfnf_pp(p);
46 }
47 else
48 {
49 std::cout << pp(p);
50 }
51 }
52 else
53 {
54 std::ofstream out(output_filename.c_str());
55 if (out)
56 {
57 if (format == core::print_internal)
58 {
59 out << pbes_to_aterm(p);
60 }
61 else if(use_pfnf_printer && detail::is_pfnf(p))
62 {
63 out << pfnf_pp(p);
64 }
65 else
66 {
67 out << pp(p);
68 }
69 out.close();
70 }
71 else
72 {
73 throw mcrl2::runtime_error("could not open output file " + output_filename + " for writing");
74 }
75 }
76}
77
78} // namespace pbes_system
79
80} // namespace mcrl2
81
82#endif // MCRL2_PBES_TOOLS_PBESPP_H
parameterized boolean equation system
Definition pbes.h:58
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
print_format_type
print_format_type represents the available pretty print formats
std::string pp_format_to_string(const print_format_type pp_format)
Print string representation of pretty print format.
@ verbose
Definition logger.h:37
bool is_pfnf(const T &x)
Definition is_pfnf.h:188
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
std::string pfnf_pp(const T &x)
Returns a PFNF string representation of the object x.
Definition pfnf_print.h:147
void pbespp(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, core::print_format_type format, bool use_pfnf_printer)
Definition pbespp.h:22
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
Definition io.cpp:328
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.