LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - lts_generation_options.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 5 5 100.0 %
Date: 2020-07-11 00:44:39 Functions: 3 3 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren
       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             : /// \file mcrl2/lts/detail/lts_generation_options.h
      10             : /// \brief Options used during state space generation.
      11             : 
      12             : #ifndef MCRL2_LTS_DETAIL_LTS_GENERATION_OPTIONS_H
      13             : #define MCRL2_LTS_DETAIL_LTS_GENERATION_OPTIONS_H
      14             : 
      15             : #include <climits>
      16             : #include "mcrl2/lts/lts_io.h"
      17             : #include "mcrl2/lps/exploration_strategy.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : namespace lts
      22             : {
      23             : 
      24             : 
      25         561 : class lts_generation_options
      26             : {
      27             :   private:
      28             :     static const std::size_t default_max_states=ULONG_MAX;
      29             :     static const std::size_t default_bithashsize=209715200ULL; // ~25 MB
      30             :     static const std::size_t default_init_tsize=10000UL;
      31             : 
      32             :   public:
      33             :     static const std::size_t default_max_traces=ULONG_MAX;
      34             : 
      35             :     mcrl2::lps::stochastic_specification specification;
      36             :     bool usedummies;
      37             :     bool removeunused;
      38             : 
      39             :     mcrl2::data::rewriter::strategy strat;
      40             :     lps::exploration_strategy expl_strat;
      41             :     std::string priority_action;
      42             :     std::size_t todo_max;
      43             :     std::size_t max_states;
      44             :     std::size_t initial_table_size;
      45             :     bool suppress_progress_messages;
      46             : 
      47             :     bool bithashing;
      48             :     std::size_t bithashsize;
      49             : 
      50             :     mcrl2::lts::lts_type outformat;
      51             :     bool outinfo;
      52             :     std::string lts;
      53             : 
      54             :     bool trace;
      55             :     std::size_t max_traces;
      56             :     std::string trace_prefix;
      57             :     bool save_error_trace;
      58             :     bool detect_deadlock;
      59             :     bool detect_nondeterminism;
      60             :     bool detect_divergence;
      61             :     bool detect_action;
      62             :     std::set < mcrl2::core::identifier_string > trace_actions;
      63             :     std::set < std::string > trace_multiaction_strings;
      64             :     std::set < mcrl2::lps::multi_action > trace_multiactions;
      65             : 
      66             :     bool use_enumeration_caching;
      67             :     bool use_summand_pruning;
      68             :     std::set< mcrl2::core::identifier_string > actions_internal_for_divergencies;
      69             : 
      70             :     /// \brief Constructor
      71         374 :     lts_generation_options() :
      72             :       usedummies(true),
      73             :       removeunused(true),
      74             :       strat(mcrl2::data::jitty),
      75             :       expl_strat(lps::es_breadth),
      76         374 :       todo_max((std::numeric_limits< std::size_t >::max)()),
      77             :       max_states(default_max_states),
      78             :       initial_table_size(default_init_tsize),
      79             :       suppress_progress_messages(false),
      80             :       bithashing(false),
      81             :       bithashsize(default_bithashsize),
      82             :       outformat(mcrl2::lts::lts_none),
      83             :       outinfo(true),
      84             :       trace(false),
      85             :       max_traces(default_max_traces),
      86             :       save_error_trace(false),
      87             :       detect_deadlock(false),
      88             :       detect_nondeterminism(false),
      89             :       detect_divergence(false),
      90             :       detect_action(false),
      91             :       use_enumeration_caching(false),
      92         748 :       use_summand_pruning(false)
      93         374 :     {}
      94             : 
      95             :     /// \brief Copy assignment operator.
      96             :     lts_generation_options& operator=(const lts_generation_options& )=default;
      97             : 
      98             :     void validate_actions()
      99             :     {
     100             :       for (const std::string& s: trace_multiaction_strings)
     101             :       {
     102             :         try
     103             :         {
     104             :           trace_multiactions.insert(mcrl2::lps::parse_multi_action(s, specification.action_labels(), specification.data()));
     105             :         }
     106             :         catch (mcrl2::runtime_error& e)
     107             :         {
     108             :           throw mcrl2::runtime_error(std::string("Multi-action ") + s + " does not exist: " + e.what());
     109             :         }
     110             :         mCRL2log(log::verbose) << "Checking for action \"" << s << "\"\n";
     111             :       }
     112             :       if (detect_action)
     113             :       {
     114             :         for (const mcrl2::core::identifier_string& ta: trace_actions)
     115             :         {
     116             :           bool found = (std::string(ta) == "tau");
     117             :           for(const process::action_label& al: specification.action_labels())
     118             :           {
     119             :             if (al.name() == ta)
     120             :             {
     121             :               found=true;
     122             :               break;
     123             :             }
     124             :           }
     125             :           if (!found)
     126             :           {
     127             :             throw mcrl2::runtime_error(std::string("Action label ") + core::pp(ta) + " is not declared.");
     128             :           }
     129             :           else
     130             :           {
     131             :             mCRL2log(log::verbose) << "Checking for action " << ta << "\n";
     132             :           }
     133             :         }
     134             :       }
     135             :       for (const mcrl2::core::identifier_string& ta: actions_internal_for_divergencies)
     136             :       {
     137             :         mcrl2::process::action_label_list::iterator it = specification.action_labels().begin();
     138             :         bool found = (std::string(ta) == "tau");
     139             :         while (!found && it != specification.action_labels().end())
     140             :         {
     141             :           found = (it++->name() == ta);
     142             :         }
     143             :         if (!found)
     144             :         {
     145             :           throw mcrl2::runtime_error(std::string("Action label ") + core::pp(ta) + " is not declared.");
     146             :         }
     147             :       }
     148             :     }
     149             : 
     150             : };
     151             : 
     152             : } // namespace lts
     153             : } // namespace mcrl2
     154             : 
     155             : #endif // MCRL2_LTS_DETAIL_LTS_GENERATION_OPTIONS_H

Generated by: LCOV version 1.13