Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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 lts/detail/liblts_liblts_counter_example.h
      10             : /// \details This file contains a class in which counter examples 
      11             : ///          for divergence preserving failures refinement can 
      12             : ///          be constructed. A counterexample is a trace from 
      13             : ///          the root. The data structure to construct such a 
      14             : ///          trace is a tree pointing to the root where each branch
      15             : ///          is labelled with an action. By walking from a leaf to
      16             : ///          the root the desired counterexample can be constructed.
      17             : 
      18             : #ifndef _LIBLTS_COUNTER_EXAMPLE_H
      19             : #define _LIBLTS_COUNTER_EXAMPLE_H
      20             : 
      21             : #include "mcrl2/lts/lts_lts.h"
      22             : #include "mcrl2/lts/trace.h"
      23             : 
      24             : 
      25             : namespace mcrl2
      26             : {
      27             : namespace lts
      28             : {
      29             : 
      30             : namespace detail
      31             : {
      32             : 
      33             : 
      34             : /// \brief A simple class storing the index of a label and an index
      35             : //         to the counterexample three in the direction of the root.
      36             : class action_index_pair
      37             : {
      38             :   protected:
      39             :     std::size_t m_label_index;
      40             :     std::size_t m_previous_entry_index;
      41             : 
      42             :   public:
      43           0 :     action_index_pair(std::size_t label_index, std::size_t previous_entry_index)
      44           0 :      : m_label_index(label_index), 
      45           0 :        m_previous_entry_index(previous_entry_index)
      46           0 :     {}
      47             : 
      48           0 :     std::size_t label_index() const
      49             :     {
      50           0 :       return m_label_index;
      51             :     }
      52             : 
      53           0 :     std::size_t previous_entry_index() const
      54             :     {
      55           0 :       return m_previous_entry_index;
      56             :     }
      57             : };
      58             : 
      59             : /// \brief A class that can be used to store counterexample trees and 
      60             : //         from which a counterexample trace can be extracted.
      61             : class counter_example_constructor
      62             : {
      63             :   public:
      64             :     typedef std::size_t index_type;
      65             : 
      66             :   protected:
      67             :     // The backward three is stored in a deque. 
      68             :     // The root has entry std::size_t(-1).
      69             : 
      70             :     static const index_type m_root_index=-1;
      71             :     std::deque< action_index_pair > m_backward_tree;
      72             :     const std::string m_name;
      73             :     const std::string m_counter_example_file;
      74             :     const bool m_structured_output;
      75             :   
      76             :   public:
      77             :     /// \brief Constructor
      78             :     //  \param name The name of the model that the counter example is for
      79             :     //  \param counter_example_file The name of the file to save the counter example to
      80             :     //  \param structured_output Whether the counterexample should be printed to std:cout
      81             :     //  \detail If structured_output=true, the counter example is not saved to file.
      82             :     //          If counter_example_file="", the name of the counter example file name is derived from name (the parameter)
      83           0 :     counter_example_constructor(const std::string& name, const std::string& counter_example_file, bool structured_output)
      84           0 :      : m_name(name)
      85           0 :      , m_counter_example_file(counter_example_file)
      86           0 :      , m_structured_output(structured_output)
      87           0 :     {}
      88             : 
      89             :     /// \brief Return the index of the root.
      90           0 :     static index_type root_index() 
      91             :     {
      92           0 :       return m_root_index;
      93             :     }
      94             : 
      95             :     /// \brief This function stores a label to the counterexample tree.
      96             :     //  \param label_index The label index is the label as used in transitions.
      97             :     //  \param previous_entry The index of the counterexample trace to which
      98             :     //                        this action label must be attached.
      99             :     //  \ret It returns a new index which can be used to extend the counterexample.
     100           0 :     index_type add_transition(std::size_t label_index, index_type previous_entry)
     101             :     {
     102           0 :       m_backward_tree.emplace_back(label_index, previous_entry);
     103           0 :       return m_backward_tree.size()-1;
     104             :     }
     105             : 
     106             :     /* A trace to index is saved, followed by a list of actions in extra_actions. */
     107             :     template < class LTS_TYPE >
     108           0 :     void save_counter_example(index_type index, const LTS_TYPE& l, const std::vector<size_t>& extra_actions=std::vector<size_t>()) const
     109             :     {
     110             :       // We first store the label indices in reverse order in a stack.
     111           0 :       std::stack< index_type > reversed_label_indices;
     112           0 :       for(index_type current_index=index; 
     113           0 :           current_index!=m_root_index; 
     114           0 :           current_index=m_backward_tree[current_index].previous_entry_index())
     115             :       {
     116           0 :         reversed_label_indices.push(m_backward_tree[current_index].label_index());
     117             :       }
     118             : 
     119           0 :       trace result;
     120           0 :       while (!reversed_label_indices.empty())
     121             :       {
     122           0 :         result.add_action(mcrl2::lps::multi_action(mcrl2::process::action(
     123           0 :                                 mcrl2::process::action_label(
     124           0 :                                        core::identifier_string(mcrl2::lts::pp(l.action_label(reversed_label_indices.top()))),
     125           0 :                                        mcrl2::data::sort_expression_list()),
     126           0 :                                 mcrl2::data::data_expression_list())));
     127           0 :         reversed_label_indices.pop();
     128             :       }
     129             : 
     130             :       /* Add the actions in extra actions. */
     131           0 :       for(const size_t& a: extra_actions)
     132             :       {
     133           0 :         result.add_action(mcrl2::lps::multi_action(mcrl2::process::action(
     134           0 :                                 mcrl2::process::action_label(
     135           0 :                                        core::identifier_string(mcrl2::lts::pp(l.action_label(a))),
     136           0 :                                        mcrl2::data::sort_expression_list()),
     137           0 :                                 mcrl2::data::data_expression_list())));
     138             :       }
     139           0 :       if (m_structured_output)
     140             :       {
     141           0 :         std::cout << m_name << ": ";
     142           0 :         result.save("", mcrl2::lts::trace::tfLine);   // Write to stdout.
     143             :       }
     144             :       else
     145             :       {
     146           0 :         std::string filename = m_name + ".trc";
     147           0 :         if (!m_counter_example_file.empty())
     148             :         {
     149           0 :           filename = m_counter_example_file;
     150             :         }
     151           0 :         mCRL2log(log::verbose) << "Saved trace to file " + filename + "\n";
     152           0 :         result.save(filename);
     153           0 :       }
     154           0 :     }
     155             : 
     156             :     /// \brief This function indicates that this is not a dummy counterexample class and that a serious counterexample is required.
     157           0 :     bool is_dummy() const
     158             :     {
     159           0 :       return false;
     160             :     }
     161             : 
     162             :     /// \brief Returns whether this counter-example is printed in a machine-readable way to stdout
     163             :     /// If false is returned, the counter-example is written to a file.
     164           0 :     bool is_structured() const
     165             :     {
     166           0 :       return m_structured_output;
     167             :     }
     168             : };
     169             : 
     170             : 
     171             : /// \brief A class that can be used to construct counter examples if no
     172             : //         counter example is desired. Its index_type is empty.
     173             : class dummy_counter_example_constructor
     174             : {
     175             :   public:
     176             :     typedef dummy_counter_example_constructor index_type;  // This yields an empty type.
     177             : 
     178          48 :     static index_type root_index()
     179             :     {
     180          48 :       return dummy_counter_example_constructor();  // This returns nothing. 
     181             :     }
     182             : 
     183         188 :     index_type add_transition(std::size_t /* label_index*/, index_type /* previous_entry*/)
     184             :     {
     185             :       // This dummy counter example generator intentionally does nothing.
     186         188 :       return *this;
     187             :     }
     188             :  
     189             :     template < class LTS_TYPE >
     190          21 :     void save_counter_example(index_type /* index */, const LTS_TYPE& /*l*/, const std::vector<size_t>& /* extra_actions */ =std::vector<size_t>()) const
     191             :     {
     192             :       // This dummy counter example generator intentionally does not save anything.
     193          21 :     }
     194             : 
     195             :     /// \brief This function indicates that this is a dummy counterexample class and that no counterexample is required.
     196         215 :     bool is_dummy() const
     197             :     {
     198         215 :       return true;
     199             :     }
     200             : 
     201             :     /// \brief Returns whether this counter-example is printed in a machine-readable way to stdout
     202             :     /// If false is returned, the counter-example is written to a file.
     203         103 :     bool is_structured() const
     204             :     {
     205         103 :       return false;
     206             :     }
     207             : };
     208             : 
     209             : } // namespace detail
     210             : } // namespace lts
     211             : } // namespace mcrl2
     212             : 
     213             : #endif // _LIBLTS_COUNTER_EXAMPLE_H