Line data    Source code

       1             : // Author(s): Muck van Weerdenburg
       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             : 
       9             : 
      10             : #ifndef MCRL2_LPS_EXPLORATION_STRATEGY_H
      11             : #define MCRL2_LPS_EXPLORATION_STRATEGY_H
      12             : 
      13             : #include <string>
      14             : #include "mcrl2/utilities/exception.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : namespace lps
      19             : {
      20             : 
      21             : enum exploration_strategy { es_none,
      22             :                             es_breadth,
      23             :                             es_depth,
      24             :                             es_random,
      25             :                             es_value_prioritized,
      26             :                             es_value_random_prioritized,
      27             :                             es_highway
      28             :                           };
      29             : 
      30             : inline
      31             : exploration_strategy parse_exploration_strategy(const std::string& s)
      32             : {
      33             :   if (s=="b" || s=="breadth")
      34             :   {
      35             :     return es_breadth;
      36             :   }
      37             :   if (s=="d" || s=="depth")
      38             :   {
      39             :     return es_depth;
      40             :   }
      41             :   if (s=="r" || s=="random")
      42             :   {
      43             :     return es_random;
      44             :   }
      45             :   if (s=="p" || s=="prioritized")
      46             :   {
      47             :     return es_value_prioritized;
      48             :   }
      49             :   if (s=="q" || s=="rprioritized")
      50             :   {
      51             :     return es_value_random_prioritized;
      52             :   }
      53             :   if (s=="h" || s == "highway")
      54             :   {
      55             :     return es_highway;
      56             :   }
      57             :   return es_none;
      58             : }
      59             : 
      60             : inline
      61         174 : std::string print_exploration_strategy(const exploration_strategy es)
      62             : {
      63         174 :   switch (es)
      64             :   {
      65          87 :     case es_breadth:
      66          87 :       return "breadth";
      67          87 :     case es_depth:
      68          87 :       return "depth";
      69           0 :     case es_random:
      70           0 :       return "random";
      71           0 :     case es_value_prioritized:
      72           0 :       return "prioritized";
      73           0 :     case es_value_random_prioritized:
      74           0 :       return "rprioritized";
      75           0 :     case es_highway:
      76           0 :       return "highway";
      77           0 :     default:
      78           0 :       throw mcrl2::runtime_error("unknown exploration strategy");
      79             :   }
      80             : }
      81             : 
      82             : inline
      83             : std::istream& operator>>(std::istream& is, exploration_strategy& strat)
      84             : {
      85             :   try
      86             :   {
      87             :     std::string s;
      88             :     is >> s;
      89             :     strat = parse_exploration_strategy(s);
      90             :   }
      91             :   catch (mcrl2::runtime_error&)
      92             :   {
      93             :     is.setstate(std::ios_base::failbit);
      94             :   }
      95             :   return is;
      96             : }
      97             : 
      98             : inline
      99         174 : std::ostream& operator<<(std::ostream& os, const exploration_strategy strat)
     100             : {
     101         174 :   os << print_exploration_strategy(strat);
     102         174 :   return os;
     103             : }
     104             : 
     105             : inline std::string description(const exploration_strategy strat)
     106             : {
     107             :   switch (strat)
     108             :   {
     109             :     case es_breadth:
     110             :       return "breadth-first search";
     111             :     case es_depth:
     112             :       return "depth-first search";
     113             :     case es_random:
     114             :       return "random simulation. Out of all next states one is chosen at random independently of whether this state has already been observed. Consequently, random simulation only terminates when a deadlocked state is encountered.";
     115             :     case es_value_prioritized:
     116             :       return "prioritize single actions on its first argument being of sort Nat where only those actions with the lowest value for this parameter are selected. E.g. if there are actions a(3) and b(4), a(3) remains and b(4) is skipped. Actions without a first parameter of sort Nat and multactions with more than one action are always chosen (option is experimental)";
     117             :     case es_value_random_prioritized:
     118             :       return "prioritize actions on its first argument being of sort Nat (see option --prioritized), and randomly select one of these to obtain a prioritized random simulation (option is experimental)";
     119             :     case es_highway:
     120             :       return "highway search. Only part of the state space is explored, by restricting the size of the todo list. N.B. The implementation deviates slightly from the published version.";
     121             :     default:
     122             :       throw mcrl2::runtime_error("unknown exploration_strategy");
     123             :   }
     124             : }
     125             : 
     126             : } // namespace lps
     127             : } // namespace mcrl2
     128             : 
     129             : #endif // MCRL2_LPS_EXPLORATION_STRATEGY_H