Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep
Automatic mass renaming. * src/dstarparse/dra2ba.cc, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh: Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep.
This commit is contained in:
parent
5301fce3bf
commit
03f78ee85a
3 changed files with 23 additions and 23 deletions
|
|
@ -148,7 +148,7 @@ namespace spot
|
||||||
// could be improved.
|
// could be improved.
|
||||||
{
|
{
|
||||||
state_set keep(sl.begin(), sl.end());
|
state_set keep(sl.begin(), sl.end());
|
||||||
auto masked = build_tgba_mask_keep(dra->aut, keep, sl.front());
|
auto masked = build_twa_mask_keep(dra->aut, keep, sl.front());
|
||||||
if (!nra_to_nba(dra, masked)->is_empty())
|
if (!nra_to_nba(dra, masked)->is_empty())
|
||||||
// This SCC is not DBA-realizable.
|
// This SCC is not DBA-realizable.
|
||||||
return false;
|
return false;
|
||||||
|
|
@ -187,7 +187,7 @@ namespace spot
|
||||||
//std::cerr << "unknown\n";
|
//std::cerr << "unknown\n";
|
||||||
// Build a sub-automaton for just the unknown states,
|
// Build a sub-automaton for just the unknown states,
|
||||||
// starting from any state in the SCC.
|
// starting from any state in the SCC.
|
||||||
auto scc_mask = build_tgba_mask_keep(aut, unknown, *unknown.begin());
|
auto scc_mask = build_twa_mask_keep(aut, unknown, *unknown.begin());
|
||||||
state_list local_final;
|
state_list local_final;
|
||||||
state_list local_nonfinal;
|
state_list local_nonfinal;
|
||||||
bool dbarealizable =
|
bool dbarealizable =
|
||||||
|
|
|
||||||
|
|
@ -84,14 +84,14 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// This is an abstract class. You should inherit from it and
|
/// This is an abstract class. You should inherit from it and
|
||||||
/// supply a wanted() method to specify which states to keep.
|
/// supply a wanted() method to specify which states to keep.
|
||||||
class tgba_mask: public twa_proxy
|
class twa_mask: public twa_proxy
|
||||||
{
|
{
|
||||||
protected:
|
protected:
|
||||||
/// \brief Constructor.
|
/// \brief Constructor.
|
||||||
/// \param masked The automaton to mask
|
/// \param masked The automaton to mask
|
||||||
/// \param init Any state to use as initial state. This state will be
|
/// \param init Any state to use as initial state. This state will be
|
||||||
/// destroyed by the destructor.
|
/// destroyed by the destructor.
|
||||||
tgba_mask(const const_twa_ptr& masked, const state* init = 0):
|
twa_mask(const const_twa_ptr& masked, const state* init = 0):
|
||||||
twa_proxy(masked),
|
twa_proxy(masked),
|
||||||
init_(init)
|
init_(init)
|
||||||
{
|
{
|
||||||
|
|
@ -101,7 +101,7 @@ namespace spot
|
||||||
|
|
||||||
|
|
||||||
public:
|
public:
|
||||||
virtual ~tgba_mask()
|
virtual ~twa_mask()
|
||||||
{
|
{
|
||||||
init_->destroy();
|
init_->destroy();
|
||||||
}
|
}
|
||||||
|
|
@ -146,14 +146,14 @@ namespace spot
|
||||||
const state* init_;
|
const state* init_;
|
||||||
};
|
};
|
||||||
|
|
||||||
class tgba_mask_keep: public tgba_mask
|
class twa_mask_keep: public twa_mask
|
||||||
{
|
{
|
||||||
const state_set& mask_;
|
const state_set& mask_;
|
||||||
public:
|
public:
|
||||||
tgba_mask_keep(const const_twa_ptr& masked,
|
twa_mask_keep(const const_twa_ptr& masked,
|
||||||
const state_set& mask,
|
const state_set& mask,
|
||||||
const state* init)
|
const state* init)
|
||||||
: tgba_mask(masked, init),
|
: twa_mask(masked, init),
|
||||||
mask_(mask)
|
mask_(mask)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -165,14 +165,14 @@ namespace spot
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
class tgba_mask_ignore: public tgba_mask
|
class twa_mask_ignore: public twa_mask
|
||||||
{
|
{
|
||||||
const state_set& mask_;
|
const state_set& mask_;
|
||||||
public:
|
public:
|
||||||
tgba_mask_ignore(const const_twa_ptr& masked,
|
twa_mask_ignore(const const_twa_ptr& masked,
|
||||||
const state_set& mask,
|
const state_set& mask,
|
||||||
const state* init)
|
const state* init)
|
||||||
: tgba_mask(masked, init),
|
: twa_mask(masked, init),
|
||||||
mask_(mask)
|
mask_(mask)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -184,14 +184,14 @@ namespace spot
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
class tgba_mask_acc_ignore: public tgba_mask
|
class twa_mask_acc_ignore: public twa_mask
|
||||||
{
|
{
|
||||||
unsigned mask_;
|
unsigned mask_;
|
||||||
public:
|
public:
|
||||||
tgba_mask_acc_ignore(const const_twa_ptr& masked,
|
twa_mask_acc_ignore(const const_twa_ptr& masked,
|
||||||
unsigned mask,
|
unsigned mask,
|
||||||
const state* init)
|
const state* init)
|
||||||
: tgba_mask(masked, init),
|
: twa_mask(masked, init),
|
||||||
mask_(mask)
|
mask_(mask)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -205,27 +205,27 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
const_twa_ptr
|
const_twa_ptr
|
||||||
build_tgba_mask_keep(const const_twa_ptr& to_mask,
|
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
||||||
const state_set& to_keep,
|
const state_set& to_keep,
|
||||||
const state* init)
|
const state* init)
|
||||||
{
|
{
|
||||||
return std::make_shared<tgba_mask_keep>(to_mask, to_keep, init);
|
return std::make_shared<twa_mask_keep>(to_mask, to_keep, init);
|
||||||
}
|
}
|
||||||
|
|
||||||
const_twa_ptr
|
const_twa_ptr
|
||||||
build_tgba_mask_ignore(const const_twa_ptr& to_mask,
|
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
||||||
const state_set& to_ignore,
|
const state_set& to_ignore,
|
||||||
const state* init)
|
const state* init)
|
||||||
{
|
{
|
||||||
return std::make_shared<tgba_mask_ignore>(to_mask, to_ignore, init);
|
return std::make_shared<twa_mask_ignore>(to_mask, to_ignore, init);
|
||||||
}
|
}
|
||||||
|
|
||||||
const_twa_ptr
|
const_twa_ptr
|
||||||
build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask,
|
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
||||||
unsigned to_ignore,
|
unsigned to_ignore,
|
||||||
const state* init)
|
const state* init)
|
||||||
{
|
{
|
||||||
return std::make_shared<tgba_mask_acc_ignore>(to_mask, to_ignore, init);
|
return std::make_shared<twa_mask_acc_ignore>(to_mask, to_ignore, init);
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -32,7 +32,7 @@ namespace spot
|
||||||
/// states from \a to_keep. The initial state
|
/// states from \a to_keep. The initial state
|
||||||
/// can optionally be reset to \a init.
|
/// can optionally be reset to \a init.
|
||||||
SPOT_API const_twa_ptr
|
SPOT_API const_twa_ptr
|
||||||
build_tgba_mask_keep(const const_twa_ptr& to_mask,
|
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
||||||
const state_set& to_keep,
|
const state_set& to_keep,
|
||||||
const state* init = 0);
|
const state* init = 0);
|
||||||
|
|
||||||
|
|
@ -43,7 +43,7 @@ namespace spot
|
||||||
/// in \a to_ignore. The initial state can optionally be reset to
|
/// in \a to_ignore. The initial state can optionally be reset to
|
||||||
/// \a init.
|
/// \a init.
|
||||||
SPOT_API const_twa_ptr
|
SPOT_API const_twa_ptr
|
||||||
build_tgba_mask_ignore(const const_twa_ptr& to_mask,
|
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
||||||
const state_set& to_ignore,
|
const state_set& to_ignore,
|
||||||
const state* init = 0);
|
const state* init = 0);
|
||||||
|
|
||||||
|
|
@ -60,7 +60,7 @@ namespace spot
|
||||||
/// function is only needed in graph algorithms that do not call
|
/// function is only needed in graph algorithms that do not call
|
||||||
/// all_acceptance_conditions().
|
/// all_acceptance_conditions().
|
||||||
SPOT_API const_twa_ptr
|
SPOT_API const_twa_ptr
|
||||||
build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask,
|
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
||||||
unsigned to_ignore,
|
unsigned to_ignore,
|
||||||
const state* init = 0);
|
const state* init = 0);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue