mCRL2
Loading...
Searching...
No Matches
search_strategy.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote, Xiao Qi
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_SEARCH_STRATEGY_H
13#define MCRL2_PBES_SEARCH_STRATEGY_H
14
16#include <string>
17
18namespace mcrl2
19{
20
21namespace pbes_system
22{
23
26{
27 breadth_first, // Generate the rhs of the last generated BES variable last.
28 depth_first, // Generate the rhs of the last generated BES variable first.
31};
32
33inline
35{
36 if (s == "breadth-first") return breadth_first;
37 else if (s == "b") return breadth_first_short;
38 else if (s == "depth-first") return depth_first;
39 else if (s == "d") return depth_first_short;
40 else throw mcrl2::runtime_error("unknown search strategy " + s);
41}
42
43inline
45{
46 switch(s)
47 {
48 case breadth_first: return "breadth-first";
49 case depth_first: return "depth-first";
50 case breadth_first_short: return "b";
51 case depth_first_short: return "d";
52 }
53 throw mcrl2::runtime_error("unknown search strategy");
54}
55
56inline
57std::istream& operator>>(std::istream& is, search_strategy& strategy)
58{
59 try
60 {
61 std::string s;
62 is >> s;
63 strategy = parse_search_strategy(s);
64 }
66 {
67 is.setstate(std::ios_base::failbit);
68 }
69 return is;
70}
71
72inline
73std::ostream& operator<<(std::ostream& os, const search_strategy s)
74{
75 os << print_search_strategy(s);
76 return os;
77}
78
79inline
80std::string description(const search_strategy s)
81{
82 switch(s)
83 {
84 case breadth_first: return "Compute the right hand side of the boolean variables"
85 " in a first come first served basis. This is comparable with a breadth-first search."
86 " This is good for generating counter examples. ";
87 case depth_first: return "Compute the right hand side of a boolean variables where "
88 " the last generated variable is investigated first. This corresponds to a depth-first "
89 " search. This can substantially outperform breadth-first search when the validity of a"
90 " formula is determined at a larger depth. ";
91 case breadth_first_short: return "Shorthand for breadth-first.";
92 case depth_first_short: return "Shorthand for depth-first.";
93 }
94 throw mcrl2::runtime_error("unknown search strategy");
95}
96
97} // namespace pbes_system
98
99} // namespace mcrl2
100
101#endif // MCRL2_PBES_SEARCH_STRATEGY_H
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
search_strategy parse_search_strategy(const std::string &s)
std::string description(const absinthe_strategy strategy)
Prints an absinthe strategy.
std::istream & operator>>(std::istream &is, absinthe_strategy &strategy)
std::string print_search_strategy(const search_strategy s)
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