mCRL2
Loading...
Searching...
No Matches
pbessolve_options.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_PBESSOLVE_OPTIONS_H
13#define MCRL2_PBES_PBESSOLVE_OPTIONS_H
14
15#include <iomanip>
19
20namespace mcrl2 {
21
22namespace pbes_system {
23
25{
29 bool prune_todo_list = false;
31 int optimization = 0;
32
33 // if true, apply optimization 4 and 5 at every iteration
34 bool aggressive = false;
35
36 // for doing a consistency check on the computed strategy
37 bool check_strategy = false;
38
40
41 std::size_t number_of_threads = 1;
42};
43
44inline
45std::ostream& operator<<(std::ostream& out, const pbessolve_options& options)
46{
47 out << "rewrite-strategy = " << options.rewrite_strategy << std::endl;
48 out << "replace-constants-by-variables = " << std::boolalpha << options.replace_constants_by_variables << std::endl;
49 out << "remove-unused-rewrite-rules = " << std::boolalpha << options.remove_unused_rewrite_rules << std::endl;
50 out << "reset-todo = " << std::boolalpha << options.prune_todo_list << std::endl;
51 out << "search-strategy = " << options.exploration_strategy << std::endl;
52 out << "optimization = " << options.optimization << std::endl;
53 out << "aggressive = " << std::boolalpha << options.aggressive << std::endl;
54 out << "check-strategy = " << std::boolalpha << options.check_strategy << std::endl;
55 out << "prune-todo-alternative = " << std::boolalpha << options.prune_todo_alternative << std::endl;
56 out << "threads = " << options.number_of_threads << std::endl;
57 return out;
58}
59
60} // namespace pbes_system
61
62} // namespace mcrl2
63
64#endif // MCRL2_PBES_PBESSOLVE_OPTIONS_H
add your file description here.
rewrite_strategy
The strategy of the rewriter.
search_strategy
Search strategy when generating a BES from a PBES.
std::ostream & operator<<(std::ostream &os, const absinthe_strategy strategy)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Search strategy when generating a BES from a PBES.