alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: rename as_var() as as_vars()

Browse source 
* spot/twa/twa.hh, spot/twaalgos/stutter.cc: Here.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2016-03-02 16:04:15 +01:00
parent 4f1fad80a4
commit 65726c0f60
3 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -1,6 +1,8 @@
New in spot 1.99.8a (not yet released) New in spot 1.99.8a (not yet released)
Nothing yet. Library:
* twa::ap_var() renamed to twa::ap_vars().
New in spot 1.99.8 (2016-02-18) New in spot 1.99.8 (2016-02-18)

4
spot/twa/twa.hh
View file

@ -740,13 +740,13 @@ namespace spot
/// \brief The vector of atomic propositions registered by this /// \brief The vector of atomic propositions registered by this
/// automaton. /// automaton.
const std::vector<formula>& ap() const const std::vector<formula>& ap() const
{ {
return aps_; return aps_;
} }
/// \brief The set of atomic propositions as a conjunction. /// \brief The set of atomic propositions as a conjunction.
bdd ap_var() const bdd ap_vars() const
{ {
return bddaps_; return bddaps_;
} }

8
spot/twaalgos/stutter.cc
View file

@ -272,13 +272,13 @@ namespace spot
twa_graph_ptr twa_graph_ptr
sl(const twa_graph_ptr& a) sl(const twa_graph_ptr& a)
{ {
return sl(a, a->ap_var()); return sl(a, a->ap_vars());
} }
twa_graph_ptr twa_graph_ptr
sl2(const twa_graph_ptr& a) sl2(const twa_graph_ptr& a)
{ {
return sl2(a, a->ap_var()); return sl2(a, a->ap_vars());
} }
twa_graph_ptr twa_graph_ptr
@ -349,7 +349,7 @@ namespace spot
sl2(twa_graph_ptr&& a, bdd atomic_propositions) sl2(twa_graph_ptr&& a, bdd atomic_propositions)
{ {
if (atomic_propositions == bddfalse) if (atomic_propositions == bddfalse)
atomic_propositions = a->ap_var(); atomic_propositions = a->ap_vars();
unsigned num_states = a->num_states(); unsigned num_states = a->num_states();
unsigned num_edges = a->num_edges(); unsigned num_edges = a->num_edges();
std::vector<bdd> selfloops(num_states, bddfalse); std::vector<bdd> selfloops(num_states, bddfalse);
@ -628,7 +628,7 @@ namespace spot
} }
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
std::move(neg), aut->ap_var()); std::move(neg), aut->ap_vars());
aut->prop_stutter_invariant(is_stut); aut->prop_stutter_invariant(is_stut);
return is_stut; return is_stut;
} }