convert.cc 6.71 KB
Newer Older
1
// -*- coding: utf-8 -*-
Etienne Renault's avatar
Etienne Renault committed
2 3
// Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
//
// 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/>.

20
#include "config.h"
21
#include <spot/twacube_algos/convert.hh>
22
#include <spot/twaalgos/contains.hh>
23 24 25 26 27
#include <assert.h>

namespace spot
{
  spot::cube satone_to_cube(bdd one, cubeset& cubeset,
28
                            std::unordered_map<int, int>& binder)
29 30 31 32
  {
    auto cube = cubeset.alloc();
    while (one != bddtrue)
      {
33 34 35 36 37 38 39 40 41 42 43 44
        if (bdd_high(one) == bddfalse)
          {
            assert(binder.find(bdd_var(one)) != binder.end());
            cubeset.set_false_var(cube, binder[bdd_var(one)]);
            one = bdd_low(one);
          }
        else
          {
            assert(binder.find(bdd_var(one)) != binder.end());
            cubeset.set_true_var(cube, binder[bdd_var(one)]);
            one = bdd_high(one);
          }
45 46 47 48 49
      }
    return cube;
  }

  bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
50
                  std::unordered_map<int, int>& reverse_binder)
51 52 53 54
  {
    bdd result = bddtrue;
    for (unsigned int i = 0; i < cubeset.size(); ++i)
      {
55 56 57 58 59
        assert(reverse_binder.find(i) != reverse_binder.end());
        if (cubeset.is_false_var(cube, i))
          result &= bdd_nithvar(reverse_binder[i]);
        if (cubeset.is_true_var(cube, i))
          result &= bdd_ithvar(reverse_binder[i]);
60 61 62
      }
    return result;
  }
63

Etienne Renault's avatar
Etienne Renault committed
64
  spot::twacube_ptr twa_to_twacube(const spot::const_twa_graph_ptr aut)
65
  {
66 67 68
    if (aut == nullptr)
      return nullptr;

Etienne Renault's avatar
Etienne Renault committed
69 70 71 72
    // Compute the necessary binder and extract atomic propositions
    std::unordered_map<int, int> ap_binder;
    std::vector<std::string>* aps = extract_aps(aut, ap_binder);

73
    // Declare the twa cube
Etienne Renault's avatar
Etienne Renault committed
74
    auto tg =  spot::make_twacube(*aps);
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95

    // Fix acceptance
    tg->acc() = aut->acc();

    // This binder maps twagraph indexes to twacube ones.
    std::unordered_map<int, int> st_binder;

    // Fill binder and create corresponding states into twacube
    for (unsigned n = 0; n < aut->num_states(); ++n)
      st_binder.insert({n, tg->new_state()});

    // Fix the initial state
    tg->set_initial(st_binder[aut->get_init_state_number()]);

    // Get the cubeset
    auto cs = tg->get_cubeset();

    // Now just build all transitions of this automaton
    // spot::cube cube(aps);
    for (unsigned n = 0; n < aut->num_states(); ++n)
      for (auto& t: aut->out(n))
96 97 98 99 100
        {
          bdd cond = t.cond;

          // Special case for bddfalse
          if (cond == bddfalse)
101 102 103 104
            continue;

          // Split the bdd into multiple transitions
          while (cond != bddfalse)
105
            {
106 107 108 109 110
              bdd one = bdd_satone(cond);
              cond -= one;
              spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
              tg->create_transition(st_binder[n], cube, t.acc,
                                    st_binder[t.dst]);
111 112
            }
        }
113 114
    // Must be contiguous to support swarming.
    assert(tg->succ_contiguous());
Etienne Renault's avatar
Etienne Renault committed
115
    delete aps;
116 117 118 119
    return tg;
  }

  std::vector<std::string>*
Etienne Renault's avatar
Etienne Renault committed
120
  extract_aps(const spot::const_twa_graph_ptr aut,
121
              std::unordered_map<int, int>& ap_binder)
122 123 124 125
  {
    std::vector<std::string>* aps = new std::vector<std::string>();
    for (auto f: aut->ap())
      {
126 127 128 129 130 131
        int size = aps->size();
        if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end())
          {
            aps->push_back(f.ap_name());
            ap_binder.insert({aut->get_dict()->var_map[f], size});
          }
132 133 134
      }
    return aps;
  }
135 136

  spot::twa_graph_ptr
137
  twacube_to_twa(spot::twacube_ptr twacube, spot::bdd_dict_ptr d)
138 139 140 141 142 143
  {
    // Grab necessary variables
    auto& theg = twacube->get_graph();
    spot::cubeset cs = twacube->get_cubeset();

    // Build the resulting graph
144 145
    if (d == nullptr)
      d = spot::make_bdd_dict();
146 147 148 149 150 151 152
    auto res = make_twa_graph(d);

    // Fix the acceptance of the resulting automaton
    res->acc() = twacube->acc();

    // Grep bdd id for each atomic propositions
    std::vector<int> bdds_ref;
Etienne Renault's avatar
Etienne Renault committed
153
    for (auto& ap : twacube->ap())
154 155 156 157 158
      bdds_ref.push_back(res->register_ap(ap));

    // Build all resulting states
    for (unsigned int i = 0; i < theg.num_states(); ++i)
      {
159 160 161
        unsigned st = res->new_state();
        (void) st;
        assert(st == i);
162 163 164 165 166
      }

    // Build all resulting conditions.
    for (unsigned int i = 1; i <= theg.num_edges(); ++i)
      {
167 168 169 170 171 172 173 174 175 176 177 178
        bdd cond = bddtrue;
        for (unsigned j = 0; j < cs.size(); ++j)
          {
            if (cs.is_true_var(theg.edge_data(i).cube_, j))
              cond &= bdd_ithvar(bdds_ref[j]);
            else if (cs.is_false_var(theg.edge_data(i).cube_, j))
              cond &= bdd_nithvar(bdds_ref[j]);
            // otherwise it 's a free variable do nothing
          }

        res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
                      cond, theg.edge_data(i).acc_);
179 180 181 182 183 184 185
      }

    // Fix the initial state
    res->set_init_state(twacube->get_initial());

    return res;
  }
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207

  bool are_equivalent(const spot::twacube_ptr twacube,
                      const spot::const_twa_graph_ptr twa)
  {
    // Compute the necessary binder and extract atomic propositions
    std::unordered_map<int, int> ap_binder;
    std::vector<std::string>* aps_twa = extract_aps(twa, ap_binder);
    std::vector<std::string> aps_twacube = twacube->ap();

    // Comparator to compare two strings in case insensitive manner
    std::function< bool (const std::string&, const std::string&) >
      comparator = [](const std::string& lhs, const std::string& rhs){
                     return lhs.compare(rhs) == 0;
                   };

    // Error. Not working on the same set of aps.
    if (aps_twa->size() != aps_twacube.size() ||
        !std::equal(aps_twa->begin(), aps_twa->end(),
                   aps_twacube.begin(), comparator))
      throw std::runtime_error("are_equivalent: not working on the same "
                               "atomic propositions");

208
    auto res = twacube_to_twa(twacube, twa->get_dict());
209 210 211 212 213

    bool result =  are_equivalent(res, twa);
    delete aps_twa;
    return result;
  }
214
}