restriction.hh

Go to the documentation of this file.

// This file is part of Awali.
// Copyright 2016-2022 Sylvain Lombardy, Victor Marsault, Jacques Sakarovitch
//
// Awali is a 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.
//
// This program 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/>.
 
/* @file accessible.hh
 *
 * This files contains static functions computing accessible states.
 */
#ifndef AWALI_ALGOS_RESTRICTION_HH
#define AWALI_ALGOS_RESTRICTION_HH
 
#include <set>
 
#include <awali/sttc/ctx/traits.hh>
#include <awali/sttc/labelset/traits.hh>
 
namespace awali {
  namespace sttc {
    
    namespace internal {
      template<typename LS>
      struct make_labelset_from_letters {
        template<typename SET>
        static LS make(const SET& letters) {
          return LS(letters);
        }
      };
 
      template<typename LS>
      struct make_labelset_from_letters<nullableset<LS>> {
        template<typename SET>
        static nullableset<LS> make(const SET& letters) {
          return nullableset<LS>(LS(letters));
        }
      };
      
    }
 
    template<typename Aut>
    void remove_letters(Aut& aut, const std::set<typename labelset_t_of<Aut>::letter_t>& letters, bool del_unvalid_transitions =true) {
      std::set<typename labelset_t_of<Aut>::letter_t> new_alphabet;
      for(auto l: aut->labelset()->genset())
        new_alphabet.insert(l);
      for(auto l: letters)
        new_alphabet.erase(l);
      context_t_of<Aut> ctx(internal::make_labelset_from_letters<labelset_t_of<Aut>>::make(new_alphabet), *(aut->weightset()));
      aut->ctx_ = ctx;
      if(del_unvalid_transitions) {
        auto labelset = aut->labelset();
        std::list<transition_t> to_erase;
        for(auto tr: aut->transitions())
          if(!labelset->is_valid(aut->label_of(tr)))
            to_erase.emplace_back(tr);
        for(auto tr: to_erase)
          aut->del_transition(tr);
      }
    }
    
        
    template<typename Aut>
    void change_alphabet(Aut& aut, const std::set<typename labelset_t_of<Aut>::letter_t>& letters, bool del_unvalid_transitions =true) {
      context_t_of<Aut> ctx(internal::make_labelset_from_letters<labelset_t_of<Aut>>::make(letters), *(aut->weightset()));
      aut->ctx_ = ctx;
      if(del_unvalid_transitions) {
        auto labelset = aut->labelset();
        std::list<transition_t> to_erase;
        for(auto tr: aut->transitions())
          if(!labelset->is_valid(aut->label_of(tr)))
            to_erase.emplace_back(tr);
        for(auto tr: to_erase)
          aut->del_transition(tr);
      }
    }
 
  }
}//end of ns awali::stc
 
#endif // !AWALI_ALGOS_RESTRICTION_HH