twa.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 <cstddef>
#include <spot/twa/fwd.hh>
#include <spot/twa/acc.hh>
#include <spot/twa/bdddict.hh>
#include <cassert>
#include <memory>
#include <unordered_map>
#include <functional>
#include <array>
#include <vector>
#include <spot/misc/casts.hh>
#include <spot/misc/hash.hh>
#include <spot/tl/formula.hh>
#include <spot/misc/trival.hh>
 
namespace spot
{
  struct twa_run;
  typedef std::shared_ptr<twa_run> twa_run_ptr;
 
  struct twa_word;
  typedef std::shared_ptr<twa_word> twa_word_ptr;
 
  class SPOT_API state
  {
  public:
    virtual int compare(const state* other) const = 0;
 
    virtual size_t hash() const = 0;
 
    virtual state* clone() const = 0;
 
    virtual void destroy() const
    {
      delete this;
    }
 
  protected:
    virtual ~state()
    {
    }
  };
 
  struct state_ptr_less_than
  {
    bool
    operator()(const state* left, const state* right) const
    {
      SPOT_ASSERT(left);
      return left->compare(right) < 0;
    }
  };
 
  struct state_ptr_equal
  {
    bool
    operator()(const state* left, const state* right) const
    {
      SPOT_ASSERT(left);
      return 0 == left->compare(right);
    }
  };
 
  struct state_ptr_hash
  {
    size_t
    operator()(const state* that) const
    {
      SPOT_ASSERT(that);
      return that->hash();
    }
  };
 
  typedef std::unordered_set<const state*,
                             state_ptr_hash, state_ptr_equal> state_set;
 
  template<class val>
  using state_map = std::unordered_map<const state*, val,
                                       state_ptr_hash, state_ptr_equal>;
 
  class SPOT_API state_unicity_table
  {
    state_set m;
  public:
 
    const state* operator()(const state* s)
    {
      auto p = m.insert(s);
      if (!p.second)
        s->destroy();
      return *p.first;
    }
 
    const state* is_new(const state* s)
    {
      auto p = m.insert(s);
      if (!p.second)
        {
          s->destroy();
          return nullptr;
        }
      return *p.first;
    }
 
    ~state_unicity_table()
    {
      for (state_set::iterator i = m.begin(); i != m.end();)
        {
          // Advance the iterator before destroying its key.  This
          // avoids issues with old g++ implementations.
          state_set::iterator old = i++;
          (*old)->destroy();
        }
    }
 
    size_t
    size()
    {
      return m.size();
    }
  };
 
 
 
  // Functions related to shared_ptr.
 
  typedef std::shared_ptr<const state> shared_state;
 
  inline void shared_state_deleter(state* s) { s->destroy(); }
 
