Line data    Source code

       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #include "mcrl2/pg/PredecessorLiftingStrategy.h"
      11             : #include "mcrl2/pg/FocusListLiftingStrategy.h"
      12             : #include "mcrl2/pg/MaxMeasureLiftingStrategy.h"
      13             : #include "mcrl2/pg/OldMaxMeasureLiftingStrategy.h"
      14             : #include "mcrl2/pg/LinPredLiftingStrategy.h"
      15             : 
      16             : #include <cstdlib>
      17             : 
      18             : /// \brief Convert string to lowercase.
      19             : /// \param in An input string
      20             : /// \return The text in \a in in lowercase
      21             : static inline
      22           0 : std::string tolower(std::string s)
      23             : {
      24             :   // dirty trick in the function to disambiguate between two tolower functions!
      25           0 :   std::transform(s.begin(), s.end(), s.begin(), (int(*)(int)) tolower);
      26           0 :   return s;
      27             : }
      28             : 
      29           0 : LiftingStrategyFactory::~LiftingStrategyFactory()
      30             : {
      31           0 : }
      32             : 
      33           0 : const char *LiftingStrategyFactory::usage()
      34             : {
      35             :     return
      36             : "linear:alternate\n"
      37             : "   Use a linear lifting strategy (aka swiping).\n"
      38             : "   - alternate: if 1, switches direction between forward and backward \n"
      39             : "     whenever the end of the list is reached (default: 0)\n"
      40             : "\n"
      41             : "predecessor:stack\n"
      42             : "   Use a predecessor lifting strategy (aka worklist).\n"
      43             : "   - stack: if 1, removes elements from the end of the queue instead \n"
      44             : "            of the beginning (default: 0)\n"
      45             : "\n"
      46             : "focuslist:alternate:max_size:lift_ratio\n"
      47             : "   Use swiping + focus list lifting strategy.\n"
      48             : "   - alternate: see 'linear' (default: 0)\n"
      49             : "   - max_size: the maximum size of the focus list, either as an absolute size\n"
      50             : "     greater than 1, or as a ratio (between 0 and 1) of the total number of\n"
      51             : "     vertices (default: 0.1)\n"
      52             : "   - lift_ratio: the maximum number of lifting attempts performed on the\n"
      53             : "     focus list before switching back to swiping, as a ratio of the maximum\n"
      54             : "     focus list size (default: 10.0)\n"
      55             : "\n"
      56             : "maxmeasure:order\n"
      57             : "   Maximum measure propagation; a variant of the predecessor lifting strategy\n"
      58             : "   that prefers to lift vertices with higher progress measures.\n"
      59             : "   - order: tie-breaking lifting order: 0 (queue-like), 1 (stack-like)\n"
      60             : "            or 2 (heap order) (default: 2)\n"
      61             : "\n"
      62             : "maxstep:order\n"
      63             : "   Maximum step variant of maximum measure propagation.\n"
      64             : "   - order: see 'maxmeasure'\n"
      65             : "\n"
      66             : "minmeasure:order\n"
      67             : "   Minimum measure propagation.\n"
      68             : "   - order: see 'maxmeasure'\n"
      69             : "\n"
      70             : "oldmaxmeasure\n"
      71             : "   Old implementation of max. measure lifting strategy.\n"
      72             : "   Included for regression testing purposes only.\n"
      73             : "\n"
      74             : "linpred\n"
      75           0 : "   Obsolete (roughly equivalent to predecessor:0:0).\n";
      76             : }
      77             : 
      78             : LiftingStrategyFactory *
      79           0 :     LiftingStrategyFactory::create(const std::string &description)
      80             : {
      81           0 :     if (description.empty()) return NULL;
      82             : 
      83             :     // Split into parts, separated by semicolon characters
      84           0 :     std::vector<std::string> parts;
      85             :     std::string::size_type i, j;
      86           0 :     for (i = 0; (j = description.find(':', i)) != std::string::npos; i = j + 1)
      87             :     {
      88           0 :         parts.push_back(std::string(description, i, j - i));
      89             :     }
      90           0 :     parts.push_back(std::string(description, i, j));
      91             : 
      92           0 :     std::string case_ = tolower(parts[0]);
      93           0 :     if ( case_ == "linear" || case_ == "lin" )
      94             :     {
      95           0 :         bool alternate = parts.size() > 1 && 0 != atoi(parts[1].c_str());
      96           0 :         return new LinearLiftingStrategyFactory(alternate);
      97             :     }
      98           0 :     else if ( case_ == "predecessor" || case_ == "pred" )
      99             :     {
     100           0 :         bool stack    = parts.size() > 1 && 0 != atoi(parts[1].c_str());
     101           0 :         return new PredecessorLiftingStrategyFactory(stack);
     102             :     }
     103           0 :     else if ( case_ == "focuslist" || case_ == "focus" )
     104             :     {
     105           0 :         bool alternate    = parts.size() > 1 && 0 != atoi(parts[1].c_str());
     106           0 :         double max_size   = (parts.size() > 2 ? atof(parts[2].c_str()) : 0);
     107           0 :         double lift_ratio = (parts.size() > 3 ? atof(parts[3].c_str()) : 0);
     108             :         return new FocusListLiftingStrategyFactory(
     109           0 :             alternate, max_size, lift_ratio );
     110             :     }
     111           0 :     else if (case_ == "maxmeasure")
     112             :     {
     113           0 :         int order = (parts.size() > 1 ? atoi(parts[1].c_str()) : 2);
     114             :         return new MaxMeasureLiftingStrategyFactory(
     115             :             (MaxMeasureLiftingStrategy2::Order)order,
     116           0 :             MaxMeasureLiftingStrategy2::MAX_VALUE);
     117             :     }
     118           0 :     else if (case_ == "maxstep")
     119             :     {
     120           0 :         int order = (parts.size() > 1 ? atoi(parts[1].c_str()) : 2);
     121             :         return new MaxMeasureLiftingStrategyFactory(
     122             :             (MaxMeasureLiftingStrategy2::Order)order, 
     123           0 :             MaxMeasureLiftingStrategy2::MAX_STEP );
     124             :     }
     125           0 :     else if (case_ == "minmeasure")
     126             :     {
     127           0 :         int order = (parts.size() > 1 ? atoi(parts[1].c_str()) : 2);
     128             :         return new MaxMeasureLiftingStrategyFactory(
     129             :             (MaxMeasureLiftingStrategy2::Order)order, 
     130           0 :             MaxMeasureLiftingStrategy2::MIN_VALUE );
     131             :     }
     132           0 :     else if (case_ == "oldmaxmeasure")
     133             :     {
     134           0 :         return new OldMaxMeasureLiftingStrategyFactory();
     135             :     }
     136           0 :     else if (case_ == "linpred")
     137             :     {
     138           0 :         return new LinPredLiftingStrategyFactory();
     139             :     }
     140             :     else
     141             :     {
     142             :         // No suitable strategy found
     143           0 :         return nullptr;
     144             :     }
     145           0 : }