Line data    Source code

       1             : // Author(s): Maurice Laveaux, Jan Martens
       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             : 
      10             : #include "mcrl2/data/data_specification.h"
      11             : #include "mcrl2/lps/stochastic_specification.h"
      12             : #include "mcrl2/process/action_label.h"
      13             : #include "mcrl2/process/process_expression.h"
      14             : #define BOOST_TEST_MODULE ltscompare_counter_example_test
      15             : #include <boost/test/included/unit_test.hpp>
      16             : 
      17             : #include "mcrl2/data/parse.h"
      18             : #include "mcrl2/lts/detail/lts_convert.h"
      19             : #include "mcrl2/lts/lts_algorithm.h"
      20             : #include "mcrl2/lts/lts_equivalence.h"
      21             : #include "mcrl2/lts/lts_io.h"
      22             : #include "mcrl2/lts/lts_lts.h"
      23             : #include "mcrl2/pbes/lts2pbes.h"
      24             : #include "mcrl2/pbes/pbesinst_structure_graph.h"
      25             : #include "mcrl2/pbes/solve_structure_graph.h"
      26             : 
      27             : using namespace mcrl2::lps;
      28             : using namespace mcrl2::lts;
      29             : using namespace mcrl2::pbes_system;
      30             : using namespace mcrl2::state_formulas;
      31             : 
      32           4 : static lts_aut_t parse_aut(const std::string& s)
      33             : {
      34           4 :   std::stringstream is(s);
      35           4 :   lts_aut_t l;
      36           4 :   l.load(is);
      37           8 :   return l;
      38           4 : }
      39             : 
      40             : inline
      41           2 : void compare(const char* s1, const char* s2, const char* counterexample_name)
      42             : {    
      43           4 :   mcrl2::lts::lts_aut_t t1 = parse_aut(s1);
      44           4 :   mcrl2::lts::lts_aut_t t2 = parse_aut(s2);
      45             : 
      46           2 :   compare(t1, t2, lts_equivalence::lts_eq_branching_bisim, true, counterexample_name);
      47             : 
      48             :   // Read the counter example file and verify that it is distinguishing
      49           2 :   std::ifstream counter_example(counterexample_name);
      50             : 
      51           2 :   mcrl2::process::action_label_list labels;
      52           2 :   labels.push_front(mcrl2::process::action_label("a", {}));
      53           2 :   labels.push_front(mcrl2::process::action_label("b", {}));
      54           2 :   labels.push_front(mcrl2::process::action_label("tau", {}));
      55             : 
      56             :   // Convert aut to lts format for lts2pbes
      57           2 :   lts_lts_t t1_lts;
      58           2 :   lts_lts_t t2_lts;
      59             : 
      60           2 :   lts_convert(t1, t1_lts, {}, labels, {}, true);
      61           2 :   lts_convert(t2, t2_lts, {}, labels, {}, true);
      62             : 
      63             :   // Parse a formula and make up some action declaration since that is necessary.  
      64           4 :   stochastic_specification spec({}, t1_lts.action_label_declarations(), {}, {}, {});
      65           2 :   mcrl2::state_formulas::state_formula formula = mcrl2::state_formulas::algorithms::parse_state_formula(counter_example, spec, false);
      66             : 
      67           2 :   lts2pbes_algorithm algorithm1(t1_lts);
      68           4 :   auto t1_pbes = algorithm1.run(formula);
      69             : 
      70           2 :   lts2pbes_algorithm algorithm2(t2_lts);
      71           4 :   auto t2_pbes = algorithm2.run(formula);
      72             : 
      73           2 :   pbessolve_options options;
      74           2 :   structure_graph G1;
      75           2 :   pbesinst_structure_graph_algorithm algorithm_inst1(options, t1_pbes, G1);
      76           2 :   algorithm_inst1.run();
      77             : 
      78           2 :   structure_graph G2;
      79           2 :   pbesinst_structure_graph_algorithm algorithm_inst2(options, t2_pbes, G2);
      80           2 :   algorithm_inst2.run();
      81             : 
      82           2 :   solve_structure_graph_algorithm algorithm_solve(true, false);   
      83           2 :   BOOST_CHECK_NE(algorithm_solve.solve(G1), algorithm_solve.solve(G2));  
      84           2 : }
      85             : 
      86           2 : BOOST_AUTO_TEST_CASE(ltscompare_br_hard_test)
      87             : {
      88           1 :     auto br_hard1 = R"(des (0,9,7)
      89             :         (0,"tau",1)
      90             :         (6, "tau", 1)
      91             :         (1, "tau", 2)
      92             :         (2, "tau", 3)
      93             :         (1, "tau", 4)
      94             :         (2, "tau", 5)
      95             :         (0, "tau", 3)
      96             :         (4, a, 4)
      97             :         (5, b, 5)
      98             :     )";
      99             : 
     100             :     
     101           1 :     auto br_hard2 = R"(des (6,9,7)
     102             :         (0,"tau",1)
     103             :         (6, "tau", 1)
     104             :         (1, "tau", 2)
     105             :         (2, "tau", 3)
     106             :         (1, "tau", 4)
     107             :         (2, "tau", 5)
     108             :         (0, "tau", 3)
     109             :         (4, a, 4)
     110             :         (5, b, 5)
     111             :     )";
     112             : 
     113           1 :     compare(br_hard1, br_hard2, "br_hard_counterexample.mcf");
     114           1 : }
     115             : 
     116           2 : BOOST_AUTO_TEST_CASE(ltscompare_tau_dist_test)
     117             : {
     118           1 :     auto tau_dist1 = R"(des (0,3,2)
     119             :         (0,"tau",1)
     120             :         (0,"a",1)
     121             :         (0,"b",1)
     122             :     )";
     123             :     
     124           1 :     auto tau_dist2 = R"(des (0,4,3)
     125             :         (0,"a",2)
     126             :         (0,"b",2)
     127             :         (0, "tau",1)
     128             :         (1,"b",2)
     129             :     )";
     130             : 
     131           1 :     compare(tau_dist1, tau_dist2, "tau_dist_counterexample.mcf");
     132           1 : }