LCOV - code coverage report
Current view: top level - lts/test - lps2lts_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 199 202 98.5 %
Date: 2020-02-19 00:44:21 Functions: 69 70 98.6 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): mCRL2 team
       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_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_WITH_GARBAGE_COLLECTION
      13             : #define MCRL2_WITH_GARBAGE_COLLECTION
      14             : #endif
      15             : 
      16             : #define BOOST_TEST_MODULE lps2lts_test
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : #include "mcrl2/data/detail/rewrite_strategies.h"
      20             : #include "mcrl2/lts/detail/exploration.h"
      21             : #include "mcrl2/lps/is_stochastic.h"
      22             : #include "mcrl2/lts/state_space_generator.h"
      23             : #include "mcrl2/lts/stochastic_lts_builder.h"
      24             : #include "mcrl2/utilities/test_utilities.h"
      25             : 
      26             : using namespace mcrl2;
      27             : using namespace mcrl2::lps;
      28             : 
      29             : template <bool Stochastic, bool Timed, typename Specification, typename LTSBuilder>
      30         168 : void generate_state_space(const Specification& lpsspec, LTSBuilder& builder, const std::string& output_filename, const lps::explorer_options& options)
      31             : {
      32         336 :   lts::state_space_generator<Stochastic, Timed, Specification> generator(lpsspec, options);
      33         168 :   generator.explore(builder);
      34         168 :   builder.save(output_filename);
      35         168 : }
      36             : 
      37         336 : std::string file_extension(lts::lts_type output_format)
      38             : {
      39         336 :   switch (output_format)
      40             :   {
      41         112 :     case lts::lts_lts: return ".lts";
      42         112 :     case lts::lts_aut: return ".aut";
      43         112 :     case lts::lts_fsm: return ".fsm";
      44           0 :     case lts::lts_dot: return ".dot";
      45           0 :     default: throw mcrl2::runtime_error("unsupported format");
      46             :   }
      47             : }
      48             : 
      49         168 : void run_lps2lts(
      50             :   const lps::stochastic_specification& stochastic_lpsspec,
      51             :   data::rewrite_strategy rstrategy,
      52             :   lps::exploration_strategy estrategy,
      53             :   lts::lts_type output_format,
      54             :   const std::string& outputfile,
      55             :   const std::string& priority_action
      56             : )
      57             : {
      58         336 :   lts::lts_generation_options options;
      59         168 :   options.trace_prefix = "lps2lts_test";
      60         168 :   options.priority_action = priority_action;
      61         168 :   options.strat = rstrategy;
      62         168 :   options.specification = stochastic_lpsspec;
      63         168 :   options.expl_strat = estrategy;
      64         168 :   options.lts = outputfile;
      65         168 :   options.outformat = output_format;
      66         336 :   lts::lps2lts_algorithm lps2lts;
      67         168 :   lps2lts.generate_lts(options);
      68         168 : }
      69             : 
      70         168 : void run_generatelts(
      71             :   const lps::stochastic_specification& stochastic_lpsspec,
      72             :   data::rewrite_strategy rstrategy,
      73             :   lps::exploration_strategy estrategy,
      74             :   lts::lts_type output_format,
      75             :   const std::string& outputfile,
      76             :   const std::string& priority_action
      77             : )
      78             : {
      79         336 :   lps::explorer_options options;
      80         168 :   options.trace_prefix = "lps2lts_test";
      81         168 :   options.confluence_action = priority_action;
      82         168 :   options.rewrite_strategy = rstrategy;
      83         168 :   options.search_strategy = estrategy;
      84         168 :   options.save_aut_at_end = true;
      85             : 
      86         168 :   bool is_timed = stochastic_lpsspec.process().has_time();
      87             : 
      88         168 :   if (lps::is_stochastic(stochastic_lpsspec))
      89             :   {
      90          24 :     auto builder = create_stochastic_lts_builder(stochastic_lpsspec, options, output_format);
      91          12 :     if (is_timed)
      92             :     {
      93           0 :       generate_state_space<true, true>(stochastic_lpsspec, *builder, outputfile, options);
      94             :     }
      95             :     else
      96             :     {
      97          12 :       generate_state_space<true, false>(stochastic_lpsspec, *builder, outputfile, options);
      98             :     }
      99             :   }
     100             :   else
     101             :   {
     102         312 :     lps::specification lpsspec = lps::remove_stochastic_operators(stochastic_lpsspec);
     103         312 :     auto builder = create_lts_builder(lpsspec, options, output_format);
     104         156 :     if (is_timed)
     105             :     {
     106           6 :       generate_state_space<false, true>(lpsspec, *builder, outputfile, options);
     107             :     }
     108             :     else
     109             :     {
     110         150 :       generate_state_space<false, false>(lpsspec, *builder, outputfile, options);
     111             :     }
     112             :   }
     113         168 : }
     114             : 
     115             : template <typename LTSType>
     116         168 : void check_lts(
     117             :   const std::string& format,
     118             :   const lps::stochastic_specification& stochastic_lpsspec,
     119             :   data::rewrite_strategy rstrategy,
     120             :   lps::exploration_strategy estrategy,
     121             :   std::size_t expected_states,
     122             :   std::size_t expected_transitions,
     123             :   std::size_t expected_labels,
     124             :   const std::string& priority_action = ""
     125             : )
     126             : {
     127         168 :   std::clog << "Translating LPS to LTS with exploration strategy " << estrategy << ", rewrite strategy " << rstrategy << "." << std::endl;
     128         336 :   LTSType result1;
     129         336 :   LTSType result2;
     130         168 :   lts::lts_type output_format = result1.type();
     131         336 :   std::string outputfile1 = static_cast<std::string>(boost::unit_test::framework::current_test_case().p_name) + ".lps2lts" + file_extension(output_format);
     132         336 :   std::string outputfile2 = static_cast<std::string>(boost::unit_test::framework::current_test_case().p_name) + ".generatelts" + file_extension(output_format);
     133         168 :   run_lps2lts(stochastic_lpsspec, rstrategy, estrategy, output_format, outputfile1, priority_action);
     134         168 :   run_generatelts(stochastic_lpsspec, rstrategy, estrategy, output_format, outputfile2, priority_action);
     135         168 :   result1.load(outputfile1);
     136         168 :   result2.load(outputfile2);
     137             : 
     138         168 :   std::cerr << format << " FORMAT\n";
     139         168 :   BOOST_CHECK_EQUAL(result1.num_states(), expected_states);
     140         168 :   BOOST_CHECK_EQUAL(result1.num_transitions(), expected_transitions);
     141         168 :   BOOST_CHECK_EQUAL(result1.num_action_labels(), expected_labels);
     142         168 :   BOOST_CHECK_EQUAL(result2.num_states(), expected_states);
     143         168 :   BOOST_CHECK_EQUAL(result2.num_transitions(), expected_transitions);
     144         168 :   BOOST_CHECK_EQUAL(result2.num_action_labels(), expected_labels);
     145             : 
     146         168 :   std::remove(outputfile1.c_str());
     147         168 :   std::remove(outputfile2.c_str());
     148         168 : }
     149             : 
     150          28 : static void check_lps2lts_specification(const std::string& specification,
     151             :                                         const std::size_t expected_states,
     152             :                                         const std::size_t expected_transitions,
     153             :                                         const std::size_t expected_labels,
     154             :                                         const std::string& priority_action = "")
     155             : {
     156          28 :   std::cerr << "CHECK STATE SPACE GENERATION FOR:\n" << specification << "\n";
     157          56 :   lps::stochastic_specification lpsspec;
     158          28 :   parse_lps(specification, lpsspec);
     159          28 :   bool contains_probabilities = lps::is_stochastic(lpsspec);
     160             : 
     161          56 :   for (data::rewrite_strategy rstrategy: data::detail::get_test_rewrite_strategies(false))
     162             :   {
     163          84 :     for (lps::exploration_strategy estrategy: { lps::es_breadth, lps::es_depth })
     164             :     {
     165          56 :       if (contains_probabilities)
     166             :       {
     167           4 :         check_lts<lts::probabilistic_lts_aut_t>("PROBABILISTIC AUT", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     168           4 :         check_lts<lts::probabilistic_lts_lts_t>("PROBABILISTIC LTS", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     169           4 :         check_lts<lts::probabilistic_lts_fsm_t>("PROBABILISTIC FSM", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     170             :       }
     171             :       else
     172             :       {
     173          52 :         check_lts<lts::lts_aut_t>("AUT", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     174          52 :         check_lts<lts::lts_lts_t>("LTS", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     175          52 :         check_lts<lts::lts_fsm_t>("FSM", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
     176             :       }
     177             :     }
     178             :   }
     179          28 : }
     180             : 
     181           3 : BOOST_AUTO_TEST_CASE(test_a_delta)
     182             : {
     183             :   std::string lps(
     184             :     "act a;\n"
     185             :     "proc P(b:Bool) = (b) -> a.P(!b)\n"
     186             :     "               + delta;\n"
     187             :     "init P(true);\n"
     188           2 :   );
     189           1 :   check_lps2lts_specification(lps, 2, 1, 2);
     190           1 : }
     191             : 
     192           3 : BOOST_AUTO_TEST_CASE(test_abp)
     193             : {
     194             :   std::string abp(
     195             :     "sort Error = struct e;\n"
     196             :     "     D = struct d1 | d2;\n"
     197             :     "\n"
     198             :     "act  i;\n"
     199             :     "     c6,r6,s6: Error;\n"
     200             :     "     c6,r6,s6,c5,r5,s5: Bool;\n"
     201             :     "     c3,r3,s3: Error;\n"
     202             :     "     c3,r3,s3,c2,r2,s2: D # Bool;\n"
     203             :     "     s4,r1: D;\n"
     204             :     "\n"
     205             :     "glob dc,dc0,dc1,dc3,dc5,dc7,dc13,dc14,dc15,dc16,dc17,dc18: D;\n"
     206             :     "     dc2,dc4,dc6,dc8,dc9,dc10,dc11,dc12: Bool;\n"
     207             :     "\n"
     208             :     "proc P(s30_S: Pos, d_S: D, b_S: Bool, s31_K: Pos, d_K: D, b_K: Bool, s32_L: Pos, b_L: Bool, s33_R: Pos, d_R: D, b_R: Bool) =\n"
     209             :     "       sum d0_S: D.\n"
     210             :     "         (s30_S == 1) ->\n"
     211             :     "         r1(d0_S) .\n"
     212             :     "         P(s30_S = 2, d_S = d0_S)\n"
     213             :     "     + sum e0_K: Bool.\n"
     214             :     "         (s31_K == 2) ->\n"
     215             :     "         i .\n"
     216             :     "         P(s31_K = if(e0_K, 4, 3), d_K = if(e0_K, dc3, d_K), b_K = if(e0_K, dc4, b_K))\n"
     217             :     "     + sum e1_L: Bool.\n"
     218             :     "         (s32_L == 2) ->\n"
     219             :     "         i .\n"
     220             :     "         P(s32_L = if(e1_L, 4, 3), b_L = if(e1_L, dc10, b_L))\n"
     221             :     "     + (s33_R == 2) ->\n"
     222             :     "         s4(d_R) .\n"
     223             :     "         P(s33_R = 3, d_R = dc16)\n"
     224             :     "     + sum e2_R: Bool.\n"
     225             :     "         (s32_L == 1 && if(e2_R, s33_R == 4, s33_R == 3)) ->\n"
     226             :     "         c5(if(e2_R, !b_R, b_R)) .\n"
     227             :     "         P(s32_L = 2, b_L = if(e2_R, !b_R, b_R), s33_R = 1, d_R = if(e2_R, dc18, dc17), b_R = if(e2_R, b_R, !b_R))\n"
     228             :     "     + (s31_K == 4 && s33_R == 1) ->\n"
     229             :     "         c3(e) .\n"
     230             :     "         P(s31_K = 1, d_K = dc7, b_K = dc8, s33_R = 4, d_R = dc15)\n"
     231             :     "     + sum e3_R: Bool.\n"
     232             :     "         ((s31_K == 3 && s33_R == 1) && if(e3_R, !b_R, b_R) == b_K) ->\n"
     233             :     "         c3(d_K, if(e3_R, !b_R, b_R)) .\n"
     234             :     "         P(s31_K = 1, d_K = dc5, b_K = dc6, s33_R = if(e3_R, 4, 2), d_R = if(e3_R, dc14, d_K))\n"
     235             :     "     + (s30_S == 2 && s31_K == 1) ->\n"
     236             :     "         c2(d_S, b_S) .\n"
     237             :     "         P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S)\n"
     238             :     "     + (s30_S == 3 && s32_L == 4) ->\n"
     239             :     "         c6(e) .\n"
     240             :     "         P(s30_S = 2, s32_L = 1, b_L = dc12)\n"
     241             :     "     + sum e_S: Bool.\n"
     242             :     "         ((s30_S == 3 && s32_L == 3) && if(e_S, b_S, !b_S) == b_L) ->\n"
     243             :     "         c6(if(e_S, b_S, !b_S)) .\n"
     244             :     "         P(s30_S = if(e_S, 1, 2), d_S = if(e_S, dc0, d_S), b_S = if(e_S, !b_S, b_S), s32_L = 1, b_L = dc11)\n"
     245             :     "     + delta;\n"
     246             :     "\n"
     247             :     "init P(1, dc, true, 1, dc1, dc2, 1, dc9, 1, dc13, true);\n"
     248           2 :   );
     249           1 :   check_lps2lts_specification(abp, 74, 92, 20);
     250           1 :   check_lps2lts_specification(abp, 74, 92, 20, "tau");
     251           1 : }
     252             : 
     253           3 : BOOST_AUTO_TEST_CASE(test_confluence)
     254             : {
     255             :   std::string spec(
     256             :     "sort State = struct S_FSM_UNINITIALIZED?isS_FSM_UNINITIALIZED | S_OFF?isS_OFF;\n"
     257             :     "     IdList = List(Nat);\n"
     258             :     "\n"
     259             :     "act  rs: State;\n"
     260             :     "\n"
     261             :     "proc P(s3_P: Pos, s1_P: State, ActPhaseArgs_pp2_P: IdList) =\n"
     262             :     "       (s3_P == 1 && ActPhaseArgs_pp2_P == []) ->\n"
     263             :     "         tau .\n"
     264             :     "         P(s3_P = 1, s1_P = S_FSM_UNINITIALIZED, ActPhaseArgs_pp2_P = [12, 9])\n"
     265             :     "     + sum s11_P: State.\n"
     266             :     "         (s3_P == 1 && !(ActPhaseArgs_pp2_P == [])) ->\n"
     267             :     "         rs(s11_P) .\n"
     268             :     "         P(s3_P = 2, s1_P = s11_P)\n"
     269             :     "     + delta;\n"
     270             :     "\n"
     271             :     "init P(1, S_FSM_UNINITIALIZED, []);\n"
     272           2 :   );
     273           1 :   check_lps2lts_specification(spec, 4, 3, 3);
     274           1 :   check_lps2lts_specification(spec, 3, 2, 3, "tau");
     275           1 : }
     276             : 
     277           3 : BOOST_AUTO_TEST_CASE(test_function_updates)
     278             : {
     279             :   std::string spec(
     280             :     "act  set,s: Pos;\n"
     281             :     "map  f:Pos->Bool;\n"
     282             :     "var  n:Pos;\n"
     283             :     "eqn  f(n)=false;\n"
     284             :     "\n"
     285             :     "proc P(b_Sensor: Pos -> Bool) =\n"
     286             :     "       sum n_Sensor: Pos.\n"
     287             :     "         (n_Sensor <= 2) ->\n"
     288             :     "         s(n_Sensor) .\n"
     289             :     "         P(b_Sensor = b_Sensor[n_Sensor -> true])\n"
     290             :     "     + sum n_Sensor0: Pos.\n"
     291             :     "         (b_Sensor(n_Sensor0) && n_Sensor0 <= 2) ->\n"
     292             :     "         set(n_Sensor0) .\n"
     293             :     "         P(b_Sensor = b_Sensor[n_Sensor0 -> false])\n"
     294             :     "     + delta;\n"
     295             :     "\n"
     296             :     "init P(f);\n"
     297           2 :   );
     298           1 :   check_lps2lts_specification(spec, 4, 12, 5);
     299           1 : }
     300             : 
     301           3 : BOOST_AUTO_TEST_CASE(test_timed) // For bug #756
     302             : {
     303             :   std::string spec(
     304             :     "act  a,Terminate;\n"
     305             :     "\n"
     306             :     "proc P(s3: Pos) =\n"
     307             :     "       (s3 == 1) ->\n"
     308             :     "         a @ 3 .\n"
     309             :     "         P(s3 = 2)\n"
     310             :     "     + (s3 == 2) ->\n"
     311             :     "         Terminate .\n"
     312             :     "         P(s3 = 3)\n"
     313             :     "     + (s3 == 3) ->\n"
     314             :     "         delta;\n"
     315             :     "\n"
     316             :     "init P(1);\n"
     317           2 :   );
     318           1 :   check_lps2lts_specification(spec, 3, 2, 3);
     319           1 : }
     320             : 
     321           3 : BOOST_AUTO_TEST_CASE(test_struct)
     322             : {
     323             :   std::string spec(
     324             :     "sort Bits = struct b0 | b1;\n"
     325             :     "     t_sys_regset_fsm_state = Bits;\n"
     326             :     "     t_timer_counter_fsm_state = Bits;\n"
     327             :     "map  timer_counter_fsm_state_idle: Bits;\n"
     328             :     "act  a: t_sys_regset_fsm_state;\n"
     329             :     "glob globd: t_sys_regset_fsm_state;\n"
     330             :     "proc P(s3_P: Pos) =\n"
     331             :     "       (s3_P == 1) ->\n"
     332             :     "         a(globd) .\n"
     333             :     "         P(s3_P = 2)\n"
     334             :     "     + delta;\n"
     335             :     "init P(1);\n"
     336           2 :   );
     337           1 :   check_lps2lts_specification(spec, 2, 1, 2);
     338           1 : }
     339             : 
     340           3 : BOOST_AUTO_TEST_CASE(test_alias_complex)
     341             : {
     342             :   std::string spec(
     343             :     "sort Bits = struct singleBit(bit: Bool)?isSingleBit | bitVector(bitVec: List(Bool))?isBitVector;\n"
     344             :     "     t_sys_regset_fsm_state = Bits;\n"
     345             :     "     t_timer_counter_fsm_state = Bits;\n"
     346             :     "\n"
     347             :     "map  repeat_rec: Bool # Nat -> List(Bool);\n"
     348             :     "     repeat: Bool # Nat -> Bits;\n"
     349             :     "\n"
     350             :     "var  b: Bool;\n"
     351             :     "     n: Nat;\n"
     352             :     "eqn  repeat(b, n)  =  if(n <= 1, singleBit(b), bitVector(repeat_rec(b, n)));\n"
     353             :     "\n"
     354             :     "act  a: t_sys_regset_fsm_state;\n"
     355             :     "\n"
     356             :     "proc P(s3: Pos) =\n"
     357             :     "       (s3 == 1) ->\n"
     358             :     "         a(repeat(true, 32)) .\n"
     359             :     "         P(s3 = 2)\n"
     360             :     "     + delta;\n"
     361             :     "\n"
     362             :     "init P(1);\n"
     363           2 :   );
     364           1 :   check_lps2lts_specification(spec, 2, 1, 2);
     365           1 : }
     366             : 
     367           3 : BOOST_AUTO_TEST_CASE(test_equality_with_empty_set)
     368             : {
     369             :   std::string spec(
     370             :     "map  emptyset:Set(Bool);\n"
     371             :     "eqn  emptyset={};\n"
     372             :     "proc P=({ b: Bool | false }  == emptyset) -> tau.P;\n"
     373             :     "init P;"
     374           2 :   );
     375           1 :   check_lps2lts_specification(spec, 1, 1, 1);
     376           1 : }
     377             : 
     378           3 : BOOST_AUTO_TEST_CASE(test_equality_of_finite_sets)
     379             : {
     380             :   std::string spec(
     381             :     "sort R = struct r2 | r1 ;\n"
     382             :     "map All: Set(R);\n"
     383             :     "eqn All = {  r: R | true };\n"
     384             :     "proc P=({r1, r2} == All) -> tau.P;\n"
     385             :     "init P;"
     386           2 :   );
     387           1 :   check_lps2lts_specification(spec, 1, 1, 1);
     388           1 : }
     389             : 
     390             : // Example from bug #832
     391           3 : BOOST_AUTO_TEST_CASE(test_plus)
     392             : {
     393             :   // This example provides two identical transitions between a state.
     394             :   // There is a discussion on whether this is desirable. Currently, for
     395             :   // efficiency reasons such extra transitions are not removed by lps2lts.
     396             :   std::string spec(
     397             :     "act a;\n"
     398             :     "proc P = a.P + a.P;\n"
     399             :     "init P;\n"
     400           2 :   );
     401           1 :   check_lps2lts_specification(spec, 1, 2, 2);
     402           1 : }
     403             : 
     404             : // The example below fails if #[0,1] does not have a decent
     405             : // type. The tricky thing is that the type of the list can be List(Nat),
     406             : // List(Int) or List(Real). Toolset version 10180 resolved this by
     407             : // delivering the type List({Nat, Int, Real}), i.e. a set of possible
     408             : // options. But this was not expected and understood by the other tools.
     409             : // This is related to bug report #949.
     410           3 : BOOST_AUTO_TEST_CASE(test_well_typedness_of_length_of_list_of_numbers)
     411             : {
     412             :   std::string spec(
     413             :     "proc B (i:Int) = (i >= 2) -> tau. B();\n"
     414             :     "init B(#[0,1]);\n"
     415           2 :   );
     416           1 :   check_lps2lts_specification(spec, 1, 1, 1);
     417           1 : }
     418             : 
     419             : #if 0 // This test has been disabled; it was decided not to fix this issue.
     420             : // The following example illustrates that enumeration can sometimes need
     421             : // a large stack depth.
     422             : // The example was attached to bug #1019, and fails with limited stack,
     423             : // succeeds with unlimited stack.
     424             : BOOST_AUTO_TEST_CASE(test_deep_stack)
     425             : {
     426             :   std::string spec(
     427             :     "sort Packet = struct packet(d0: Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool);\n"
     428             :     "act  Terminate;\n"
     429             :     "proc P(s3: Pos) =\n"
     430             :     "   (s3 == 2) ->\n"
     431             :     "     Terminate .\n"
     432             :     "     P(s3 = 3)\n"
     433             :     " + sum p: Packet.\n"
     434             :     "     (s3 == 1) ->\n"
     435             :     "     tau .\n"
     436             :     "     P(s3 = 2)\n"
     437             :     " + delta;\n"
     438             :     "init P(1);\n"
     439             :   );
     440             :   check_lps2lts_specification(spec, 3, 524289, 2);
     441             : }
     442             : #endif // false
     443             : 
     444             : 
     445           3 : BOOST_AUTO_TEST_CASE(test_max_states)
     446             : {
     447             :   std::string spec(
     448             :   "act a;\n"
     449             :   "proc P(s: Pos) =\n"
     450             :   "  (s <= 10) -> a . P(s+1);\n"
     451           2 :   "init P(1);\n");
     452             : 
     453           2 :   lps::stochastic_specification specification;
     454           1 :   parse_lps(spec,specification);
     455             : 
     456           2 :   lts::lts_generation_options options;
     457           1 :   options.trace_prefix = "lps2lts_test";
     458           1 :   options.specification = specification;
     459           1 :   options.lts = utilities::temporary_filename("lps2lts_test_file");
     460           1 :   options.max_states = 5;
     461             : 
     462           2 :   lts::lts_aut_t result;
     463           1 :   options.outformat = result.type();
     464           2 :   lts::lps2lts_algorithm lps2lts;
     465           1 :   lps2lts.generate_lts(options);
     466           1 :   result.load(options.lts);
     467           1 :   remove(options.lts.c_str()); // Clean up after ourselves
     468             : 
     469           1 :   BOOST_CHECK_LT(result.num_states(), 10u);
     470           1 : }
     471             : 
     472           3 : BOOST_AUTO_TEST_CASE(test_interaction_sum_and_assignment_notation1)
     473             : {
     474             :   std::string spec(
     475             :     "proc B (i:Bool) = sum i:Bool.tau. B();\n"
     476             :     "init B(true);\n"
     477           2 :   );
     478           1 :   check_lps2lts_specification(spec, 1, 2, 1);
     479           1 : }
     480             : 
     481           3 : BOOST_AUTO_TEST_CASE(test_interaction_sum_and_assignment_notation2)
     482             : {
     483             :   std::string spec(
     484             :     "proc B (i:Bool) = sum i:Bool.tau. B(i=i);\n"
     485             :     "init B(true);\n"
     486           2 :   );
     487           1 :   check_lps2lts_specification(spec, 2, 4, 1);
     488           1 : }
     489             : 
     490           3 : BOOST_AUTO_TEST_CASE(test_whether_function_update_is_declared)
     491             : {
     492             :   std::string spec(
     493             :     "sort  T = struct a|b;\n"
     494             :     "act int;\n"
     495             :     "map g: Bool -> T;\n"
     496             :     "var y: Bool;\n"
     497             :     "eqn g(y) = a;\n"
     498             :     "act d: Bool -> T;\n"
     499             :     "proc P(f: Bool -> T) = int . P(f[true->b]);\n"
     500             :     "init P(g) ;\n"
     501           2 :   );
     502           1 :   check_lps2lts_specification(spec, 2, 2, 2);
     503           1 : }
     504             : 
     505           3 : BOOST_AUTO_TEST_CASE(test_whether_bag_enumeration_with_similar_elements_is_allowed)
     506             : {
     507             :   std::string spec(
     508             :     "sort S = struct s1 | s2;\n"
     509             :     "act int;\n"
     510             :     "proc P(b: Bag(S)) = (count(s1, b) < 3) -> int.P();\n"
     511             :     "init P({s1: 1, s1: 1});\n"
     512           2 :   );
     513           1 :   check_lps2lts_specification(spec, 1, 1, 2);
     514           1 : }
     515             : 
     516           3 : BOOST_AUTO_TEST_CASE(test_whether_functions_to_functions_are_causing_problems)
     517             : {
     518             :   std::string spec(
     519             :     "map f:Nat->Nat->Nat->Nat;\n"
     520             :     "    g:Nat->Nat;\n"
     521             :     "var x,y,z:Nat;"
     522             :     "eqn f(x)(y)(z)=x+y+z;\n"
     523             :     "    f(x)(y)=g;\n"
     524             :     "act int:Nat;\n"
     525             :     "proc P = int(f(1)(2)(3)).P();\n"
     526             :     "init P;\n"
     527           2 :   );
     528           1 :   check_lps2lts_specification(spec, 1, 1, 2);
     529           1 : }
     530             : 
     531           3 : BOOST_AUTO_TEST_CASE(test_whether_functions_can_be_enumerated)
     532             : {
     533             :   std::string spec(
     534             :     "act int:Bool->Bool;\n"
     535             :     "proc P = sum f:Bool->Bool.int(f).P;\n"
     536             :     "init P;\n"
     537           2 :   );
     538           1 :   check_lps2lts_specification(spec, 1, 4, 5);
     539           1 : }
     540             : 
     541           3 : BOOST_AUTO_TEST_CASE(test_whether_functions_with_more_arguments_can_be_enumerated)
     542             : {
     543             :   std::string spec(
     544             :     "act int:Bool#Bool#Bool->Bool;\n"
     545             :     "proc P = sum f:Bool#Bool#Bool->Bool.f(true,true,true)->int(f).P;\n"
     546             :     "init P;\n"
     547           2 :   );
     548           1 :   check_lps2lts_specification(spec, 1, 128, 129);
     549           1 : }
     550             : 
     551           3 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_can_be_enumerated)
     552             : {
     553             :   std::string spec(
     554             :     "act int:FSet(Bool);\n"
     555             :     "proc P = sum f:FSet(Bool).int(f).P;\n"
     556             :     "init P;\n"
     557           2 :   );
     558           1 :   check_lps2lts_specification(spec, 1, 4, 5);
     559           1 : }
     560             : 
     561           3 : BOOST_AUTO_TEST_CASE(test_whether_sets_can_be_enumerated)
     562             : {
     563             :   std::string spec(
     564             :     "act int:FSet(Bool);\n"
     565             :     "proc P = sum f:FSet(Bool).int(f).P;\n"
     566             :     "init P;\n"
     567           2 :   );
     568           1 :   check_lps2lts_specification(spec, 1, 4, 5);
     569           1 : }
     570             : 
     571           3 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_with_conditions_can_be_enumerated)
     572             : {
     573             :   std::string spec(
     574             :     "act int:FSet(Bool);\n"
     575             :     "proc P = sum f:FSet(Bool).(true in f) -> int(f).P;\n"
     576             :     "init P;\n"
     577           2 :   );
     578           1 :   check_lps2lts_specification(spec, 1, 2, 3);
     579           1 : }
     580             : 
     581           3 : BOOST_AUTO_TEST_CASE(test_whether_sets_with_conditions_can_be_enumerated)
     582             : {
     583             :   std::string spec(
     584             :     "act int:Set(Bool);\n"
     585             :     "proc P = sum f:Set(Bool).(true in f) -> int(f).P;\n"
     586             :     "init P;\n"
     587           2 :   );
     588           1 :   check_lps2lts_specification(spec, 1, 2, 3);
     589           1 : }
     590             : 
     591           3 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_of_functions_can_be_enumerated)
     592             : {
     593             :   std::string spec(
     594             :     "act int:FSet(Bool->Bool);\n"
     595             :     "proc P = sum f:FSet(Bool->Bool).((lambda x:Bool.true) in f) -> int(f).P;\n"
     596             :     "init P;\n"
     597           2 :   );
     598           1 :   check_lps2lts_specification(spec, 1, 8, 9);
     599           1 : }
     600             : 
     601           3 : BOOST_AUTO_TEST_CASE(test_whether_sets_of_functions_can_be_enumerated)
     602             : {
     603             :   std::string spec(
     604             :     "act int:Set(Bool->Bool);\n"
     605             :     "proc P = sum f:Set(Bool->Bool).((lambda x:Bool.true) in f) -> int(f).P;\n"
     606             :     "init P;\n"
     607           2 :   );
     608           1 :   check_lps2lts_specification(spec, 1, 8, 9);
     609           1 : }
     610             : 
     611           3 : BOOST_AUTO_TEST_CASE(test_whether_probabilistic_state_spaces_are_generated_correctly)   // Related to #1542
     612             : {
     613             :   std::string spec(
     614             :     "act a;\n"
     615             :     "proc P(b:Bool) = b->a.P(false);\n"
     616             :     "init dist b: Bool[if(b, 1 / 4, 3 / 4)] . P(b);\n"
     617           2 :   );
     618           1 :   check_lps2lts_specification(spec, 2, 1, 2);
     619           1 : }
     620             : 
     621           3 : BOOST_AUTO_TEST_CASE(coins_simulate_dice)   // Example from the probabilistic examples directory. 
     622             : {
     623             :     std::string spec(
     624             :     "act  flip: Bool;\n"
     625             :     "     dice: Nat;\n"
     626             :     "\n"
     627             :     "glob dc,dc3,dc4,dc5,dc6,dc7,dc8,dc9,dc10,dc11,dc12,dc13,dc14,dc15,dc16,dc17,dc18,dc19: Bool;\n"
     628             :     "     dc1,dc2: Nat;\n"
     629             :     "\n"
     630             :     "proc P(s1: Pos, b3,b2: Bool, s,d: Nat) =\n"
     631             :     "       (s1 == 1 && b2 && s == 0) ->\n"
     632             :     "         flip(b2) .\n"
     633             :     "         dist b2: Bool[1 / 2] .\n"
     634             :     "         P(s1 = 1, b3 = dc3, b2 = b2, s = 1, d = 0)\n"
     635             :     "     + (s1 == 1 && !b2 && s == 0) ->\n"
     636             :     "         flip(b2) .\n"
     637             :     "         dist b2: Bool[1 / 2] .\n"
     638             :     "         P(s1 = 1, b3 = dc4, b2 = b2, s = 2, d = 0)\n"
     639             :     "     + (s1 == 1 && b2 && s == 1 && !(s == 0)) ->\n"
     640             :     "         flip(b2) .\n"
     641             :     "         dist b2: Bool[1 / 2] .\n"
     642             :     "         P(s1 = 1, b3 = dc5, b2 = b2, s = 3, d = 0)\n"
     643             :     "     + (s1 == 1 && !b2 && s == 1 && !(s == 0)) ->\n"
     644             :     "         flip(b2) .\n"
     645             :     "         dist b2: Bool[1 / 2] .\n"
     646             :     "         P(s1 = 1, b3 = dc6, b2 = b2, s = 4, d = 0)\n"
     647             :     "     + (s1 == 1 && b2 && s == 2 && !(s == 1) && !(s == 0)) ->\n"
     648             :     "         flip(b2) .\n"
     649             :     "         dist b2: Bool[1 / 2] .\n"
     650             :     "         P(s1 = 1, b3 = dc7, b2 = b2, s = 5, d = 0)\n"
     651             :     "     + (s1 == 1 && !b2 && s == 2 && !(s == 1) && !(s == 0)) ->\n"
     652             :     "         flip(b2) .\n"
     653             :     "         dist b2: Bool[1 / 2] .\n"
     654             :     "         P(s1 = 1, b3 = dc8, b2 = b2, s = 6, d = 0)\n"
     655             :     "     + (s1 == 1 && b2 && s == 3 && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     656             :     "         flip(b2) .\n"
     657             :     "         dist b2: Bool[1 / 2] .\n"
     658             :     "         P(s1 = 1, b3 = dc9, b2 = b2, s = 1, d = 0)\n"
     659             :     "     + (s1 == 1 && !b2 && s == 3 && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     660             :     "         flip(b2) .\n"
     661             :     "         dist b2: Bool[1 / 2] .\n"
     662             :     "         P(s1 = 1, b3 = dc10, b2 = b2, s = 7, d = 1)\n"
     663             :     "     + (s1 == 1 && b2 && s == 4 && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     664             :     "         flip(b2) .\n"
     665             :     "         dist b2: Bool[1 / 2] .\n"
     666             :     "         P(s1 = 1, b3 = dc11, b2 = b2, s = 7, d = 2)\n"
     667             :     "     + (s1 == 1 && !b2 && s == 4 && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     668             :     "         flip(b2) .\n"
     669             :     "         dist b2: Bool[1 / 2] .\n"
     670             :     "         P(s1 = 1, b3 = dc12, b2 = b2, s = 7, d = 3)\n"
     671             :     "     + (s1 == 1 && b2 && s == 5 && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     672             :     "         flip(b2) .\n"
     673             :     "         dist b2: Bool[1 / 2] .\n"
     674             :     "         P(s1 = 1, b3 = dc13, b2 = b2, s = 7, d = 4)\n"
     675             :     "     + (s1 == 1 && !b2 && s == 5 && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     676             :     "         flip(b2) .\n"
     677             :     "         dist b2: Bool[1 / 2] .\n"
     678             :     "         P(s1 = 1, b3 = dc14, b2 = b2, s = 7, d = 5)\n"
     679             :     "     + (s1 == 1 && b2 && s == 6 && !(s == 5) && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     680             :     "         flip(b2) .\n"
     681             :     "         dist b2: Bool[1 / 2] .\n"
     682             :     "         P(s1 = 1, b3 = dc15, b2 = b2, s = 7, d = 6)\n"
     683             :     "     + (s1 == 1 && !b2 && s == 6 && !(s == 5) && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
     684             :     "         flip(b2) .\n"
     685             :     "         dist b2: Bool[1 / 2] .\n"
     686             :     "         P(s1 = 1, b3 = dc16, b2 = b2, s = 2, d = 0)\n"
     687             :     "     + (s1 == 1 && s == 7) ->\n"
     688             :     "         dice(d) .\n"
     689             :     "         dist b2: Bool[1 / 2] .\n"
     690             :     "         P(s1 = 1, b3 = dc17, b2 = b2)\n"
     691             :     "     + (s1 == 2 && b3) ->\n"
     692             :     "         flip(b3) .\n"
     693             :     "         dist b2: Bool[1 / 2] .\n"
     694             :     "         P(s1 = 1, b3 = dc18, b2 = b2, s = 1, d = 0)\n"
     695             :     "     + (s1 == 2 && !b3) ->\n"
     696             :     "         flip(b3) .\n"
     697             :     "         dist b2: Bool[1 / 2] .\n"
     698             :     "         P(s1 = 1, b3 = dc19, b2 = b2, s = 2, d = 0)\n"
     699             :     "     + delta;\n"
     700             :     "\n"
     701             :     "init dist b3: Bool[1 / 2] . P(2, b3, dc, dc1, dc2);\n"
     702           2 :   );
     703           1 :   check_lps2lts_specification(spec, 26, 26, 9);
     704           4 : } 

Generated by: LCOV version 1.13