pbes_explorer.h

Go to the documentation of this file.

// Author(s): Gijs Kant
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
#ifndef MCRL2_PBES_PBES_EXPLORER_H
#define MCRL2_PBES_PBES_EXPLORER_H
 
#define PBES_EXPLORER_VERSION 1
 
#include "mcrl2/pbes/detail/pbes_greybox_interface.h"
#include "mcrl2/pbes/detail/ppg_rewriter.h"
#include "mcrl2/pbes/detail/ppg_traverser.h"
 
using mcrl2::data::data_expression;
using mcrl2::data::variable;
 
namespace mcrl2
{
 
namespace pbes_system
{
 
namespace detail
{
    template <typename MapContainer>
    typename MapContainer::mapped_type map_at(const MapContainer& m, typename MapContainer::key_type key);
} // namespace detail
 
 
 
class lts_type {
  int state_length;
  std::vector<std::string> state_names;
  std::vector<std::string> state_types;
  std::vector<std::string> state_type_list;
  std::map<std::string,int> state_type_index;
  std::vector<int> state_type_no;
  std::vector<std::string> state_label_names;
  std::vector<std::string> state_label_types;
  std::vector<std::string> edge_label_names;
  std::vector<std::string> edge_label_types;
 
public:
  lts_type(int state_length);
 
  ~lts_type();
 
  int get_state_length() const;
 
  std::size_t get_number_of_state_types() const;
 
  const std::vector<std::string>& get_state_names() const;
 
  const std::vector<std::string>& get_state_types() const;
 
  int get_state_type_no(int part) const;
 
  std::string get_state_type_name(int type_no) const;
 
  std::size_t get_number_of_state_labels() const;
 
  const std::vector<std::string>& get_state_labels() const;
 
  const std::vector<std::string>& get_state_label_types() const;
 
  std::size_t get_number_of_edge_labels() const;
 
  const std::vector<std::string>& get_edge_labels() const;
 
  const std::vector<std::string>& get_edge_label_types() const;
 
  void add_state(const std::string& name, const std::string& type);
 
  void add_state_label(const std::string& name, const std::string& type);
 
  void add_edge_label(const std::string& name, const std::string& type);
};
 
 
 
 
class ltsmin_state {
 
friend class lts_info;
friend class explorer;
 
public:
    typedef parity_game_generator::operation_type operation_type;
 
private:
    int priority; // Priority (depends on fixpoint operator and equation order)
    std::string var; // Propositional variable name
    operation_type type; // player or type (And/Or, Abelard/Eloise, Odd/Even)
    std::vector<data_expression> param_values; // List of parameter values
 
protected:
    ltsmin_state(const std::string& varname, const pbes_expression& e);
 
    const std::vector<data_expression>& get_parameter_values() const;
 
    void add_parameter_value(const data_expression&);
 
    pbes_expression to_pbes_expression() const;
 
public:
    ltsmin_state(const std::string& varname);
 
    bool operator<( const ltsmin_state& other ) const;
 
    bool operator==( const ltsmin_state& other ) const;
 
    //int get_priority() const;
 
    std::string get_variable() const;
 
    //operation_type get_type() const;
 
    std::string state_to_string() const;
};
 
 
 
 
class lts_info {
 
friend class ltsmin_state;
friend class explorer;
 
public:
    typedef parity_game_generator::operation_type operation_type;
private:
    pbes& p;
    detail::pbes_greybox_interface* pgg;
    bool reset_option;
    bool always_split_option;
    lts_type type;
    std::map<int,std::vector<bool> > read_matrix;
    std::map<int,std::vector<bool> > write_matrix;
    std::map<int,std::vector<bool> > matrix;
    std::map<std::string,int> param_index;
    std::vector<data_expression> param_default_values;
    int number_of_groups;
    std::vector<pbes_expression> transition_expression;
    std::vector<pbes_expression> transition_expression_plain;
    std::vector<std::string> transition_variable_name;
    std::vector<operation_type> transition_type;
    std::map<std::string, propositional_variable> variables;
    std::map<std::string, operation_type> variable_type;
    std::map<std::string, fixpoint_symbol> variable_symbol;
    std::map<std::string, int> variable_priority;
    std::map<std::string, pbes_expression> variable_expression;
    std::map<std::string, data::variable_list> variable_parameters;
    std::map<std::string, std::vector<std::string> > variable_parameter_signatures;
    std::map<std::string, std::vector<int> > variable_parameter_indices;
    std::map<std::string, std::map<int,int> > variable_parameter_index_positions;
 
    static std::map<variable,std::string> variable_signatures;
 
    int count_variables(const pbes_expression& e);
 
    bool is_pass_through_state(const propositional_variable_instantiation& propvar);
 
    std::vector<pbes_expression> split_expression_and_substitute_variables(const pbes_expression& e, int current_priority, operation_type current_type, std::set<std::string> vars_stack);
 
    void compute_lts_type();
 
    void compute_transition_groups();
 
    void compute_dependency_matrix();
 
protected:
 
    const std::vector<pbes_expression>& get_transition_expressions() const;
 
    const std::map<std::string, propositional_variable>& get_variables() const;
 
    const std::map<std::string, fixpoint_symbol>& get_variable_symbols() const;
 
    const std::map<std::string, data::variable_list>& get_variable_parameters() const;
 
    static bool tf(const pbes_expression& phi);
 
    static std::set<std::string> occ(const pbes_expression& expr);
 
    static std::set<std::string> free(const pbes_expression& expr);
 
    std::set<std::string> used(const pbes_expression& expr);
 