  struct state_shared_ptr_less_than
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      SPOT_ASSERT(left);
      return left->compare(right.get()) < 0;
    }
  };
 
  struct state_shared_ptr_equal
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      SPOT_ASSERT(left);
      return 0 == left->compare(right.get());
    }
  };
 
  struct state_shared_ptr_hash
  {
    size_t
    operator()(shared_state that) const
    {
      SPOT_ASSERT(that);
      return that->hash();
    }
  };
 
  typedef std::unordered_set<shared_state,
                             state_shared_ptr_hash,
                             state_shared_ptr_equal> shared_state_set;
 
  class SPOT_API twa_succ_iterator
  {
  public:
    virtual
    ~twa_succ_iterator()
    {
    }
 
 
    virtual bool first() = 0;
 
    virtual bool next() = 0;
 
    virtual bool done() const = 0;
 
 
 
    virtual const state* dst() const = 0;
    virtual bdd cond() const = 0;
    virtual acc_cond::mark_t acc() const = 0;
 
  };
 
  namespace internal
  {
    struct SPOT_API succ_iterator
    {
    protected:
      twa_succ_iterator* it_;
    public:
 
      succ_iterator(twa_succ_iterator* it):
        it_(it)
      {
      }
 
      bool operator==(succ_iterator o) const
      {
        return it_ == o.it_;
      }
 
      bool operator!=(succ_iterator o) const
      {
        return it_ != o.it_;
      }
 
      const twa_succ_iterator* operator*() const
      {
        return it_;
      }
 
      void operator++()
      {
        if (!it_->next())
          it_ = nullptr;
      }
    };
 
#ifndef SWIG
    class twa_succ_iterable
    {
    protected:
      const twa* aut_;
      twa_succ_iterator* it_;
    public:
      twa_succ_iterable(const twa* aut, twa_succ_iterator* it)
        : aut_(aut), it_(it)
      {
      }
 
      twa_succ_iterable(twa_succ_iterable&& other) noexcept
        : aut_(other.aut_), it_(other.it_)
      {
        other.it_ = nullptr;
      }
 
      ~twa_succ_iterable(); // Defined in this file after twa
 
      internal::succ_iterator begin()
      {
        return it_->first() ? it_ : nullptr;
      }
 
      internal::succ_iterator end()
      {
        return nullptr;
      }
    };
#endif // SWIG
  }
 
 
 
  class SPOT_API twa: public std::enable_shared_from_this<twa>
  {
  protected:
    twa(const bdd_dict_ptr& d);
    mutable twa_succ_iterator* iter_cache_;
    bdd_dict_ptr dict_;
  public:
 
    virtual ~twa();
 
    virtual const state* get_init_state() const = 0;
 
    virtual twa_succ_iterator*
    succ_iter(const state* local_state) const = 0;
 
#ifndef SWIG
    internal::twa_succ_iterable
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
 #endif
 
    void release_iter(twa_succ_iterator* i) const
    {
      if (iter_cache_)
        delete i;
      else
        iter_cache_ = i;
    }
 
    bdd_dict_ptr get_dict() const
    {
      return dict_;
    }
 
    int register_ap(formula ap)
    {
      int res = dict_->has_registered_proposition(ap, this);
      if (res < 0)
        {
          aps_.emplace_back(ap);
          res = dict_->register_proposition(ap, this);
          bddaps_ &= bdd_ithvar(res);
        }
      return res;
    }
 
    int register_ap(std::string ap)
    {
      return register_ap(formula::ap(ap));
    }
 
    void unregister_ap(int num);
 
    void register_aps_from_dict()
    {
      if (!aps_.empty())
        throw std::runtime_error("register_aps_from_dict() may not be"
                                 " called on an automaton that has already"
                                 " registered some AP");
      auto& m = get_dict()->bdd_map;
      unsigned s = m.size();
      for (unsigned n = 0; n < s; ++n)
        if (m[n].refs.find(this) != m[n].refs.end())
          {
            aps_.emplace_back(m[n].f);
            bddaps_ &= bdd_ithvar(n);
          }
    }
 
    const std::vector<formula>& ap() const
    {
      return aps_;
    }
 
    bdd ap_vars() const
    {
      return bddaps_;
    }
 
    virtual std::string format_state(const state* s) const = 0;
 
    virtual state* project_state(const state* s,
                                 const const_twa_ptr& t) const;
 
    const acc_cond& acc() const
    {
      return acc_;
    }
 
    acc_cond& acc()
    {
      return acc_;
    }
 
    virtual bool is_empty() const;
 
    virtual twa_run_ptr accepting_run() const;
 
    virtual twa_word_ptr accepting_word() const;
 
    virtual bool intersects(const_twa_ptr other) const;
 
    virtual bool intersects(const_twa_word_ptr w) const;
 
    virtual twa_run_ptr intersecting_run(const_twa_ptr other) const;
 
    // (undocumented)
    //
    // If \a from_other is true, the returned run will be over the
    // \a other automaton.  Otherwise, the run will be over this
    // automaton.
    //
    // This function was deprecated in Spot 2.8.
    SPOT_DEPRECATED("replace a->intersecting_run(b, true) "
                    "by b->intersecting_run(a).")
    twa_run_ptr intersecting_run(const_twa_ptr other,
                                 bool from_other) const
    {
      if (from_other)
        return other->intersecting_run(shared_from_this());
      else
        return this->intersecting_run(other);
    }
 
    virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
 
    virtual twa_run_ptr exclusive_run(const_twa_ptr other) const;
 
    virtual twa_word_ptr exclusive_word(const_twa_ptr other) const;
 
  private:
    acc_cond acc_;
 
  public:
    unsigned num_sets() const
    {
      return acc_.num_sets();
    }
 
    const acc_cond::acc_code& get_acceptance() const
    {
      return acc_.get_acceptance();
    }
 
    void set_acceptance(unsigned num, const acc_cond::acc_code& c)
    {
      acc_ = acc_cond(num, c);
    }
 
    void set_acceptance(const acc_cond& c)
    {
      acc_ = c;
    }
 
    void copy_acceptance_of(const const_twa_ptr& a)
    {
      acc_ = a->acc();
    }
 
    void copy_ap_of(const const_twa_ptr& a)
    {
      for (auto f: a->ap())
        this->register_ap(f);
    }
 
    void copy_named_properties_of(const const_twa_ptr& a);
 
    void set_generalized_buchi(unsigned num)
    {
      acc_ = acc_cond(num, acc_cond::acc_code::generalized_buchi(num));
    }
 
    void set_generalized_co_buchi(unsigned num)
    {
      acc_ = acc_cond(num, acc_cond::acc_code::generalized_co_buchi(num));
    }
 
    acc_cond::mark_t set_buchi()
    {
      acc_ = acc_cond(1, acc_cond::acc_code::buchi());
      return {0};
    }
 
    acc_cond::mark_t set_co_buchi()
    {
      acc_ = acc_cond(1, acc_cond::acc_code::cobuchi());
      return {0};
    }
 
  private:
    std::vector<formula> aps_;
    bdd bddaps_;
 
    struct bprop
    {
      trival::repr_t state_based_acc:2;     // State-based acceptance.
      trival::repr_t inherently_weak:2;     // Inherently Weak automaton.
      trival::repr_t weak:2;                // Weak automaton.
      trival::repr_t terminal:2;            // Terminal automaton.
      trival::repr_t universal:2;           // Universal automaton.
      trival::repr_t unambiguous:2;         // Unambiguous automaton.
      trival::repr_t stutter_invariant:2;   // Stutter invariant language.
      trival::repr_t very_weak:2;           // very-weak, or 1-weak
      trival::repr_t semi_deterministic:2;  // semi-deterministic automaton.
      trival::repr_t complete:2;            // Complete automaton.
    };
    union
    {
      unsigned props;
      bprop is;
    };
 
  protected:
#ifndef SWIG
    // Dynamic properties, are given with a name and a destructor function.
    std::unordered_map<std::string,
                       std::pair<void*,
                                 std::function<void(void*)>>> named_prop_;
#endif
    void* get_named_prop_(std::string s) const;
 
  public:
 
#ifndef SWIG
    void set_named_prop(std::string s,
                        void* val, std::function<void(void*)> destructor);
 
    template<typename T>
    void set_named_prop(std::string s, T* val)
    {
      set_named_prop(s, val,
                     [](void *p) noexcept { delete static_cast<T*>(p); });
    }
 
    void set_named_prop(std::string s, std::nullptr_t);
 
    template<typename T>
    T* get_named_prop(std::string s) const
    {
      if (void* p = get_named_prop_(s))
        return static_cast<T*>(p);
      else
        return nullptr;
    }
 
    template<typename T>
    T* get_or_set_named_prop(std::string s)
    {
      if (void* p = get_named_prop_(s))
        return static_cast<T*>(p);
 
      auto tmp = new T;
      set_named_prop(s, tmp);
      return tmp;
    }
 
#endif
 
    void release_named_properties()
    {
      // Destroy all named properties.
      for (auto& np: named_prop_)
        np.second.second(np.second.first);
      named_prop_.clear();
    }
 
    trival prop_state_acc() const
    {
      if (num_sets() == 0)
        return trival(true);
      return trival::from_repr_t(is.state_based_acc);
    }
 
    void prop_state_acc(trival val)
    {
      is.state_based_acc = val.val();
    }
 
    trival is_sba() const
    {
      return prop_state_acc() && acc().is_buchi();
    }
 
    trival prop_inherently_weak() const
    {
      return trival::from_repr_t(is.inherently_weak);
    }
 
    void prop_inherently_weak(trival val)
    {
      is.inherently_weak = val.val();
      if (!val)
        is.very_weak = is.terminal = is.weak = val.val();
    }
 
    trival prop_terminal() const
    {
      return trival::from_repr_t(is.terminal);
    }
 
    void prop_terminal(trival val)
    {
      is.terminal = val.val();
      if (val)
        is.inherently_weak = is.weak = val.val();
    }
 
    trival prop_weak() const
    {
      return trival::from_repr_t(is.weak);
    }
 
    void prop_weak(trival val)
    {
      is.weak = val.val();
      if (val)
        is.inherently_weak = val.val();
      if (!val)
        is.very_weak = is.terminal = val.val();
    }
 
    trival prop_very_weak() const
    {
      return trival::from_repr_t(is.very_weak);
    }
 
    void prop_very_weak(trival val)
    {
      is.very_weak = val.val();
      if (val)
        is.weak = is.inherently_weak = val.val();
    }
 
 
    trival prop_complete() const
    {
      return trival::from_repr_t(is.complete);
    }
 
    void prop_complete(trival val)
    {
      is.complete = val.val();
    }
 
    trival prop_universal() const
    {
      return trival::from_repr_t(is.universal);
    }
 
    void prop_universal(trival val)
    {
      is.universal = val.val();
      if (val)
        // universal implies unambiguous and semi-deterministic
        is.unambiguous = is.semi_deterministic = val.val();
    }
 
    // Starting with Spot 2.4, an automaton is deterministic if it is
    // both universal and existential, but as we already have
    // twa::is_existential(), we only need to additionally record the
    // universal property.  Before that, the deterministic property
    // was just a synonym for universal, hence we keep the deprecated
    // function prop_deterministic() with this meaning.
    SPOT_DEPRECATED("use prop_universal() instead")
    void prop_deterministic(trival val)
    {
      prop_universal(val);
    }
 
    SPOT_DEPRECATED("use prop_universal() instead")
    trival prop_deterministic() const
    {
      return prop_universal();
    }
 
    trival prop_unambiguous() const
    {
      return trival::from_repr_t(is.unambiguous);
    }
 
    void prop_unambiguous(trival val)
    {
      is.unambiguous = val.val();
      if (!val)
        is.universal = val.val();
    }
 
    trival prop_semi_deterministic() const
    {
      return trival::from_repr_t(is.semi_deterministic);
    }
 
    void prop_semi_deterministic(trival val)
    {
      is.semi_deterministic = val.val();
      if (!val)
        is.universal = val.val();
    }
 
    trival prop_stutter_invariant() const
    {
      return trival::from_repr_t(is.stutter_invariant);
    }
 
    void prop_stutter_invariant(trival val)
    {
      is.stutter_invariant = val.val();
    }
 
    struct prop_set
    {
      bool state_based;     
      bool inherently_weak; 
      bool deterministic;   
      bool improve_det;     
      bool complete;        
      bool stutter_inv;     
 
      prop_set()
      : state_based(false),
        inherently_weak(false),
        deterministic(false),
        improve_det(false),
        complete(false),
        stutter_inv(false)
      {
      }
 
      prop_set(bool state_based,
               bool inherently_weak,
               bool deterministic,
               bool improve_det,
               bool complete,
               bool stutter_inv)
      : state_based(state_based),
        inherently_weak(inherently_weak),
        deterministic(deterministic),
        improve_det(improve_det),
        complete(complete),
        stutter_inv(stutter_inv)
      {
      }
 
#ifndef SWIG
      // The "complete" argument was added in Spot 2.4
      SPOT_DEPRECATED("prop_set() now takes 6 arguments")
      prop_set(bool state_based,
               bool inherently_weak,
               bool deterministic,
               bool improve_det,
               bool stutter_inv)
      : state_based(state_based),
        inherently_weak(inherently_weak),
        deterministic(deterministic),
        improve_det(improve_det),
        complete(false),
        stutter_inv(stutter_inv)
      {
      }
#endif
 
      static prop_set all()
      {
        return { true, true, true, true, true, true };
      }
    };
 
    void prop_copy(const const_twa_ptr& other, prop_set p)
    {
      if (p.state_based)
        prop_state_acc(other->prop_state_acc());
      if (p.inherently_weak)
        {
          prop_terminal(other->prop_terminal());
          prop_weak(other->prop_weak());
          prop_very_weak(other->prop_very_weak());
          prop_inherently_weak(other->prop_inherently_weak());
        }
      if (p.deterministic)
        {
          prop_universal(other->prop_universal());
          prop_semi_deterministic(other->prop_semi_deterministic());
          prop_unambiguous(other->prop_unambiguous());
        }
      else if (p.improve_det)
        {
          if (other->prop_universal().is_true())
            {
              prop_universal(true);
            }
          else
            {
              if (other->prop_semi_deterministic().is_true())
                prop_semi_deterministic(true);
              if (other->prop_unambiguous().is_true())
                prop_unambiguous(true);
            }
        }
      if (p.complete)
        prop_complete(other->prop_complete());
      if (p.stutter_inv)
        prop_stutter_invariant(other->prop_stutter_invariant());
    }
 
    void prop_keep(prop_set p)
    {
      if (!p.state_based)
        prop_state_acc(trival::maybe());
      if (!p.inherently_weak)
        {
          prop_terminal(trival::maybe());
          prop_weak(trival::maybe());
          prop_very_weak(trival::maybe());
          prop_inherently_weak(trival::maybe());
        }
      if (!p.deterministic)
        {
          if (!(p.improve_det && prop_universal().is_true()))
            prop_universal(trival::maybe());
          if (!(p.improve_det && prop_semi_deterministic().is_true()))
            prop_semi_deterministic(trival::maybe());
          if (!(p.improve_det && prop_unambiguous().is_true()))
            prop_unambiguous(trival::maybe());
        }
      if (!p.complete)
        prop_complete(trival::maybe());
      if (!p.stutter_inv)
        prop_stutter_invariant(trival::maybe());
    }
 
    void prop_reset()
    {
      prop_keep({});
    }
  };
 
#ifndef SWIG
  namespace internal
  {
    inline twa_succ_iterable::~twa_succ_iterable()
    {
      if (it_)
        aut_->release_iter(it_);
    }
  }
#endif // SWIG
 
 
 
 
 
 
 
 
 
 
}