12#ifndef MCRL2_PBES_SEARCH_STRATEGY_H
13#define MCRL2_PBES_SEARCH_STRATEGY_H
67 is.setstate(std::ios_base::failbit);
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. ";
Standard exception class for reporting runtime errors.
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...