dualize.cc 13 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// 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/>.

#include <spot/misc/minato.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/isdet.hh>

namespace spot
{
  namespace
  {
    class dualizer final
    {
    private:
      // Input automaton
      const const_twa_graph_ptr aut_;
      // State id to bdd variable association
      // [id] == bddtrue means the state will be accepting everything
      // (true state) in the dual automaton.
      // [id] == bddfalse means the state will be rejecting everything
      // (sink) in the dual automaton, which can lead to the removal of
      // the transitions going into that state and therefore to the removal
      // of the state when applying purge_unreachable_states().
      // When [id] != bddtrue/bddfalse, the value correspond to the state
      // bdd variable.
      std::vector<bdd> state_to_var_;
      // bdd variable to state id association
      std::map<int, unsigned> var_to_state_;
      // Acceptance mark to bdd variable association
      std::vector<int> mark_to_var_;
      // bdd variable to acceptance mark association
      std::map<int, unsigned> var_to_mark_;
      // bdd representing all the state variables
      bdd all_states_;
      // bdd representing all the marks variables
      bdd all_marks_;
      // bdd representing states & marks variables
      bdd all_vars_;
      // Id of the true state sink. -1U if none.
      unsigned true_state_;
      // In case the acceptance condition is never unsatisfied, but the
      // automaton is not complete, we do transform the acceptance condition
      // to Büchi, and need to mark all the existing transitions with the
      // proper mark, that will be stored in acc_. 0U if not used.
      acc_cond::mark_t acc_;
      // Whether aut_ has a state accepting all.
      bool has_sink;

      // Any sink state in the input automaton will become a true state in the
      // output. Knowing those allows us to simplify some universal transitions.
      // There could be more than one sink state in the input automaton, and in
      // this case they will be squashed into a single true state in the output
      // automaton.
      void find_sink_states(acc_cond::mark_t& second)
      {
        // Loop over the states and search a state that has no outgoing
        // transitions, or only self-loops labeled by the same non-accepting
        // mark. A similar test is done in complete_here().
        unsigned n = aut_->num_states();
        for (unsigned i = 0; i < n; ++i)
          {
            bool sinkable = true;
            bool first = true;
            acc_cond::mark_t commonacc = second;
            for (auto& t: aut_->out(i))
              {
                if (t.dst != i)
                  {
                    sinkable = false;
                    break;
                  }
                if (first)
                  {
                    commonacc = t.acc;
                    first = false;
                  }
                else if (t.acc != commonacc)
                  {
                    sinkable = false;
                    break;
                  }
              }
            if (sinkable && !aut_->acc().accepting(commonacc))
              {
                second = commonacc;
                state_to_var_[i] = bddtrue;
                true_state_ = i;
                has_sink = true;
              }
          }
      }
      // Any true state in the input automaton will become a sink state in the
      // output. Knowing those allow us to simplify some universal transitions.
      // There could be more than one true state in the input automaton. All
      // true states from the input automaton will be removed in the output
      // and the transitions leading to those states will be removed as well.
      void find_true_states()
      {
        // Loop over the states and search a state that has a self-loop on
        // any letter (bddtrue), with an accepting mark.
        unsigned n = aut_->num_states();
        for (unsigned i = 0; i < n; ++i)
          {
            bool acc_all = false;
            for (auto& t: aut_->out(i))
              {
                if (t.dst == i && t.cond == bddtrue
                               && aut_->acc().accepting(t.acc))
                  {
                    acc_all = true;
                    break;
                  }
              }
            if (acc_all)
              {
                state_to_var_[i] = bddfalse;
                has_sink = true;
              }
          }
      }

      void copy_edges(const twa_graph_ptr &res)
      {
        std::vector<unsigned> st;
        unsigned n = aut_->num_states();
        for (unsigned i = 0; i < n; ++i)
          {
            bdd delta = dualized_transition_function(i);
            bdd ap = bdd_exist(bdd_support(delta), all_vars_);
            bdd letters = bdd_exist(delta, all_vars_);

            while (letters != bddfalse)
              {
                bdd oneletter = bdd_satoneset(letters, ap, bddtrue);
                letters -= oneletter;

                minato_isop isop(delta & oneletter);
                bdd cube;

                while ((cube = isop.next()) != bddfalse)
                  {
                    bdd cond = bdd_exist(cube, all_vars_);
                    bdd dest = bdd_existcomp(cube, all_vars_);

                    st.clear();
                    acc_cond::mark_t m = bdd_to_state(dest, st);
                    if  (st.empty())
                      {
                        st.push_back(true_state_);
                        if (aut_->prop_state_acc())
                          m = aut_->state_acc_sets(i);
                      }
                    res->new_univ_edge(i, st.begin(), st.end(), cond, m);
                  }
              }
          }
      }

      // Handles the dualization of a universal initial transition.
      // In theory the transition would be split into several existential 
      // initial transitions, but since spot does not allow multiple initial 
      // states, we rather use a trick: We add a new initial state, and then
      // copy all exiting transitions from each of the state of the universal
      // initial transition.
      void univ_init(const twa_graph_ptr& res)
      {
        bdd comb = bddfalse;
        outedge_combiner oe(res);
        for (unsigned c : aut_->univ_dests(aut_->get_init_state_number()))
          comb |= oe(c);

        auto s = res->new_state();
        res->set_init_state(s);
        oe.new_dests(s, comb);
      }

