Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/lps/explorer_options.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_EXPLORER_OPTIONS_H
      13             : #define MCRL2_LPS_EXPLORER_OPTIONS_H
      14             : 
      15             : #include <iomanip>
      16             : #include "mcrl2/core/detail/print_utility.h"
      17             : #include "mcrl2/data/rewrite_strategy.h"
      18             : #include "mcrl2/lps/multi_action.h"
      19             : #include "mcrl2/lps/exploration_strategy.h"
      20             : 
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace lps {
      25             : 
      26             : struct explorer_options
      27             : {
      28             :   data::rewrite_strategy rewrite_strategy = data::jitty;
      29             :   exploration_strategy search_strategy;
      30             :   bool one_point_rule_rewrite = false;
      31             :   bool replace_constants_by_variables = false;
      32             :   bool remove_unused_rewrite_rules = false;
      33             :   bool cached = false;
      34             :   bool global_cache = false;
      35             :   bool confluence = false;
      36             :   bool detect_deadlock = false;
      37             :   bool detect_nondeterminism = false;
      38             :   bool detect_divergence = false;
      39             :   bool detect_action = false;
      40             :   bool check_probabilities = false;
      41             :   bool save_error_trace = false;
      42             :   bool generate_traces = false;
      43             :   bool suppress_progress_messages = false;
      44             :   bool save_at_end = false;
      45             :   bool dfs_recursive = false;
      46             :   bool discard_lts_state_labels = false;
      47             :   bool rewrite_actions = true;    // If false, this option prevents rewriting actions.
      48             :                                   // Rewriting actions is only needed if they occur in the
      49             :                                   // generated lts, or in traces. 
      50             :   std::size_t max_states = std::numeric_limits<std::size_t>::max();
      51             :   std::size_t max_traces = 0;
      52             :   std::size_t highway_todo_max = std::numeric_limits<std::size_t>::max();
      53             :   std::size_t number_of_threads = 1;
      54             :   std::string trace_prefix;
      55             :   std::set<core::identifier_string> trace_actions;
      56             :   std::set<lps::multi_action> trace_multiactions;
      57             :   std::set<core::identifier_string> actions_internal_for_divergencies;
      58             :   std::string confluence_action = "ctau";
      59             : 
      60             :   // Constructor.
      61         192 :   explorer_options()
      62         192 :   {}
      63             : 
      64             :   // Constructor.
      65          10 :   explorer_options(data::rewrite_strategy rewr_strat)
      66          10 :    : rewrite_strategy(rewr_strat)
      67          10 :   {}
      68             : 
      69             :   //
      70         202 :   explorer_options(const explorer_options& other) = default;
      71             :   explorer_options& operator=(const explorer_options& other) = default;
      72             : };
      73             : 
      74             : inline
      75             : std::ostream& operator<<(std::ostream& out, const explorer_options& options)
      76             : {
      77             :   out << "rewrite-strategy = " << options.rewrite_strategy << std::endl;
      78             :   out << "search-strategy = " << options.search_strategy << std::endl;
      79             :   out << "cached = " << std::boolalpha << options.cached << std::endl;
      80             :   out << "global-cache = " << std::boolalpha << options.global_cache << std::endl;
      81             :   out << "confluence = " << std::boolalpha << options.confluence << std::endl;
      82             :   out << "confluence-action = " << options.confluence << std::endl;
      83             :   out << "one-point-rule-rewrite = " << std::boolalpha << options.one_point_rule_rewrite << std::endl;
      84             :   out << "replace-constants-by-variables = " << std::boolalpha << options.replace_constants_by_variables << std::endl;
      85             :   out << "remove-unused-rewrite-rules = " << std::boolalpha << options.remove_unused_rewrite_rules << std::endl;
      86             :   out << "check-probabilities = " << std::boolalpha << options.check_probabilities << std::endl;
      87             :   out << "detect-deadlock = " << std::boolalpha << options.detect_deadlock << std::endl;
      88             :   out << "detect-nondeterminism = " << std::boolalpha << options.detect_nondeterminism << std::endl;
      89             :   out << "detect-divergence = " << std::boolalpha << options.detect_divergence << std::endl;
      90             :   out << "detect-action = " << std::boolalpha << options.detect_action << std::endl;
      91             :   out << "discard-lts-state-labels = " << std::boolalpha << options.discard_lts_state_labels << std::endl;
      92             :   out << "save-error-trace = " << std::boolalpha << options.save_error_trace << std::endl;
      93             :   out << "generate-traces = " << std::boolalpha << options.generate_traces << std::endl;
      94             :   out << "suppress-progress-messages = " << std::boolalpha << options.suppress_progress_messages << std::endl;
      95             :   out << "save-aut-at-end = " << std::boolalpha << options.save_at_end << std::endl;
      96             :   out << "dfs-recursive = " << std::boolalpha << options.dfs_recursive << std::endl;
      97             :   out << "max-states = " << options.max_states << std::endl;
      98             :   out << "max-traces = " << options.max_traces << std::endl;
      99             :   out << "todo-max = " << options.highway_todo_max << std::endl;
     100             :   out << "threads = " << options.number_of_threads << std::endl;
     101             :   out << "trace-prefix = " << options.trace_prefix << std::endl;
     102             :   out << "trace-actions = " << core::detail::print_set(options.trace_actions) << std::endl;
     103             :   out << "trace-multiactions = " << core::detail::print_set(options.trace_multiactions) << std::endl;
     104             :   out << "actions-internal-for-divergencies = " << core::detail::print_set(options.actions_internal_for_divergencies) << std::endl;
     105             :   return out;
     106             : }
     107             : 
     108             : } // namespace lps
     109             : 
     110             : } // namespace mcrl2
     111             : 
     112             : #endif // MCRL2_LPS_EXPLORER_OPTIONS_H