ltlf2dfa.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/twa/twagraph.hh>
#include <spot/misc/bddlt.hh>
#include <spot/misc/trival.hh>
#include <spot/twaalgos/backprop.hh>
 
namespace spot
{
 
  struct SPOT_API mtdfa_stats
    {
      unsigned states;
 
      unsigned aps;
 
      unsigned nodes;
 
      unsigned terminals;
 
      bool has_true;
      bool has_false;
 
      unsigned long long paths;
 
      unsigned long long edges;
    };
 
  struct SPOT_API mtdfa: public std::enable_shared_from_this<mtdfa>
  {
    public:
    mtdfa(const bdd_dict_ptr& dict) noexcept
    : dict_(dict)
    {
    }
 
    ~mtdfa()
    {
      dict_->unregister_all_my_variables(this);
    }
 
    std::vector<bdd> states;  
    std::vector<formula> names; 
    std::vector<formula> aps;
 
    unsigned num_roots() const
    {
      return states.size();
    }
 
    unsigned num_states() const
    {
      return states.size() + bdd_has_true(states);
    }
 
    // This assumes that all states are reachable, so we just have to
    // check if one terminal is accepting.
    bool is_empty() const;
 
    std::ostream& print_dot(std::ostream& os,
                            int index = -1,
                            bool labels = true) const;
 
    twa_graph_ptr as_twa(bool state_based = false, bool labels = true) const;
 
    mtdfa_stats get_stats(bool nodes, bool paths) const;
 
    bdd_dict_ptr get_dict() const
    {
      return dict_;
    }
 
    void set_controllable_variables(const std::vector<std::string>& vars,
                                    bool ignore_non_registered_ap = false);
    void set_controllable_variables(bdd vars);
 
    bdd get_controllable_variables() const
    {
      return controllable_variables_;
    }
 
    private:
    bdd_dict_ptr dict_;
    bdd controllable_variables_ = bddtrue;
    };
 
  typedef std::shared_ptr<mtdfa> mtdfa_ptr;
  typedef std::shared_ptr<const mtdfa> const_mtdfa_ptr;
 
  SPOT_API mtdfa_ptr
  ltlf_to_mtdfa(formula f, const bdd_dict_ptr& dict,
                bool fuse_same_bdds = true,
                bool simplify_terms = true,
                bool detect_empty_univ = true,
                bool preserve_quantifiers_in_names = false);
 
 
  enum ltlf_synthesis_backprop {
    state_refine,         
    bfs_node_backprop,    
    dfs_node_backprop,    
  };
 
  struct SPOT_API ltlf_synthesis_options
  {
    bool one_step_preprocess = true;
 
    bool terminating_semantics = true;
 
    bool fuse_same_bdds = true;
 
    bool simplify_terms = true;
 
    bool detect_empty_univ = true;
  };
 
  SPOT_API mtdfa_ptr
  ltlf_to_mtdfa_for_synthesis(formula f, const bdd_dict_ptr& dict,
                              const std::vector<std::string>& outvars,
                              ltlf_synthesis_backprop backprop
                              = dfs_node_backprop,
                              bool realizability = false,
                              ltlf_synthesis_options options = {});
 
  SPOT_API mtdfa_ptr
  ltlf_to_mtdfa_compose(formula f, const bdd_dict_ptr& dict,
                        bool minimize = true, bool order_for_aps = true,
                        bool want_names = true,
                        bool fuse_same_bdds = true,
                        bool simplify_terms = true);
 
  SPOT_API mtdfa_ptr minimize_mtdfa(const mtdfa_ptr& dfa);
 
