mtdswa.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 <unordered_map>
 
namespace spot
{
  struct SPOT_API mtdswa: public std::enable_shared_from_this<mtdswa>
  {
  public:
    mtdswa(const bdd_dict_ptr& dict) noexcept
      : dict_(dict)
     {
     }
 
    ~mtdswa()
    {
      dict_->unregister_all_my_variables(this);
    }
 
    std::vector<formula> aps;
 
    std::vector<bdd> states;
    std::vector<formula> names;
    std::vector<acc_cond::mark_t> colors;
    acc_cond acc;
 
    // If this map is non-empty, it is used to map terminal values
    // to states while printing the automaton.  Use this only for debugging,
    // other algorithms will ignore it.
    std::unordered_map<int, int> terminal_to_state_map;
    // colors some nodes
    std::unordered_map<int, unsigned> highlight_nodes;
    // for each element (A, B) put state A in cluster B
    std::unordered_map<int, int> highlight_groups;
 
    bdd_dict_ptr get_dict() const
    {
      return dict_;
    }
 
    unsigned num_roots() const
    {
      return states.size();
    }
 
    unsigned num_states() const
    {
      return states.size() + bdd_has_true(states);
    }
 
    std::ostream& print_dot(std::ostream& os, const char* opts = nullptr) const;
 
    twa_graph_ptr as_twa(bool state_based = false,
                         bool labels = true,
                         bool complete = false) const;
 
    void sinks_as_states();
 
    void sinks_as_constants(bool keep_all_states = false);
 
    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<mtdswa> mtdswa_ptr;
  typedef std::shared_ptr<const mtdswa> const_mtdswa_ptr;
 
  SPOT_API mtdswa_ptr dtwa_to_mtdswa(const twa_graph_ptr& aut);
 
  SPOT_API std::vector<int> scc_vector(const mtdswa_ptr& aut);
 
  SPOT_API std::vector<unsigned> loding_weak_ranking(const mtdswa_ptr& aut,
                                                     bool fix = false);
 
  SPOT_API
  mtdswa_ptr minimize_mtdswa(const mtdswa_ptr& dfa);
  SPOT_API
  mtdswa_ptr minimize_mtdswa(const mtdswa_ptr& dfa,
                             const std::vector<unsigned>& initial_partition);
 
  class SPOT_API simple_ltl_translator
  {
  public:
    simple_ltl_translator(const bdd_dict_ptr& dict,
                          bool simplify_terms = true);
 
    mtdswa_ptr ltl_to_mtdswa(formula f, bool fuse_same_bdds);
    mtdswa_ptr ltl_to_mtdswa_synthesis(formula f,
                                       const std::vector<std::string>& outvars,
                                       bool realizability, int debug = -1);
 
    bdd ltl_to_mtbdd(formula f);
    formula leaf_to_formula(int b, int term) const;
 
    formula terminal_to_formula(int t) const;
    int formula_to_int(formula f);
    int formula_propeq_to_int(formula f);
    int formula_to_terminal(formula f);
    bdd formula_to_terminal_bdd(formula f);
    int formula_to_terminal_bdd_as_int(formula f);
    int formula_propeq_to_terminal_bdd_as_int(formula f);
 
    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, int level = 0);
    formula propeq_representative(formula f, bool isacc);
 
    bddExtCache* get_cache()
    {
      return &cache_;
    }
 
    ~simple_ltl_translator();
  private:
    // Pair representing a formula at a given X-nesting level
    struct formula_level_pair
    {
      formula f;
      int level;
 
      bool operator==(const formula_level_pair& other) const
      {
        return f == other.f && level == other.level;
      }
    };
 
    struct formula_level_pair_hash
    {
      std::size_t operator()(const formula_level_pair& p) const
      {
        return p.f.id() ^ (p.level * 0x9e3779b9);
      }
    };
 
    std::unordered_map<formula_level_pair, bdd,
                       formula_level_pair_hash> propositional_equiv_bdd_;
    std::unordered_map<bdd, formula, bdd_hash> propositional_equiv_[2];
 
    std::unordered_map<formula, bdd> formula_to_bdd_;
    std::unordered_map<formula, int> formula_to_int_;
    std::unordered_map<formula, int> propeq_to_int_;
    std::vector<formula> int_to_formula_;
    bdd_dict_ptr dict_;
    bddExtCache cache_;
    bool simplify_terms_;
  };
 
  SPOT_API
  mtdswa_ptr obligation_to_mtdswa(formula f, const bdd_dict_ptr& dict,
                                  bool fuse_same_bdds = true,
                                  bool simplify_terms = true);
 
  SPOT_API
  mtdswa_ptr obligation_synthesis(formula f, const bdd_dict_ptr& dict,
                                  const std::vector<std::string>& outvars,
                                  bool realizability = false,
                                  bool simplify_terms = true,
                                  int debug = -1);
 
  SPOT_API twa_graph_ptr
  mtdswa_strategy_to_mealy(mtdswa_ptr strategy, bool labels = true,
                           bool loop = false);
}