    std::set<std::string> used(const pbes_expression& expr, const std::set<std::string>& L);
 
    std::set<std::string> copied(const pbes_expression& expr);
 
    std::set<std::string> copied(const pbes_expression& expr, const std::set<std::string>& L);
 
    std::set<std::string> changed(const pbes_expression& phi);
 
    std::set<std::string> changed(const pbes_expression& phi, const std::set<std::string>& L);
 
    std::set<std::string> reset(const pbes_expression& phi, const std::set<std::string>& d);
 
    static std::set<std::string> get_param_set(const data::variable_list& params);
 
    static std::vector<std::string> get_param_sequence(const data::variable_list& params);
 
    std::vector<int> get_param_indices(const data::variable_list& params);
 
    std::map<int,int> get_param_index_positions(const data::variable_list& params);
 
    static inline std::string get_param_signature(const variable& param);
 
    const data_expression& get_default_value(int index);
 
    lts_info(pbes& p, detail::pbes_greybox_interface* pgg, bool reset, bool always_split);
 
public:
 
    bool get_reset_option() const;
 
    int get_number_of_groups() const;
 
    const std::vector<std::string>& get_transition_variable_names() const;
 
    const std::vector<operation_type>& get_transition_types() const;
 
    const std::map<std::string, operation_type>& get_variable_types() const;
 
    const std::map<std::string, int>& get_variable_priorities() const;
 
    const std::map<std::string, std::vector<std::string> >& get_variable_parameter_signatures() const;
 
    const std::map<std::string, std::vector<int> >& get_variable_parameter_indices() const;
 
    const std::map<std::string, std::map<int,int> >& get_variable_parameter_index_positions() const;
 
    const lts_type& get_lts_type() const;
 
    const std::map<int,std::vector<bool> >& get_dependency_matrix() const;
 
    const std::map<int,std::vector<bool> >& get_read_matrix() const;
 
    const std::map<int,std::vector<bool> >& get_write_matrix() const;
 
    int get_index(const std::string& signature);
 
    bool is_read_dependent_propvar(int group);
 
    bool is_read_dependent_parameter(int group, int part);
 
    bool is_write_dependent_propvar(int group);
 
    bool is_write_dependent_parameter(int group, int part);
 
    std::string state_to_string(const ltsmin_state& state);
 
    static inline std::string get_param_signature(const std::string& paramname, const std::string& paramtype);
};
 
 
 
 
class explorer {
 
public:
    typedef parity_game_generator::operation_type operation_type;
 
private:
    pbes p;
    lts_info* info;
    std::map<std::string,int> localmap_string2int;
    std::vector<std::string> localmap_int2string;
    std::vector<std::map<data_expression,int> > localmaps_data2int;
    std::vector<std::vector<data_expression> > localmaps_int2data;
 
protected:
    ltsmin_state get_state(const propositional_variable_instantiation& expr) const;
 
    std::string data_to_string(const data::data_expression& e);
 
    data::data_expression string_to_data(const std::string& s);
 
    int get_value_index(int type_no, const data_expression& value);
 
    const data_expression& get_data_value(int type_no, int index);
 
    detail::pbes_greybox_interface* pgg;
 
public:
    explorer(const std::string& filename, const std::string& rewrite_strategy, bool reset_flag, bool always_split_flag);
 
    explorer(const pbes& p_, const std::string& rewrite_strategy, bool reset_flag, bool always_split_flag);
 
    ~explorer();
 
    lts_info* get_info() const;
 
    ltsmin_state get_initial_state() const;
 
    void initial_state(int* state);
 
    static inline ltsmin_state true_state();
 
    static inline ltsmin_state false_state();
 
    int get_index(int type_no, const std::string& s);
 
    int get_string_index(const std::string& s);
 
    void to_state_vector(const ltsmin_state& dst_state, int* dst, const ltsmin_state& src_state, int* const& src);
 
    std::string get_value(int type_no, int index);
 
    const std::string& get_string_value(int index);
 
    ltsmin_state from_state_vector(int* const& src);
 
    std::vector<ltsmin_state> get_successors(const ltsmin_state& state);
 
    template <typename callback>
        void next_state_all(int* const& src, callback& cb)
    {
        int state_length = this->info->get_lts_type().get_state_length();
        ltsmin_state state = this->from_state_vector(src);
        //std::clog << "next_state_all: " << state->to_string() << std::endl;
        std::vector<ltsmin_state> successors = this->get_successors(state);
        // int dst[state_length]; N.B. This is not portable C++
        int* dst = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
        for (auto & successor : successors) {
 
            this->to_state_vector(successor, dst, state, src);
            cb(dst);
            //std::clog << "  succ: " << (*succ)->to_string() << std::endl;
        }
    }
 
    std::vector<ltsmin_state> get_successors(const ltsmin_state& state, int group);
 
    template <typename callback>
        void next_state_long(int* const& src, int group, callback& cb)
    {
        int state_length = this->info->get_lts_type().get_state_length();
        std::string group_varname = info->get_transition_variable_names()[group];
        std::string varname = this->get_string_value(src[0]);
        if (varname==group_varname)
        {
            ltsmin_state state = this->from_state_vector(src);
            std::vector<ltsmin_state> successors = this->get_successors(state, group);
            // int dst[state_length]; N.B. This is not portable C++
            int* dst = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
            for (auto & successor : successors) {
                this->to_state_vector(successor, dst, state, src);
                cb(dst, group);
            }
        }
    }
 
};
 
} // namespace pbes_system
 
} // namespace mcrl2
 
#endif // MCRL2_PBES_PBES_EXPLORER_H