  SPOT_API mtdfa_ptr product(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
 
  SPOT_API mtdfa_ptr product_or(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
 
  SPOT_API mtdfa_ptr product_xor(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
 
  SPOT_API mtdfa_ptr product_xnor(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
 
  SPOT_API mtdfa_ptr product_implies(const mtdfa_ptr& dfa1,
                                     const mtdfa_ptr& dfa2);
 
  SPOT_API mtdfa_ptr complement(const mtdfa_ptr& dfa);
 
  SPOT_API mtdfa_ptr trim(const mtdfa_ptr& dfa);
 
  SPOT_API mtdfa_ptr quantify_exists(const mtdfa_ptr& dfa, bdd vars,
                                     bool trim = true);
  SPOT_API mtdfa_ptr quantify_exists(const mtdfa_ptr& dfa,
                                     const formula& ap, bool trim = true);
  SPOT_API mtdfa_ptr quantify_exists(const mtdfa_ptr& dfa,
                                     const std::vector<formula>& aps,
                                     bool trim = true);
 
  SPOT_API mtdfa_ptr quantify_forall(const mtdfa_ptr& dfa, bdd vars,
                                     bool trim = true);
  SPOT_API mtdfa_ptr quantify_forall(const mtdfa_ptr& dfa,
                                     const formula& ap, bool trim = true);
  SPOT_API mtdfa_ptr quantify_forall(const mtdfa_ptr& dfa,
                                     const std::vector<formula>& aps,
                                     bool trim = true);
 
  SPOT_API mtdfa_ptr twadfa_to_mtdfa(const twa_graph_ptr& twa);
 
 
  class SPOT_API ltlf_translator
  {
  public:
    ltlf_translator(const bdd_dict_ptr& dict,
                    bool simplify_terms = true);
 
    mtdfa_ptr ltlf_to_mtdfa(formula f, bool fuse_same_bdds,
                            bool detect_empty_univ = true,
                            bool preserve_quantifiers_in_names = false);
 
    mtdfa_ptr ltlf_to_mtdfa_synthesis(formula f, bool fuse_same_bdds,
                                      bool detect_empty_univ = true,
                                      const std::vector<std::string>* outvars
                                      = nullptr,
                                      bool do_backprop = false,
                                      bool realizability = false,
                                      bool one_step_preprocess = false,
                                      bool bfs = true,
                                      bool terminating_semantics = true,
                                      bool preserve_quantifiers_in_names
                                      = false);
 
    bdd ltlf_to_mtbdd(formula f);
    std::pair<formula, bool>  leaf_to_formula(int b, int term) const;
 
    formula terminal_to_formula(int t) const;
    int formula_to_int(formula f);
    int formula_to_terminal(formula f, bool may_stop = false);
    bdd formula_to_terminal_bdd(formula f, bool may_stop = false);
    int formula_to_terminal_bdd_as_int(formula f, bool may_stop = false);
 
    bdd combine_and(bdd left, bdd right);
    bdd combine_or(bdd left, bdd right);
    bdd combine_implies(bdd left, bdd right);
    bdd combine_equiv(bdd left, bdd right);
    bdd combine_xor(bdd left, bdd right);
    bdd combine_not(bdd b);
 
 
    bdd propeq_encode(formula f);
    formula propeq_representative(formula f);
    int formula_propeq_to_int(formula f);
    int formula_propeq_to_terminal_bdd_as_int(formula f, bool may_stop);
    int formula_propeq_to_terminal(formula f, bool may_stop = false);
 
 
    bddExtCache* get_cache()
    {
      return &cache_;
    }
 
    ~ltlf_translator();
  private:
    std::unordered_map<formula, int> formula_to_var_;
    std::unordered_map<formula, bdd> propositional_equiv_bdd_;
    std::unordered_map<bdd, formula, bdd_hash> propositional_equiv_;
    std::unordered_map<formula, int> propeq_to_int_;
 
    std::unordered_map<formula, bdd> formula_to_bdd_;
    std::unordered_map<formula, int> formula_to_int_;
    std::vector<formula> int_to_formula_;
    bdd_dict_ptr dict_;
    bddExtCache cache_;
    bool simplify_terms_;
  };
 
  SPOT_API std::vector<bool>
  mtdfa_winning_region(mtdfa_ptr dfa);
 
  SPOT_API std::vector<bool>
  mtdfa_winning_region_lazy(mtdfa_ptr dfa);
 
  SPOT_API std::vector<trival>
  mtdfa_winning_region_lazy3(mtdfa_ptr dfa);
 
  SPOT_API mtdfa_ptr mtdfa_restrict_as_game(mtdfa_ptr dfa);
  SPOT_API mtdfa_ptr
  mtdfa_restrict_as_game(mtdfa_ptr dfa,
                         const std::vector<bool>& winning_states);
  SPOT_API mtdfa_ptr
  mtdfa_restrict_as_game(mtdfa_ptr dfa,
                         const std::vector<trival>& winning_states);
 
 
  SPOT_API backprop_graph
  mtdfa_to_backprop(mtdfa_ptr dfa, bool early_stop = true,
                    bool preserve_names = false);
 
  SPOT_API mtdfa_ptr
  mtdfa_winning_strategy(mtdfa_ptr dfa, bool backprop_nodes);
 
  SPOT_API twa_graph_ptr
  mtdfa_strategy_to_mealy(mtdfa_ptr strategy, bool labels = true,
                          bool loop = false);
}