LCOV - code coverage report
Current view: top level - lps/test - symbolic_reachability_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 52 70 74.3 %
Date: 2020-07-11 00:44:39 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen van der Wulp
       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 symbolic_reachability_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #include <boost/test/minimal.hpp>
      13             : 
      14             : #include "mcrl2/lps/find.h"
      15             : #include "mcrl2/lps/io.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : #include "mcrl2/lps/next_state_generator.h"
      18             : 
      19             : using namespace mcrl2;
      20             : 
      21           1 : const std::string case_no_influenced_parameters(
      22             :   "act a;\n\n"
      23             :   "proc X(i: Nat) = a.X(i);\n\n"
      24             :   "init X(0);\n");
      25             : 
      26           1 : const std::string case_influenced_condition(
      27             :   "act a;\n\n"
      28             :   "proc X(i: Nat) = (i < 4) -> a.X(i) <> delta;\n\n"
      29             :   "init X(0);\n");
      30             : 
      31           1 : const std::string case_influenced_next(
      32             :   "act a;\n\n"
      33             :   "proc X(i: Nat, j : Nat) = a.X(j, i);\n\n"
      34             :   "init X(0, 0);\n");
      35             : 
      36           1 : const std::string case_influenced_action(
      37             :   "act a : Nat;\n\n"
      38             :   "proc X(i: Nat) = a(i + 1).X(i);\n\n"
      39             :   "init X(0);\n");
      40             : 
      41           1 : const std::string case_influenced_time(
      42             :   "act a;\n\n"
      43             :   "proc X(i: Nat) = a@(i + 1).X(i);\n\n"
      44             :   "init X(0);\n");
      45             : 
      46           1 : const std::string case_two_parameters(
      47             :   "act a : Nat;\n\n"
      48             :   "proc X(i: Nat, j : Nat) = (j < 4) -> a(i).X(i, j + 1) <> delta;\n\n"
      49             :   "init X(0, 1);\n");
      50             : 
      51           1 : const std::string case_summands(
      52             :   "act a: Nat;\n\n"
      53             :   "proc X(i: Nat, j : Nat) = a(j + 1).X(i, j) + a(i + 1).X(i, j);\n\n"
      54             :   "init X(0, 1);\n");
      55             : 
      56           1 : const std::string case_last(
      57             :   "act a: Nat;\n\n"
      58             :   "sort D = struct d1 | d2;\n"
      59             :   "proc X(id : Nat, n : Nat, dd:D) = sum d:D. a(id).X(id,(n + 1) mod 10, d);\n\n"
      60             :   "init allow({a},X(1,0,d1) || X(2,0,d1));\n");
      61             : 
      62           8 : class group_information
      63             : {
      64             : 
      65             :   private:
      66             :     mcrl2::lps::stochastic_specification const& m_model;
      67             :     std::vector< std::vector< std::size_t > > m_group_indices;
      68             : 
      69             :   private:
      70             : 
      71             :     template <typename SummandVector>
      72          16 :     void gather_summands(const SummandVector& summands, const data::variable_list& parameter_list, const std::set<data::variable>& parameter_set, std::size_t& summand_index)
      73             :     {
      74          26 :       for (typename SummandVector::const_iterator i = summands.begin(); i != summands.end(); ++i)
      75             :       {
      76          20 :         std::set<data::variable> used_variables = lps::find_free_variables(*i);
      77          20 :         std::set<data::variable> used_parameters;
      78          10 :         std::set_intersection(used_variables.begin(), used_variables.end(), parameter_set.begin(), parameter_set.end(), std::inserter(used_parameters, used_parameters.begin()));
      79             : 
      80          10 :         std::size_t j_index = 0;
      81          16 :         for (const auto & j : parameter_list)
      82             :         {
      83           6 :           if (used_parameters.find(j) != used_parameters.end())
      84             :           {
      85           3 :             m_group_indices[summand_index].push_back(j_index);
      86             :           }
      87           6 :           j_index++;
      88             :         }
      89          10 :         summand_index++;
      90             :       }
      91          16 :     }
      92             : 
      93           8 :     void gather(lps::stochastic_specification const& l)
      94             :     {
      95          16 :       lps::stochastic_linear_process specification(l.process());
      96             : 
      97           8 :       std::size_t size = specification.action_summands().size() + specification.deadlock_summands().size();
      98           8 :       m_group_indices.resize(size);
      99             : 
     100          16 :       std::set<data::variable> parameter_set = data::find_all_variables(specification.process_parameters());
     101           8 :       std::size_t summand_index = 0;
     102           8 :       gather_summands(specification.action_summands(), specification.process_parameters(), parameter_set, summand_index);
     103           8 :       gather_summands(specification.deadlock_summands(), specification.process_parameters(), parameter_set, summand_index);
     104           8 :     }
     105             : 
     106             :   public:
     107             :     /**
     108             :      * \brief constructor from an mCRL2 lps
     109             :      **/
     110           8 :     group_information(mcrl2::lps::stochastic_specification const& l) : m_model(l)
     111             :     {
     112           8 :       gather(l);
     113           8 :     }
     114             : 
     115             :     /**
     116             :      * \brief The number of groups (summands in the LPS)
     117             :      * \return lps::specification(l).summands().size()
     118             :      **/
     119           8 :     inline std::size_t number_of_groups() const
     120             :     {
     121           8 :       return m_group_indices.size();
     122             :     }
     123             : 
     124             :     inline std::size_t number_of_parameters() const
     125             :     {
     126             :       return m_model.process().process_parameters().size();
     127             :     }
     128             : 
     129             :     /**
     130             :      * \brief Indices of process parameters that influence event or next state of a summand
     131             :      * \param[in] index the selected summand
     132             :      * \returns reference to a vector of indices of parameters
     133             :      **/
     134             :     inline std::vector< std::size_t > const& operator[](std::size_t index) const
     135             :     {
     136             :       return m_group_indices[index];
     137             :     }
     138             : };
     139             : 
     140             : 
     141           8 : void check_info(mcrl2::lps::stochastic_specification const& model)
     142             : {
     143          16 :   group_information info(model);
     144             : 
     145           8 :   BOOST_CHECK(info.number_of_groups() == model.process().summand_count());
     146             : 
     147             : #ifdef SHOW_INFO
     148             :   for (std::size_t i = 0; i < info.number_of_groups(); ++i)
     149             :   {
     150             :     std::vector< std::size_t > const& group_info(info[i]);
     151             : 
     152             :     std::cerr << "group " << i << " : {";
     153             : 
     154             :     if (!group_info.empty())
     155             :     {
     156             :       std::cerr << group_info[0];
     157             :     }
     158             : 
     159             :     for (std::vector< std::size_t >::const_iterator j = ++group_info.begin(); j < group_info.end(); ++j)
     160             :     {
     161             : 
     162             :       std::cerr << "," << *j;
     163             :     }
     164             : 
     165             :     std::cerr << "}" << std::endl;
     166             :   }
     167             : #endif
     168           8 : }
     169             : 
     170           1 : int test_main(int argc, char** argv)
     171             : {
     172             :   using namespace mcrl2;
     173             :   using namespace mcrl2::lps;
     174             : 
     175           1 :   check_info(linearise(case_no_influenced_parameters));
     176           1 :   check_info(linearise(case_influenced_condition));
     177           1 :   check_info(linearise(case_influenced_action));
     178           1 :   check_info(linearise(case_influenced_time));
     179           1 :   check_info(linearise(case_influenced_next));
     180           1 :   check_info(linearise(case_two_parameters));
     181           1 :   check_info(linearise(case_summands));
     182           1 :   check_info(linearise(case_last));
     183             : 
     184           2 :   lps::stochastic_specification model=linearise(case_no_influenced_parameters);
     185             : 
     186           1 :   if (1 < argc)
     187             :   {
     188           0 :     load_lps(model, argv[1]);
     189             : 
     190           0 :     model.process().deadlock_summands().clear();
     191             : 
     192           0 :     data::rewriter        rewriter(model.data());
     193             : 
     194           0 :     next_state_generator explorer(model, rewriter);
     195             : 
     196           0 :     std::stack< state >     stack;
     197           0 :     std::set< state >   known;
     198             : 
     199           0 :     stack.push(explorer.initial_states().front().state());
     200           0 :     known.insert(stack.top());
     201             : 
     202           0 :     while (!stack.empty())
     203             :     {
     204           0 :       state current(stack.top());
     205           0 :       stack.pop();
     206             : 
     207           0 :       for (std::size_t i = 0; i < model.process().summand_count(); ++i)
     208             :       {
     209           0 :         next_state_generator::enumerator_queue_t enumeration_queue;
     210           0 :         for(next_state_generator::iterator j = explorer.begin(current, i, &enumeration_queue); j != explorer.end(); ++j)
     211             :         {
     212           0 :           if (known.find(j->target_state()) == known.end())
     213             :           {
     214           0 :             std::cerr << atermpp::pp(j->target_state()) << std::endl;
     215           0 :             known.insert(j->target_state());
     216           0 :             stack.push(j->target_state());
     217             :           }
     218             :         }
     219             :       }
     220             :     }
     221             :   }
     222             : 
     223           2 :   return 0;
     224           3 : }

Generated by: LCOV version 1.13