Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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 mcrl2/pbes/lts2pbes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_LTS2PBES_H
      13             : #define MCRL2_PBES_LTS2PBES_H
      14             : 
      15             : #include "mcrl2/modal_formula/count_fixpoints.h"
      16             : #include "mcrl2/pbes/lps2pbes.h"
      17             : #include "mcrl2/pbes/detail/lts2pbes_e.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace pbes_system {
      22             : 
      23             : /// \brief Algorithm for translating a state formula and an untimed specification to a pbes.
      24             : class lts2pbes_algorithm
      25             : {
      26             :   public:
      27             :     typedef lts::lts_lts_t::states_size_type state_type;
      28             :     typedef pbes_system::detail::lts2pbes_lts::edge_list edge_list;
      29             : 
      30             :   protected:
      31             :     const lts::lts_lts_t& lts0;
      32             :     pbes_system::detail::lts2pbes_lts lts1;
      33             :     utilities::progress_meter m_progress_meter;
      34             :     data::set_identifier_generator m_id_generator;
      35             : 
      36             :     template <typename Parameters>
      37           4 :     void run(const state_formulas::state_formula& f, std::vector<pbes_equation>& equations, Parameters& parameters)
      38             :     {
      39           4 :       detail::E_lts2pbes(f, parameters, equations, core::term_traits_optimized<pbes_expression>());
      40           4 :     }
      41             : 
      42             :   public:
      43             :     /// \brief Constructor.
      44           4 :     explicit lts2pbes_algorithm(const lts::lts_lts_t& l)
      45           4 :       : lts0(l), lts1(l)
      46           4 :     {}
      47             : 
      48             :     /// \brief Runs the translation algorithm
      49             :     /// \param formspec A state formula specification.
      50             :     /// \param preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed
      51             :     //                                    for a more compact translation.
      52             :     /// \param generate_counter_example A boolean indicating whether a counterexample must be generated.
      53             :     /// \return The result of the translation
      54           4 :     pbes run(const state_formulas::state_formula_specification& formspec,
      55             :              bool preprocess_modal_operators = false,
      56             :              bool generate_counter_example = false
      57             :             )
      58             :     {
      59             :       // TODO: extract identifiers from the LTS(?)
      60           4 :       std::set<core::identifier_string> lts_ids;
      61           4 :       state_formulas::state_formula f = state_formulas::preprocess_state_formula(formspec.formula(), lts_ids, preprocess_modal_operators);
      62             : 
      63             :       // initialize progress meter
      64           4 :       std::size_t num_fixpoints = state_formulas::count_fixpoints(f);
      65           4 :       std::size_t num_steps = num_fixpoints * lts1.state_count();
      66           4 :       m_progress_meter.set_size(num_steps);
      67           4 :       mCRL2log(log::verbose) << "Generating " << num_steps << " equations." << std::endl;
      68             : 
      69             :       // compute the equations
      70           4 :       std::vector<pbes_equation> equations;
      71           4 :       if (generate_counter_example)
      72             :       {
      73           0 :         detail::lts2pbes_counter_example_parameters parameters(f, lts0, lts1, m_id_generator, m_progress_meter);
      74           0 :         run(f, equations, parameters);
      75           0 :         equations = equations + parameters.equations();
      76           0 :       }
      77             :       else
      78             :       {
      79           4 :         detail::lts2pbes_parameters parameters(f, lts0, lts1, m_id_generator, m_progress_meter);
      80           4 :         run(f, equations, parameters);
      81             :       }
      82             : 
      83             :       // compute the initial state
      84           4 :       state_type s0 = lts0.initial_state();
      85           4 :       core::identifier_string Xs0 = detail::make_identifier(detail::mu_name(f), s0);
      86           4 :       data::data_expression_list e = detail::mu_expressions(f);
      87           4 :       propositional_variable_instantiation init(Xs0, e);
      88             : 
      89           8 :       return pbes(lts0.data(), equations, init);
      90           4 :     }
      91             : };
      92             : 
      93             : /// \brief Translates an LTS and a modal formula into a PBES that represents the corresponding
      94             : /// model checking problem.
      95             : /// \param l A labelled transition system.
      96             : /// \param formspec A modal formula specification.
      97             : /// \param preprocess_modal_operators A boolean indicating that modal operators must be preprocessed.
      98             : /// \param generate_counter_example A boolean indicating that a counter example must be generated.
      99             : inline
     100             : pbes lts2pbes(const lts::lts_lts_t& l, const state_formulas::state_formula_specification& formspec, bool preprocess_modal_operators = false, bool generate_counter_example = false)
     101             : {
     102             :   lts2pbes_algorithm algorithm(l);
     103             :   return algorithm.run(formspec, preprocess_modal_operators, generate_counter_example);
     104             : }
     105             : 
     106             : } // namespace pbes_system
     107             : 
     108             : } // namespace mcrl2
     109             : 
     110             : #endif // MCRL2_PBES_LTS2PBES_H