      // Allocates the states and marks as variables into the bdd dictionary.
      // Also adds the corresponding mapping, and sets all_states_, all_marks_,
      // and all_vars_ to hold those variables as bdds.
      void allocate_dict_vars(const twa_graph_ptr& res)
      {
        auto dict = aut_->get_dict();

        unsigned numstates = aut_->num_states();
        all_states_ = bddtrue;
        for (unsigned i = 0; i < numstates; ++i)
          {
            int v = dict->register_anonymous_variables(1, this);
            if (state_to_var_[i] != bddtrue)
              state_to_var_[i] = bdd_ithvar(v);
            var_to_state_[v] = i;
            all_states_ &= bdd_ithvar(v);
          }

        unsigned numsets = res->num_sets();
        all_marks_ = bddtrue;
        for (unsigned i = 0; i < numsets; ++i)
          {
            int v = dict->register_anonymous_variables(1, this);
            mark_to_var_.push_back(v);
            var_to_mark_.emplace(v, i);
            all_marks_ &= bdd_ithvar(v);
          }
        all_vars_ = all_states_ & all_marks_;
      }

      // Returns the dualized transition function of any input state as a bdd.
      bdd dualized_transition_function(unsigned state_id)
      {
        if (state_to_var_[state_id] == bddtrue)
          return bddfalse;

        bdd res = bddtrue;
        for (auto& e : aut_->out(state_id))
          {
            bdd dest = bddfalse;
            for (unsigned d : aut_->univ_dests(e))
              dest |= state_to_var_[d];

            bdd mark_bdd = bddtrue;
            acc_cond::mark_t m = acc_ ? acc_ : e.acc;
            for (unsigned s: m.sets())
              mark_bdd &= bdd_ithvar(mark_to_var_[s]);

            res &= bdd_imp(e.cond, mark_bdd & dest);
          }
        return res;
      }

      // Given the bdd representation b of a transition, adds destination states
      // to s, and returns the marks on the transition. s being empty means the 
      // transition goes toward a "forever true" state. s with size one
      // represents an existential transition, while size over one represents 
      // a universal transition.
      acc_cond::mark_t bdd_to_state(bdd b, std::vector<unsigned>& s)
      {
        acc_cond::mark_t m = 0U;
        while (b != bddtrue)
          {
            assert(bdd_low(b) == bddfalse);
            int v = bdd_var(b);
            auto it = var_to_state_.find(v);
            if (it != var_to_state_.end())
              s.push_back(it->second);
            else
              m.set(var_to_mark_[v]);

            b = bdd_high(b);
          }
        return m;
      }

    public:
      dualizer(const const_twa_graph_ptr& aut)
        : aut_(aut),
          state_to_var_(aut_->num_states(), bddfalse),
          true_state_(-1U),
          acc_(0U),
          has_sink(false)
      {
      }

      ~dualizer()
      {
        aut_->get_dict()->unregister_all_my_variables(this);
      }

      twa_graph_ptr run()
      {
        bool cmpl = is_complete(aut_);
        auto um = aut_->acc().unsat_mark();

        auto res = make_twa_graph(aut_->get_dict());
        res->copy_ap_of(aut_);

        if (!um.first && cmpl)
          {
            //Shortcut if dual is false
            res->new_states(1);
            res->new_edge(0, 0, bddtrue, 0U);
            res->set_init_state(0);
            res->set_acceptance(0, acc_cond::acc_code::f());

            res->prop_terminal(true);
            res->prop_complete(true);
            res->prop_universal(true);
            return res;
          }
        if (is_deterministic(aut_))
          {
            res = cleanup_acceptance_here(spot::complete(aut_));
            res->set_acceptance(res->num_sets(),
                                res->get_acceptance().complement());
            // Complementing the acceptance is likely to break the terminal
            // property, but not weakness.  We make a useless call to
            // prop_keep() just so we remember to update it in the future if a
            // new argument is added.
            res->prop_keep({true, true, true, true, true, true});
            res->prop_terminal(trival::maybe());
            return res;
          }

        const_twa_graph_ptr autptr;
        res->new_states(aut_->num_states());
        if (!cmpl)
          {
            if (!um.first)
              {
                acc_ = res->set_buchi();
                autptr = res;
              }
            else
              {
                find_sink_states(um.second);
                autptr = aut_;
              }
            if (true_state_ == -1U)
              true_state_ = res->new_state();
          }
        // This case does not cover cmpl && !um.first
        // Due to previous test shortcutting automatons that accept all words.
        else
          {
            assert(um.first);
            find_sink_states(um.second);
            autptr = aut_;
          }
        if (true_state_ != -1U)
          res->new_edge(true_state_, true_state_, bddtrue, um.second);

        res->set_acceptance(autptr->num_sets(),
                            autptr->get_acceptance().complement());
        allocate_dict_vars(res);
        find_true_states();

        copy_edges(res);

        unsigned init_state = aut_->get_init_state_number();
        if (aut_->is_univ_dest(init_state))
          univ_init(res);
        else
          res->set_init_state(init_state);

        res->merge_edges();
        res->purge_unreachable_states();

        res->prop_copy(aut_, {true, true, false, false, false, true});
        res->prop_terminal(trival::maybe());
        if (!has_sink)
          res->prop_complete(true);

        cleanup_acceptance_here(res);
        return res;
      }
    };
  }

  twa_graph_ptr dualize(const const_twa_graph_ptr& aut)
  {
    dualizer du(aut);
    return du.run();
  }
}