twacube.cc 3.5 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
22
23
24
25
26
27
28
#include "twacube.hh"
#include <iostream>

namespace spot
{
  cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_))
  {
  }
29
  cstate::cstate(unsigned id): id_(id)
30
31
32
  {
  }

33
  unsigned cstate::label()
34
35
36
37
38
39
40
41
42
  {
    return id_;
  }

  transition::transition(transition&& t) noexcept:
  cube_(std::move(t.cube_)), acc_(std::move(t.acc_))
  {  }

  transition::transition(const cube& cube,
43
                         acc_cond::mark_t acc):
44
45
46
    cube_(cube),  acc_(acc)
  { }

47
  twacube::twacube(const std::vector<std::string> aps):
48
49
50
51
52
53
    init_(0U), aps_(aps), cubeset_(aps.size())
  {
  }

  twacube::~twacube()
  {
Etienne Renault's avatar
Etienne Renault committed
54
    const spot::cubeset cs = get_cubeset();
55
    for (unsigned i = 1; i <= theg_.num_edges(); ++i)
56
57
58
59
60
61
62
63
64
65
66
67
68
      cs.release(theg_.edge_data(i).cube_);
  }

  const acc_cond& twacube::acc() const
  {
    return acc_;
  }

  acc_cond& twacube::acc()
  {
    return acc_;
  }

Etienne Renault's avatar
Etienne Renault committed
69
  std::vector<std::string> twacube::ap() const
70
71
72
73
  {
    return aps_;
  }

74
  unsigned twacube::new_state()
75
76
77
78
  {
    return theg_.new_state();
  }

79
  void twacube::set_initial(unsigned init)
80
81
82
83
  {
    init_ = init;
  }

84
  unsigned twacube::get_initial() const
85
86
  {
    if (theg_.num_states() == 0)
87
      throw std::runtime_error("automaton has no state at all");
88
89
90
91

    return init_;
  }

92
  cstate* twacube::state_from_int(unsigned i)
93
94
95
96
97
  {
    return &theg_.state_data(i);
  }

  void
98
99
  twacube::create_transition(unsigned src, const cube& cube,
                             const acc_cond::mark_t& mark, unsigned dst)
100
101
102
103
104
105
106
107
108
109
110
111
112
  {
    theg_.new_edge(src, dst, cube, mark);
  }

  const cubeset&
  twacube::get_cubeset()  const
  {
    return cubeset_;
  }

  bool
  twacube::succ_contiguous() const
  {
113
    unsigned i = 1;
114
115
    while (i <= theg_.num_edges())
      {
116
        unsigned j = i;
117
118
119
120
121
122
123

        // Walk first bucket of successors
        while (j <= theg_.num_edges() &&
               theg_.edge_storage(i).src == theg_.edge_storage(j).src)
          ++j;

        // Remove the next bucket
124
        unsigned itmp = j;
125
126
127
128
129
130
131
132
133

        // Look if there are some transitions missing in this bucket.
        while (j <= theg_.num_edges())
          {
            if (theg_.edge_storage(i).src == theg_.edge_storage(j).src)
              return false;
            ++j;
          }
        i = itmp;
134
135
136
137
138
139
140
141
142
      }
    return true;
  }

  std::ostream&
  operator<<(std::ostream& os, const twacube& twa)
  {
    spot::cubeset cs = twa.get_cubeset();
    os << "init : " << twa.init_ << '\n';
143
     for (unsigned i = 1; i <= twa.theg_.num_edges(); ++i)
144
       os << twa.theg_.edge_storage(i).src << "->"
145
146
147
148
          << twa.theg_.edge_storage(i).dst <<  " : "
          << cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
          << ' ' << twa.theg_.edge_data(i).acc_
          << '\n';
149
150
151
    return os;
  }
}