twacube: move useless unsigned int to unsigned
* spot/twacube/twacube.cc, spot/twacube/twacube.hh: here.
This commit is contained in:
parent
cb343ff02d
commit
b8258ac638
2 changed files with 29 additions and 29 deletions
|
|
@ -25,14 +25,14 @@ namespace spot
|
||||||
cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_))
|
cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_))
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
cstate::cstate(unsigned int id): id_(id)
|
cstate::cstate(unsigned id): id_(id)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
cstate::~cstate()
|
cstate::~cstate()
|
||||||
{ }
|
{ }
|
||||||
|
|
||||||
unsigned int cstate::label()
|
unsigned cstate::label()
|
||||||
{
|
{
|
||||||
return id_;
|
return id_;
|
||||||
}
|
}
|
||||||
|
|
@ -60,7 +60,7 @@ namespace spot
|
||||||
twacube::~twacube()
|
twacube::~twacube()
|
||||||
{
|
{
|
||||||
spot::cubeset cs = get_cubeset();
|
spot::cubeset cs = get_cubeset();
|
||||||
for (unsigned int i = 1; i <= theg_.num_edges(); ++i)
|
for (unsigned i = 1; i <= theg_.num_edges(); ++i)
|
||||||
cs.release(theg_.edge_data(i).cube_);
|
cs.release(theg_.edge_data(i).cube_);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -79,17 +79,17 @@ namespace spot
|
||||||
return aps_;
|
return aps_;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned int twacube::new_state()
|
unsigned twacube::new_state()
|
||||||
{
|
{
|
||||||
return theg_.new_state();
|
return theg_.new_state();
|
||||||
}
|
}
|
||||||
|
|
||||||
void twacube::set_initial(unsigned int init)
|
void twacube::set_initial(unsigned init)
|
||||||
{
|
{
|
||||||
init_ = init;
|
init_ = init;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned int twacube::get_initial()
|
unsigned twacube::get_initial()
|
||||||
{
|
{
|
||||||
if (theg_.num_states() == 0)
|
if (theg_.num_states() == 0)
|
||||||
new_state();
|
new_state();
|
||||||
|
|
@ -97,14 +97,14 @@ namespace spot
|
||||||
return init_;
|
return init_;
|
||||||
}
|
}
|
||||||
|
|
||||||
cstate* twacube::state_from_int(unsigned int i)
|
cstate* twacube::state_from_int(unsigned i)
|
||||||
{
|
{
|
||||||
return &theg_.state_data(i);
|
return &theg_.state_data(i);
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
twacube::create_transition(unsigned int src, const cube& cube,
|
twacube::create_transition(unsigned src, const cube& cube,
|
||||||
const acc_cond::mark_t& mark, unsigned int dst)
|
const acc_cond::mark_t& mark, unsigned dst)
|
||||||
{
|
{
|
||||||
theg_.new_edge(src, dst, cube, mark);
|
theg_.new_edge(src, dst, cube, mark);
|
||||||
}
|
}
|
||||||
|
|
@ -118,10 +118,10 @@ namespace spot
|
||||||
bool
|
bool
|
||||||
twacube::succ_contiguous() const
|
twacube::succ_contiguous() const
|
||||||
{
|
{
|
||||||
unsigned int i = 1;
|
unsigned i = 1;
|
||||||
while (i <= theg_.num_edges())
|
while (i <= theg_.num_edges())
|
||||||
{
|
{
|
||||||
unsigned int j = i;
|
unsigned j = i;
|
||||||
|
|
||||||
// Walk first bucket of successors
|
// Walk first bucket of successors
|
||||||
while (j <= theg_.num_edges() &&
|
while (j <= theg_.num_edges() &&
|
||||||
|
|
@ -129,7 +129,7 @@ namespace spot
|
||||||
++j;
|
++j;
|
||||||
|
|
||||||
// Remove the next bucket
|
// Remove the next bucket
|
||||||
unsigned int itmp = j;
|
unsigned itmp = j;
|
||||||
|
|
||||||
// Look if there are some transitions missing in this bucket.
|
// Look if there are some transitions missing in this bucket.
|
||||||
while (j <= theg_.num_edges())
|
while (j <= theg_.num_edges())
|
||||||
|
|
@ -148,7 +148,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
spot::cubeset cs = twa.get_cubeset();
|
spot::cubeset cs = twa.get_cubeset();
|
||||||
os << "init : " << twa.init_ << '\n';
|
os << "init : " << twa.init_ << '\n';
|
||||||
for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i)
|
for (unsigned i = 1; i <= twa.theg_.num_edges(); ++i)
|
||||||
os << twa.theg_.edge_storage(i).src << "->"
|
os << twa.theg_.edge_storage(i).src << "->"
|
||||||
<< twa.theg_.edge_storage(i).dst << " : "
|
<< twa.theg_.edge_storage(i).dst << " : "
|
||||||
<< cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
|
<< cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
|
||||||
|
|
|
||||||
|
|
@ -36,11 +36,11 @@ namespace spot
|
||||||
cstate() {}
|
cstate() {}
|
||||||
cstate(const cstate& s) = delete;
|
cstate(const cstate& s) = delete;
|
||||||
cstate(cstate&& s) noexcept;
|
cstate(cstate&& s) noexcept;
|
||||||
cstate(unsigned int id);
|
cstate(unsigned id);
|
||||||
virtual ~cstate();
|
virtual ~cstate();
|
||||||
unsigned int label();
|
unsigned label();
|
||||||
private:
|
private:
|
||||||
unsigned int id_;
|
unsigned id_;
|
||||||
};
|
};
|
||||||
|
|
||||||
/// \brief Class for representing a transition.
|
/// \brief Class for representing a transition.
|
||||||
|
|
@ -64,7 +64,7 @@ namespace spot
|
||||||
typedef graph_t::edge_storage_t edge_storage_t;
|
typedef graph_t::edge_storage_t edge_storage_t;
|
||||||
|
|
||||||
trans_index(trans_index& ci) = delete;
|
trans_index(trans_index& ci) = delete;
|
||||||
trans_index(unsigned int state, graph_t& g):
|
trans_index(unsigned state, graph_t& g):
|
||||||
st_(g.state_storage(state))
|
st_(g.state_storage(state))
|
||||||
{
|
{
|
||||||
reset();
|
reset();
|
||||||
|
|
@ -97,7 +97,7 @@ namespace spot
|
||||||
|
|
||||||
/// \brief Returns the current transition according to a specific
|
/// \brief Returns the current transition according to a specific
|
||||||
/// \a seed. The \a seed is traditionnally the thread identifier.
|
/// \a seed. The \a seed is traditionnally the thread identifier.
|
||||||
inline unsigned int current(unsigned int seed = 0) const
|
inline unsigned current(unsigned seed = 0) const
|
||||||
{
|
{
|
||||||
// no-swarming : since twacube are dedicated for parallelism, i.e.
|
// no-swarming : since twacube are dedicated for parallelism, i.e.
|
||||||
// swarming, we expect swarming is activated.
|
// swarming, we expect swarming is activated.
|
||||||
|
|
@ -114,7 +114,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
unsigned int idx_; ///< The current transition
|
unsigned idx_; ///< The current transition
|
||||||
const graph_t::state_storage_t& st_; ///< The underlying states
|
const graph_t::state_storage_t& st_; ///< The underlying states
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
@ -137,23 +137,23 @@ namespace spot
|
||||||
std::vector<std::string> get_ap();
|
std::vector<std::string> get_ap();
|
||||||
|
|
||||||
/// \brief This method creates a new state.
|
/// \brief This method creates a new state.
|
||||||
unsigned int new_state();
|
unsigned new_state();
|
||||||
|
|
||||||
/// \brief Updates the initial state to \a init
|
/// \brief Updates the initial state to \a init
|
||||||
void set_initial(unsigned int init);
|
void set_initial(unsigned init);
|
||||||
|
|
||||||
/// \brief Returns the id of the initial state in the automaton.
|
/// \brief Returns the id of the initial state in the automaton.
|
||||||
unsigned int get_initial();
|
unsigned get_initial();
|
||||||
|
|
||||||
/// \brief Accessor for a state from its id.
|
/// \brief Accessor for a state from its id.
|
||||||
cstate* state_from_int(unsigned int i);
|
cstate* state_from_int(unsigned i);
|
||||||
|
|
||||||
/// \brief create a transition between state \a src and state \a dst,
|
/// \brief create a transition between state \a src and state \a dst,
|
||||||
/// using \a cube as the labelling cube and \a mark as the acceptance mark.
|
/// using \a cube as the labelling cube and \a mark as the acceptance mark.
|
||||||
void create_transition(unsigned int src,
|
void create_transition(unsigned src,
|
||||||
const cube& cube,
|
const cube& cube,
|
||||||
const acc_cond::mark_t& mark,
|
const acc_cond::mark_t& mark,
|
||||||
unsigned int dst);
|
unsigned dst);
|
||||||
|
|
||||||
/// \brief Accessor the cube's manipulator.
|
/// \brief Accessor the cube's manipulator.
|
||||||
const cubeset& get_cubeset() const;
|
const cubeset& get_cubeset() const;
|
||||||
|
|
@ -175,20 +175,20 @@ namespace spot
|
||||||
/// \brief Returns the storage associated to a transition.
|
/// \brief Returns the storage associated to a transition.
|
||||||
const graph_t::edge_storage_t&
|
const graph_t::edge_storage_t&
|
||||||
trans_storage(std::shared_ptr<trans_index> ci,
|
trans_storage(std::shared_ptr<trans_index> ci,
|
||||||
unsigned int seed = 0) const
|
unsigned seed = 0) const
|
||||||
{
|
{
|
||||||
return theg_.edge_storage(ci->current(seed));
|
return theg_.edge_storage(ci->current(seed));
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Returns the data associated to a transition.
|
/// \brief Returns the data associated to a transition.
|
||||||
const transition& trans_data(std::shared_ptr<trans_index> ci,
|
const transition& trans_data(std::shared_ptr<trans_index> ci,
|
||||||
unsigned int seed = 0) const
|
unsigned seed = 0) const
|
||||||
{
|
{
|
||||||
return theg_.edge_data(ci->current(seed));
|
return theg_.edge_data(ci->current(seed));
|
||||||
}
|
}
|
||||||
|
|
||||||
///< \brief Returns the successor of state \a i.
|
///< \brief Returns the successor of state \a i.
|
||||||
std::shared_ptr<trans_index> succ(unsigned int i)
|
std::shared_ptr<trans_index> succ(unsigned i)
|
||||||
{
|
{
|
||||||
return std::make_shared<trans_index>(i, theg_);
|
return std::make_shared<trans_index>(i, theg_);
|
||||||
}
|
}
|
||||||
|
|
@ -196,7 +196,7 @@ namespace spot
|
||||||
friend SPOT_API std::ostream& operator<<(std::ostream& os,
|
friend SPOT_API std::ostream& operator<<(std::ostream& os,
|
||||||
const twacube& twa);
|
const twacube& twa);
|
||||||
private:
|
private:
|
||||||
unsigned int init_; ///< The Id of the initial state
|
unsigned init_; ///< The Id of the initial state
|
||||||
acc_cond acc_; ///< The acceptance contidion
|
acc_cond acc_; ///< The acceptance contidion
|
||||||
const std::vector<std::string> aps_; ///< The name of atomic propositions
|
const std::vector<std::string> aps_; ///< The name of atomic propositions
|
||||||
graph_t theg_; ///< The underlying graph
|
graph_t theg_; ///< The underlying graph
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue