26 #include <spot/twa/fwd.hh>
27 #include <spot/twa/acc.hh>
28 #include <spot/twa/bdddict.hh>
31 #include <unordered_map>
35 #include <spot/misc/casts.hh>
36 #include <spot/misc/hash.hh>
38 #include <spot/misc/trival.hh>
43 typedef std::shared_ptr<twa_run> twa_run_ptr;
46 typedef std::shared_ptr<twa_word> twa_word_ptr;
84 virtual size_t hash()
const = 0;
130 operator()(
const state* left,
const state* right)
const
133 return left->
compare(right) < 0;
153 operator()(
const state* left,
const state* right)
const
156 return 0 == left->
compare(right);
177 operator()(
const state* that)
const
189 typedef std::unordered_set<
const state*,
216 auto p = m.insert(s);
228 auto p = m.insert(s);
239 for (state_set::iterator i = m.begin(); i != m.end();)
243 state_set::iterator old = i++;
260 typedef std::shared_ptr<const state> shared_state;
262 inline void shared_state_deleter(state* s) { s->destroy(); }
280 operator()(shared_state left,
281 shared_state right)
const
284 return left->compare(right.get()) < 0;
308 operator()(shared_state left,
309 shared_state right)
const
312 return 0 == left->compare(right.get());
337 operator()(shared_state that)
const
345 typedef std::unordered_set<shared_state,
537 : aut_(other.aut_), it_(other.it_)
546 return it_->
first() ? it_ :
nullptr;
622 class SPOT_API
twa:
public std::enable_shared_from_this<twa>
625 twa(
const bdd_dict_ptr& d);
678 return {
this, succ_iter(s)};
729 int res = dict_->has_registered_proposition(
ap,
this);
732 aps_.emplace_back(
ap);
733 res = dict_->register_proposition(
ap,
this);
734 bddaps_ &= bdd_ithvar(res);
764 throw std::runtime_error(
"register_aps_from_dict() may not be"
765 " called on an automaton that has already"
766 " registered some AP");
767 auto& m = get_dict()->bdd_map;
768 unsigned s = m.size();
769 for (
unsigned n = 0; n < s; ++n)
770 if (m[n].refs.find(
this) != m[n].refs.end())
772 aps_.emplace_back(m[n].f);
773 bddaps_ &= bdd_ithvar(n);
779 const std::vector<formula>&
ap()
const
812 const const_twa_ptr& t)
const;
892 "by b->intersecting_run(a).")
893 twa_run_ptr intersecting_run(const_twa_ptr other,
894 bool from_other)
const
897 return other->intersecting_run(shared_from_this());
899 return this->intersecting_run(other);
971 for (
auto f: a->ap())
972 this->register_ap(f);
1055 std::vector<formula> aps_;
1061 trival::repr_t state_based_acc:2;
1062 trival::repr_t inherently_weak:2;
1063 trival::repr_t weak:2;
1064 trival::repr_t terminal:2;
1065 trival::repr_t universal:2;
1066 trival::repr_t unambiguous:2;
1067 trival::repr_t stutter_invariant:2;
1068 trival::repr_t very_weak:2;
1069 trival::repr_t semi_deterministic:2;
1081 std::unordered_map<std::string,
1083 std::function<void(
void*)>>> named_prop_;
1085 void* get_named_prop_(std::string s)
const;
1106 void* val, std::function<
void(
void*)> destructor);
1123 template<
typename T>
1126 set_named_prop(s, val,
1127 [](
void *p) noexcept {
delete static_cast<T*
>(p); });
1157 template<
typename T>
1160 if (
void* p = get_named_prop_(s))
1161 return static_cast<T*
>(p);
1178 template<
typename T>
1181 if (
void* p = get_named_prop_(s))
1182 return static_cast<T*
>(p);
1185 set_named_prop(s, tmp);
1198 for (
auto& np: named_prop_)
1199 np.second.second(np.second.first);
1200 named_prop_.clear();
1211 if (num_sets() == 0)
1213 return trival::from_repr_t(is.state_based_acc);
1222 is.state_based_acc = val.val();
1231 return prop_state_acc() && acc().is_buchi();
1244 return trival::from_repr_t(is.inherently_weak);
1256 is.inherently_weak = val.val();
1258 is.very_weak = is.terminal = is.weak = val.val();
1274 return trival::from_repr_t(is.terminal);
1286 is.terminal = val.val();
1288 is.inherently_weak = is.weak = val.val();
1300 return trival::from_repr_t(is.weak);
1313 is.weak = val.val();
1315 is.inherently_weak = val.val();
1317 is.very_weak = is.terminal = val.val();
1330 return trival::from_repr_t(is.very_weak);
1342 is.very_weak = val.val();
1344 is.weak = is.inherently_weak = val.val();
1361 return trival::from_repr_t(is.complete);
1369 is.complete = val.val();
1385 return trival::from_repr_t(is.universal);
1397 is.universal = val.val();
1400 is.unambiguous = is.semi_deterministic = val.val();
1410 void prop_deterministic(
trival val)
1412 prop_universal(val);
1416 trival prop_deterministic()
const
1418 return prop_universal();
1436 return trival::from_repr_t(is.unambiguous);
1447 is.unambiguous = val.val();
1449 is.universal = val.val();
1466 return trival::from_repr_t(is.semi_deterministic);
1477 is.semi_deterministic = val.val();
1479 is.universal = val.val();
1496 return trival::from_repr_t(is.stutter_invariant);
1502 is.stutter_invariant = val.val();
1547 bool inherently_weak;
1554 : state_based(false),
1555 inherently_weak(false),
1556 deterministic(false),
1563 prop_set(
bool state_based,
1564 bool inherently_weak,
1569 : state_based(state_based),
1570 inherently_weak(inherently_weak),
1571 deterministic(deterministic),
1572 improve_det(improve_det),
1574 stutter_inv(stutter_inv)
1581 prop_set(
bool state_based,
1582 bool inherently_weak,
1586 : state_based(state_based),
1587 inherently_weak(inherently_weak),
1588 deterministic(deterministic),
1589 improve_det(improve_det),
1591 stutter_inv(stutter_inv)
1613 return {
true,
true,
true,
true,
true,
true };
1630 prop_state_acc(other->prop_state_acc());
1631 if (p.inherently_weak)
1633 prop_terminal(other->prop_terminal());
1634 prop_weak(other->prop_weak());
1635 prop_very_weak(other->prop_very_weak());
1636 prop_inherently_weak(other->prop_inherently_weak());
1638 if (p.deterministic)
1640 prop_universal(other->prop_universal());
1641 prop_semi_deterministic(other->prop_semi_deterministic());
1642 prop_unambiguous(other->prop_unambiguous());
1644 else if (p.improve_det)
1646 if (other->prop_universal().is_true())
1648 prop_universal(
true);
1652 if (other->prop_semi_deterministic().is_true())
1653 prop_semi_deterministic(
true);
1654 if (other->prop_unambiguous().is_true())
1655 prop_unambiguous(
true);
1659 prop_complete(other->prop_complete());
1661 prop_stutter_invariant(other->prop_stutter_invariant());
1672 prop_state_acc(trival::maybe());
1673 if (!p.inherently_weak)
1675 prop_terminal(trival::maybe());
1676 prop_weak(trival::maybe());
1677 prop_very_weak(trival::maybe());
1678 prop_inherently_weak(trival::maybe());
1680 if (!p.deterministic)
1682 if (!(p.improve_det && prop_universal().is_true()))
1683 prop_universal(trival::maybe());
1684 if (!(p.improve_det && prop_semi_deterministic().is_true()))
1685 prop_semi_deterministic(trival::maybe());
1686 if (!(p.improve_det && prop_unambiguous().is_true()))
1687 prop_unambiguous(trival::maybe());
1690 prop_complete(trival::maybe());
1692 prop_stutter_invariant(trival::maybe());
1704 inline twa_succ_iterable::~twa_succ_iterable()
An acceptance condition.
Definition: acc.hh:62
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1529
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2027
Helper class to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:526
Render state pointers unique via a hash table.
Definition: twa.hh:202
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:226
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:214
Abstract class for states.
Definition: twa.hh:51
virtual size_t hash() const =0
Hash a state.
virtual state * clone() const =0
Duplicate a state.
virtual void destroy() const
Release a state.
Definition: twa.hh:98
virtual ~state()
Destructor.
Definition: twa.hh:110
virtual int compare(const state *other) const =0
Compares two states (that come from the same automaton).
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
Iterate over the successors of a state.
Definition: twa.hh:398
virtual acc_cond::mark_t acc() const =0
Get the acceptance mark of the edge leading to this successor.
virtual const state * dst() const =0
Get the destination state of the current edge.
virtual bool done() const =0
Check whether the iteration is finished.
virtual bool first()=0
Position the iterator on the first successor (if any).
virtual bool next()=0
Jump to the next successor (if any).
virtual bdd cond() const =0
Get the condition on the edge leading to this successor.
A Transition-based ω-Automaton.
Definition: twa.hh:623
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1284
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:963
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:949
virtual twa_run_ptr intersecting_run(const_twa_ptr other) const
Return an accepting run recognizing a word accepted by two automata.
virtual const state * get_init_state() const =0
Get the initial state of the automaton.
void prop_inherently_weak(trival val)
Set the "inherently weak" property.
Definition: twa.hh:1254
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:821
trival prop_universal() const
Whether the automaton is universal.
Definition: twa.hh:1383
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:990
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:1027
void set_generalized_co_buchi(unsigned num)
Set generalized co-Büchi acceptance.
Definition: twa.hh:1007
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1195
void set_named_prop(std::string s, void *val, std::function< void(void *)> destructor)
Declare a named property.
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:629
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1311
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:1158
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1434
T * get_or_set_named_prop(std::string s)
Create or retrieve a named property.
Definition: twa.hh:1179
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1494
void set_named_prop(std::string s, std::nullptr_t)
Erase a named property.
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:785
virtual state * project_state(const state *s, const const_twa_ptr &t) const
Project a state on an automaton.
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:1124
virtual twa_run_ptr accepting_run() const
Return an accepting run if one exists.
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1500
void copy_named_properties_of(const const_twa_ptr &a)
Copy all the named properties of a into this automaton.
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1272
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1209
void set_acceptance(const acc_cond &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:957
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:969
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1242
void prop_semi_deterministic(trival val)
Set the semi-deterministic property.
Definition: twa.hh:1475
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:934
virtual twa_word_ptr exclusive_word(const_twa_ptr other) const
Return a word accepted by exactly one of the two automata.
void prop_complete(trival val)
Set the complete property.
Definition: twa.hh:1367
void prop_unambiguous(trival val)
Set the unambiguous property.
Definition: twa.hh:1445
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:816
virtual twa_succ_iterator * succ_iter(const state *local_state) const =0
Get an iterator over the successors of local_state.
void unregister_ap(int num)
Unregister an atomic proposition.
trival prop_very_weak() const
Whether the automaton is very-weak.
Definition: twa.hh:1328
virtual std::string format_state(const state *s) const =0
Format the state as a string for printing.
acc_cond::mark_t set_co_buchi()
Set co-Büchi acceptance.
Definition: twa.hh:1048
void prop_very_weak(trival val)
Set the very-weak property.
Definition: twa.hh:1340
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1220
trival prop_complete() const
Whether the automaton is complete.
Definition: twa.hh:1359
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:710
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1298
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1229
void prop_universal(trival val)
Set the universal property.
Definition: twa.hh:1395
virtual bool is_empty() const
Check whether the language of the automaton is empty.
static prop_set all()
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1611
void register_aps_from_dict()
Register all atomic propositions that have already been registered by the bdd_dict for this automaton...
Definition: twa.hh:761
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:779
virtual twa_run_ptr exclusive_run(const_twa_ptr other) const
Return an accepting run recognizing a word accepted by exactly one of the two automata.
virtual twa_word_ptr accepting_word() const
Return an accepting word if one exists.
trival prop_semi_deterministic() const
Whether the automaton is semi-deterministic.
Definition: twa.hh:1464
virtual twa_word_ptr intersecting_word(const_twa_ptr other) const
Return a word accepted by two automata.
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:686
int register_ap(std::string ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:739
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:627
virtual bool intersects(const_twa_ptr other) const
Check whether the language of this automaton intersects that of the other automaton.
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:940
internal::twa_succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:676
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:727
Definition: automata.hh:27
void prop_keep(prop_set p)
Keep only a subset of properties of the current automaton.
Definition: twa.hh:1669
std::unordered_set< shared_state, state_shared_ptr_hash, state_shared_ptr_equal > shared_state_set
Unordered set of shared states.
Definition: twa.hh:347
void prop_copy(const const_twa_ptr &other, prop_set p)
Copy the properties of another automaton.
Definition: twa.hh:1627
std::unordered_map< const state *, val, state_ptr_hash, state_ptr_equal > state_map
Unordered map of abstract states.
Definition: twa.hh:197
std::unordered_set< const state *, state_ptr_hash, state_ptr_equal > state_set
Unordered set of abstract states.
Definition: twa.hh:190
twa_graph_ptr complete(const const_twa_ptr &aut)
Clone a twa and complete it.
An acceptance formula.
Definition: acc.hh:479
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:764
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:754
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:746
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:778
An acceptance mark.
Definition: acc.hh:85
Helper structure to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:487
An Equivalence Relation for state*.
Definition: twa.hh:151
Hash Function for state*.
Definition: twa.hh:175
Strict Weak Ordering for state*.
Definition: twa.hh:128
An Equivalence Relation for shared_state (shared_ptr<const state*>).
Definition: twa.hh:306
Hash Function for shared_state (shared_ptr<const state*>).
Definition: twa.hh:335
Strict Weak Ordering for shared_state (shared_ptr<const state*>).
Definition: twa.hh:278