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;
63 virtual int compare(
const state* other)
const = 0;
84 virtual size_t hash()
const = 0;
87 virtual state* clone()
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*,
196 using state_map = std::unordered_map<
const state*, val,
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,
422 virtual bool first() = 0;
434 virtual bool next() = 0;
451 virtual bool done()
const = 0;
467 virtual const state* dst()
const = 0;
471 virtual bdd cond()
const = 0;
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);
639 virtual const state* get_init_state()
const = 0;
649 succ_iter(
const state* local_state)
const = 0;
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);
748 void unregister_ap(
int num);
764 throw std::runtime_error(
"register_ap_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 796 virtual std::string format_state(
const state* s)
const = 0;
811 virtual state* project_state(
const state* s,
812 const const_twa_ptr& t)
const;
831 virtual bool is_empty()
const;
845 virtual twa_run_ptr accepting_run()
const;
856 virtual twa_word_ptr accepting_word()
const;
860 virtual bool intersects(const_twa_ptr other)
const;
879 virtual twa_run_ptr intersecting_run(const_twa_ptr other,
880 bool from_other =
false)
const;
889 virtual twa_word_ptr intersecting_word(const_twa_ptr other)
const;
894 void set_num_sets_(
unsigned num)
896 if (num < acc_.num_sets())
901 acc_.add_sets(num - acc_.num_sets());
908 return acc_.num_sets();
914 return acc_.get_acceptance();
924 acc_.set_acceptance(c);
944 for (
auto f: a->ap())
945 this->register_ap(f);
963 acc_.set_generalized_buchi();
981 acc_.set_generalized_co_buchi();
1001 set_generalized_buchi(1);
1002 return acc_.mark(0);
1022 set_generalized_co_buchi(1);
1023 return acc_.mark(0);
1027 std::vector<formula> aps_;
1033 trival::repr_t state_based_acc:2;
1034 trival::repr_t inherently_weak:2;
1035 trival::repr_t weak:2;
1036 trival::repr_t terminal:2;
1037 trival::repr_t universal:2;
1038 trival::repr_t unambiguous:2;
1039 trival::repr_t stutter_invariant:2;
1040 trival::repr_t very_weak:2;
1041 trival::repr_t semi_deterministic:2;
1042 trival::repr_t complete:2;
1052 std::unordered_map<std::string,
1054 std::function<void(void*)>>> named_prop_;
1056 void* get_named_prop_(std::string s)
const;
1061 void set_named_prop(std::string s,
1077 void* val, std::function<
void(
void*)> destructor);
1094 template<
typename T>
1097 set_named_prop(s, val, [](
void *p) {
delete static_cast<T*
>(p); });
1110 void set_named_prop(std::string s, std::nullptr_t);
1127 template<
typename T>
1130 if (
void* p = get_named_prop_(s))
1131 return static_cast<T*
>(p);
1148 template<
typename T>
1151 if (
void* p = get_named_prop_(s))
1152 return static_cast<T*
>(p);
1155 set_named_prop(s, tmp);
1168 for (
auto& np: named_prop_)
1169 np.second.second(np.second.first);
1170 named_prop_.clear();
1181 if (num_sets() == 0)
1183 return is.state_based_acc;
1192 is.state_based_acc = val.val();
1201 return prop_state_acc() && acc().is_buchi();
1214 return is.inherently_weak;
1226 is.inherently_weak = val.val();
1228 is.very_weak = is.terminal = is.weak = val.val();
1256 is.terminal = val.val();
1258 is.inherently_weak = is.weak = val.val();
1283 is.weak = val.val();
1285 is.inherently_weak = val.val();
1287 is.very_weak = is.terminal = val.val();
1300 return is.very_weak;
1312 is.very_weak = val.val();
1314 is.weak = is.inherently_weak = val.val();
1339 is.complete = val.val();
1355 return is.universal;
1367 is.universal = val.val();
1370 is.unambiguous = is.semi_deterministic = val.val();
1379 SPOT_DEPRECATED(
"use prop_universal() instead")
1380 void prop_deterministic(
trival val)
1382 prop_universal(val);
1385 SPOT_DEPRECATED(
"use prop_universal() instead")
1386 trival prop_deterministic()
const 1388 return prop_universal();
1406 return is.unambiguous;
1417 is.unambiguous = val.val();
1419 is.universal = val.val();
1436 return is.semi_deterministic;
1447 is.semi_deterministic = val.val();
1449 is.universal = val.val();
1466 return is.stutter_invariant;
1472 is.stutter_invariant = val.val();
1517 bool inherently_weak;
1524 : state_based(
false),
1525 inherently_weak(
false),
1526 deterministic(
false),
1533 prop_set(
bool state_based,
1534 bool inherently_weak,
1539 : state_based(state_based),
1540 inherently_weak(inherently_weak),
1541 deterministic(deterministic),
1542 improve_det(improve_det),
1544 stutter_inv(stutter_inv)
1550 SPOT_DEPRECATED(
"prop_set() now takes 6 arguments")
1551 prop_set(
bool state_based,
1552 bool inherently_weak,
1556 : state_based(state_based),
1557 inherently_weak(inherently_weak),
1558 deterministic(deterministic),
1559 improve_det(improve_det),
1561 stutter_inv(stutter_inv)
1583 return {
true,
true,
true,
true,
true,
true };
1597 void prop_copy(
const const_twa_ptr& other, prop_set p)
1600 prop_state_acc(other->prop_state_acc());
1601 if (p.inherently_weak)
1603 prop_terminal(other->prop_terminal());
1604 prop_weak(other->prop_weak());
1605 prop_very_weak(other->prop_very_weak());
1606 prop_inherently_weak(other->prop_inherently_weak());
1608 if (p.deterministic)
1610 prop_universal(other->prop_universal());
1611 prop_semi_deterministic(other->prop_semi_deterministic());
1612 prop_unambiguous(other->prop_unambiguous());
1614 else if (p.improve_det)
1616 if (other->prop_universal().is_true())
1618 prop_universal(
true);
1622 if (other->prop_semi_deterministic().is_true())
1623 prop_semi_deterministic(
true);
1624 if (other->prop_unambiguous().is_true())
1625 prop_unambiguous(
true);
1629 prop_complete(other->prop_complete());
1631 prop_stutter_invariant(other->prop_stutter_invariant());
1639 void prop_keep(prop_set p)
1642 prop_state_acc(trival::maybe());
1643 if (!p.inherently_weak)
1645 prop_terminal(trival::maybe());
1646 prop_weak(trival::maybe());
1647 prop_very_weak(trival::maybe());
1648 prop_inherently_weak(trival::maybe());
1650 if (!p.deterministic)
1652 if (!(p.improve_det && prop_universal().is_true()))
1653 prop_universal(trival::maybe());
1654 if (!(p.improve_det && prop_semi_deterministic().is_true()))
1655 prop_semi_deterministic(trival::maybe());
1656 if (!(p.improve_det && prop_unambiguous().is_true()))
1657 prop_unambiguous(trival::maybe());
1660 prop_complete(trival::maybe());
1662 prop_stutter_invariant(trival::maybe());
1670 inline twa_succ_iterable::~twa_succ_iterable()
1673 aut_->release_iter(it_);
Helper class to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:525
virtual ~state()
Destructor.
Definition: twa.hh:110
Definition: automata.hh:26
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1242
Helper structure to iterate over the successors of a state using the on-the-fly interface.
Definition: twa.hh:486
An Equivalence Relation for state*.
Definition: twa.hh:150
Render state pointers unique via a hash table.
Definition: twa.hh:201
internal::twa_succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:676
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1281
void prop_complete(trival val)
Set the complete property.
Definition: twa.hh:1337
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:785
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1268
void prop_inherently_weak(trival val)
Set the "inherently weak" property.
Definition: twa.hh:1224
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:627
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:629
A Transition-based ω-Automaton.
Definition: twa.hh:622
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1470
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:821
Abstract class for states.
Definition: twa.hh:50
Strict Weak Ordering for shared_state (shared_ptr<const state*>).
Definition: twa.hh:277
T * get_or_set_named_prop(std::string s)
Create or retrieve a named property.
Definition: twa.hh:1149
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:710
virtual bool next()=0
Jump to the next successor (if any).
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:960
void set_generalized_co_buchi(unsigned num)
Set generalized co-Büchi acceptance.
Definition: twa.hh:978
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:936
void prop_universal(trival val)
Set the universal property.
Definition: twa.hh:1365
virtual bool first()=0
Position the iterator on the first successor (if any).
void set_acceptance(const acc_cond &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:930
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:912
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:1095
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:779
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:816
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:921
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1190
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1212
void prop_unambiguous(trival val)
Set the unambiguous property.
Definition: twa.hh:1415
Hash Function for shared_state (shared_ptr<const state*>).
Definition: twa.hh:334
Iterate over the successors of a state.
Definition: twa.hh:397
void prop_semi_deterministic(trival val)
Set the semi-deterministic property.
Definition: twa.hh:1445
acc_cond::mark_t set_co_buchi()
Set co-Büchi acceptance.
Definition: twa.hh:1020
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1165
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:727
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:214
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1254
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1464
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:226
Hash Function for state*.
Definition: twa.hh:174
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1179
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1404
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
trival prop_very_weak() const
Whether the automaton is very-weak.
Definition: twa.hh:1298
trival prop_complete() const
Whether the automaton is complete.
Definition: twa.hh:1329
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:686
virtual int compare(const state *other) const =0
Compares two states (that come from the same automaton).
int register_ap(std::string ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:739
trival prop_semi_deterministic() const
Whether the automaton is semi-deterministic.
Definition: twa.hh:1434
virtual size_t hash() const =0
Hash a state.
virtual void destroy() const
Release a state.
Definition: twa.hh:98
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1199
static prop_set all()
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1581
Strict Weak Ordering for state*.
Definition: twa.hh:127
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:906
trival prop_universal() const
Whether the automaton is universal.
Definition: twa.hh:1353
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:999
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:942
void prop_very_weak(trival val)
Set the very-weak property.
Definition: twa.hh:1310
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:1128
An Equivalence Relation for shared_state (shared_ptr<const state*>).
Definition: twa.hh:305