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

          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/trace/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           0 : 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 bool m_structured_output;
      74             :   
      75             :   public:
      76           0 :     counter_example_constructor(const std::string& name, bool structured_output)
      77           0 :      : m_name(name)
      78           0 :      , m_structured_output(structured_output)
      79           0 :     {}
      80             : 
      81             :     /// \brief Return the index of the root.
      82           0 :     static index_type root_index() 
      83             :     {
      84           0 :       return m_root_index;
      85             :     }
      86             : 
      87             :     /// \brief This function stores a label to the counterexample tree.
      88             :     //  \param label_index The label index is the label as used in transitions.
      89             :     //  \param previous_entry The index of the counterexample trace to which
      90             :     //                        this action label must be attached.
      91             :     //  \ret It returns a new index which can be used to extend the counterexample.
      92           0 :     index_type add_transition(std::size_t label_index, index_type previous_entry)
      93             :     {
      94           0 :       m_backward_tree.emplace_back(label_index, previous_entry);
      95           0 :       return m_backward_tree.size()-1;
      96             :     }
      97             : 
      98             :     /* A trace to index is saved, followed by a list of actions in extra_actions. */
      99             :     template < class LTS_TYPE >
     100           0 :     void save_counter_example(index_type index, const LTS_TYPE& l, const std::vector<size_t>& extra_actions=std::vector<size_t>()) const
     101             :     {
     102             :       // We first store the label indices in reverse order in a stack.
     103           0 :       std::stack< index_type > reversed_label_indices;
     104           0 :       for(index_type current_index=index; 
     105           0 :           current_index!=m_root_index; 
     106           0 :           current_index=m_backward_tree[current_index].previous_entry_index())
     107             :       {
     108           0 :         reversed_label_indices.push(m_backward_tree[current_index].label_index());
     109             :       }
     110             : 
     111           0 :       trace::Trace result;
     112           0 :       while (!reversed_label_indices.empty())
     113             :       {
     114           0 :         result.addAction(mcrl2::lps::multi_action(mcrl2::process::action(
     115             :                                 mcrl2::process::action_label(
     116           0 :                                        core::identifier_string(mcrl2::lts::pp(l.action_label(reversed_label_indices.top()))),
     117             :                                        mcrl2::data::sort_expression_list()),
     118             :                                 mcrl2::data::data_expression_list())));
     119           0 :         reversed_label_indices.pop();
     120             :       }
     121             : 
     122             :       /* Add the actions in extra actions. */
     123           0 :       for(const size_t& a: extra_actions)
     124             :       {
     125           0 :         result.addAction(mcrl2::lps::multi_action(mcrl2::process::action(
     126             :                                 mcrl2::process::action_label(
     127             :                                        core::identifier_string(mcrl2::lts::pp(l.action_label(a))),
     128             :                                        mcrl2::data::sort_expression_list()),
     129             :                                 mcrl2::data::data_expression_list())));
     130             :       }
     131           0 :       if (m_structured_output)
     132             :       {
     133           0 :         std::cout << m_name << ": ";
     134           0 :         result.save(std::cout, mcrl2::trace::tfLine);
     135             :       }
     136             :       else
     137             :       {
     138           0 :         std::string filename = m_name + ".trc";
     139           0 :         mCRL2log(log::verbose) << "Saved trace to file " + filename + "\n";
     140           0 :         result.save(filename);
     141             :       }
     142           0 :     }
     143             : 
     144             :     /// \brief This function indicates that this is not a dummy counterexample class and that a serious counterexample is required.
     145           0 :     bool is_dummy() const
     146             :     {
     147           0 :       return false;
     148             :     }
     149             : 
     150             :     /// \brief Returns whether this counter-example is printed in a machine-readable way to stdout
     151             :     /// If false is returned, the counter-example is written to a file.
     152           0 :     bool is_structured() const
     153             :     {
     154           0 :       return m_structured_output;
     155             :     }
     156             : };
     157             : 
     158             : 
     159             : /// \brief A class that can be used to construct counter examples if no
     160             : //         counter example is desired. Its index_type is empty.
     161             : class dummy_counter_example_constructor
     162             : {
     163             :   public:
     164             :     typedef dummy_counter_example_constructor index_type;  // This yields an empty type.
     165             : 
     166          48 :     static index_type root_index()
     167             :     {
     168          48 :       return dummy_counter_example_constructor();  // This returns nothing. 
     169             :     }
     170             : 
     171         188 :     index_type add_transition(std::size_t /* label_index*/, index_type /* previous_entry*/)
     172             :     {
     173             :       // This dummy counter example generator intentionally does nothing.
     174         188 :       return *this;
     175             :     }
     176             :  
     177             :     template < class LTS_TYPE >
     178          21 :     void save_counter_example(index_type /* index */, const LTS_TYPE& /*l*/, const std::vector<size_t>& /* extra_actions */ =std::vector<size_t>()) const
     179             :     {
     180             :       // This dummy counter example generator intentionally does not save anything.
     181          21 :     }
     182             : 
     183             :     /// \brief This function indicates that this is a dummy counterexample class and that no counterexample is required.
     184         215 :     bool is_dummy() const
     185             :     {
     186         215 :       return true;
     187             :     }
     188             : 
     189             :     /// \brief Returns whether this counter-example is printed in a machine-readable way to stdout
     190             :     /// If false is returned, the counter-example is written to a file.
     191         103 :     bool is_structured() const
     192             :     {
     193         103 :       return false;
     194             :     }
     195             : };
     196             : 
     197             : } // namespace detail
     198             : } // namespace lts
     199             : } // namespace mcrl2
     200             : 
     201             : #endif // _LIBLTS_COUNTER_EXAMPLE_H

Generated by: LCOV version 1.13