25 #include <spot/twa/fwd.hh>
26 #include <spot/twa/acc.hh>
27 #include <spot/twa/bdddict.hh>
30 #include <unordered_map>
34 #include <spot/misc/casts.hh>
35 #include <spot/misc/hash.hh>
37 #include <spot/misc/trival.hh>
56 virtual int compare(
const state* other)
const = 0;
77 virtual size_t hash()
const = 0;
80 virtual state* clone()
const = 0;
123 operator()(
const state* left,
const state* right)
const
126 return left->
compare(right) < 0;
146 operator()(
const state* left,
const state* right)
const
149 return 0 == left->
compare(right);
170 operator()(
const state* that)
const
182 typedef std::unordered_set<
const state*,
189 using state_map = std::unordered_map<
const state*, val,
209 auto p = m.insert(s);
221 auto p = m.insert(s);
232 for (state_set::iterator i = m.begin(); i != m.end();)
236 state_set::iterator old = i++;
253 typedef std::shared_ptr<const state> shared_state;
255 inline void shared_state_deleter(state* s) { s->destroy(); }
273 operator()(shared_state left,
274 shared_state right)
const
277 return left->compare(right.get()) < 0;
301 operator()(shared_state left,
302 shared_state right)
const
305 return 0 == left->compare(right.get());
330 operator()(shared_state that)
const
338 typedef std::unordered_set<shared_state,
415 virtual bool first() = 0;
427 virtual bool next() = 0;
444 virtual bool done()
const = 0;
460 virtual const state* dst()
const = 0;
464 virtual bdd cond()
const = 0;
577 class SPOT_API
twa:
public std::enable_shared_from_this<twa>
580 twa(
const bdd_dict_ptr& d);
605 : aut_(other.aut_), it_(other.it_)
618 return it_->
first() ? it_ :
nullptr;
635 virtual const state* get_init_state()
const = 0;
645 succ_iter(
const state* local_state)
const = 0;
674 return {
this, succ_iter(s)};
725 int res = dict_->has_registered_proposition(ap,
this);
729 res = dict_->register_proposition(ap,
this);
730 bddaps_ &= bdd_ithvar(res);
744 void unregister_ap(
int num);
760 throw std::runtime_error(
"register_ap_from_dict() may not be"
761 " called on an automaton that has already"
762 " registered some AP");
763 auto& m = get_dict()->bdd_map;
764 unsigned s = m.size();
765 for (
unsigned n = 0; n < s; ++n)
766 if (m[n].refs.find(
this) != m[n].refs.end())
768 aps_.push_back(m[n].f);
769 bddaps_ &= bdd_ithvar(n);
775 const std::vector<formula>&
ap()
const
792 virtual std::string format_state(
const state* s)
const = 0;
807 virtual state* project_state(
const state* s,
808 const const_twa_ptr& t)
const;
824 virtual bool is_empty()
const;
829 void set_num_sets_(
unsigned num)
831 if (num < acc_.num_sets())
836 acc_.add_sets(num - acc_.num_sets());
843 return acc_.num_sets();
849 return acc_.get_acceptance();
859 acc_.set_acceptance(c);
861 prop_state_acc(
true);
868 unsigned num = acc_.num_sets();
870 prop_state_acc(
true);
876 for (
auto f: a->ap())
877 this->register_ap(f);
895 acc_.set_generalized_buchi();
897 prop_state_acc(
true);
917 set_generalized_buchi(1);
922 std::vector<formula> aps_;
928 trival::repr_t state_based_acc:2;
929 trival::repr_t inherently_weak:2;
930 trival::repr_t weak:2;
931 trival::repr_t terminal:2;
932 trival::repr_t deterministic:2;
933 trival::repr_t unambiguous:2;
934 trival::repr_t stutter_invariant:2;
944 std::unordered_map<std::string,
946 std::function<void(void*)>>> named_prop_;
948 void* get_named_prop_(std::string s)
const;
953 void set_named_prop(std::string s,
965 void* val, std::function<
void(
void*)> destructor);
981 set_named_prop(s, val, [](
void *p) {
delete static_cast<T*
>(p); });
999 void* p = get_named_prop_(s);
1002 return static_cast<T*
>(p);
1013 for (
auto& np: named_prop_)
1014 np.second.second(np.second.first);
1015 named_prop_.clear();
1026 return is.state_based_acc;
1035 is.state_based_acc = val.val();
1044 return prop_state_acc() && acc().is_buchi();
1057 return is.inherently_weak;
1069 is.inherently_weak = val.val();
1071 is.terminal = is.weak = val.val();
1097 is.terminal = val.val();
1099 is.inherently_weak = is.weak = val.val();
1124 is.weak = val.val();
1126 is.inherently_weak = val.val();
1128 is.terminal = val.val();
1144 return is.deterministic;
1155 is.deterministic = val.val();
1158 is.unambiguous = val.val();
1176 return is.unambiguous;
1187 is.unambiguous = val.val();
1189 is.deterministic = val.val();
1206 return is.stutter_invariant;
1212 is.stutter_invariant = val.val();
1272 return {
true,
true,
true,
true };
1289 prop_state_acc(other->prop_state_acc());
1292 prop_terminal(other->prop_terminal());
1293 prop_weak(other->prop_weak());
1294 prop_inherently_weak(other->prop_inherently_weak());
1298 prop_deterministic(other->prop_deterministic());
1299 prop_unambiguous(other->prop_unambiguous());
1302 prop_stutter_invariant(other->prop_stutter_invariant());
1313 prop_state_acc(trival::maybe());
1316 prop_terminal(trival::maybe());
1317 prop_weak(trival::maybe());
1318 prop_inherently_weak(trival::maybe());
1322 prop_deterministic(trival::maybe());
1323 prop_unambiguous(trival::maybe());
1326 prop_stutter_invariant(trival::maybe());
virtual ~state()
Destructor.
Definition: twa.hh:103
bool stutter_inv
preserve stutter invariance
Definition: twa.hh:1253
Helper structure to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:479
bool inherently_weak
preserve inherently weak, weak, & terminal
Definition: twa.hh:1251
An Equivalence Relation for state*.
Definition: twa.hh:143
Render state pointers unique via a hash table.
Definition: twa.hh:194
void prop_weak(trival val)
Set the weak property.
Definition: twa.hh:1122
bdd ap_vars() const
The set of atomic propositions as a conjunction.
Definition: twa.hh:781
void prop_inherently_weak(trival val)
Set the "inherently weak" proeprty.
Definition: twa.hh:1067
twa_succ_iterator * iter_cache_
Any iterator returned via release_iter.
Definition: twa.hh:582
bdd_dict_ptr dict_
BDD dictionary used by the automaton.
Definition: twa.hh:584
trival prop_inherently_weak() const
Whether the automaton is inherently weak.
Definition: twa.hh:1055
A Transition-based ω-Automaton.
Definition: twa.hh:577
void prop_stutter_invariant(trival val)
Set the stutter-invariant property.
Definition: twa.hh:1210
acc_cond & acc()
The acceptance condition of the automaton.
Definition: twa.hh:817
Abstract class for states.
Definition: twa.hh:43
Strict Weak Ordering for shared_state (shared_ptr).
Definition: twa.hh:270
trival prop_unambiguous() const
Whether the automaton is unambiguous.
Definition: twa.hh:1174
bool deterministic
preserve deterministic and unambiguous
Definition: twa.hh:1252
trival prop_state_acc() const
Whether the automaton uses state-based acceptance.
Definition: twa.hh:1024
Helper class to iterate over the successor of a state using the on-the-fly interface.
Definition: twa.hh:593
virtual bool next()=0
Jump to the next successor (if any).
succ_iterable succ(const state *s) const
Build an iterable over the successors of s.
Definition: twa.hh:672
void set_generalized_buchi(unsigned num)
Set generalized Büchi acceptance.
Definition: twa.hh:892
void copy_acceptance_of(const const_twa_ptr &a)
Copy the acceptance condition of another TωA.
Definition: twa.hh:865
static prop_set all()
An all-true prop_set.
Definition: twa.hh:1270
virtual bool first()=0
Position the iterator on the first successor (if any).
void set_named_prop(std::string s, T *val)
Declare a named property.
Definition: twa.hh:979
void set_acceptance(unsigned num, const acc_cond::acc_code &c)
Set the acceptance condition of the automaton.
Definition: twa.hh:856
void prop_state_acc(trival val)
Set the state-based-acceptance property.
Definition: twa.hh:1033
virtual void destroy() const
Release a state.
Definition: twa.hh:91
void prop_unambiguous(trival val)
Sets the unambiguous property.
Definition: twa.hh:1185
Hash Function for shared_state (shared_ptr).
Definition: twa.hh:327
Iterate over the successors of a state.
Definition: twa.hh:390
trival prop_stutter_invariant() const
Whether the automaton is stutter-invariant.
Definition: twa.hh:1204
void release_named_properties()
Destroy all named properties.
Definition: twa.hh:1010
void prop_deterministic(trival val)
Set the deterministic property.
Definition: twa.hh:1153
trival prop_terminal() const
Whether the automaton is terminal.
Definition: twa.hh:1083
const acc_cond::acc_code & get_acceptance() const
Acceptance formula used by the automaton.
Definition: twa.hh:847
trival prop_weak() const
Whether the automaton is weak.
Definition: twa.hh:1109
int register_ap(formula ap)
Register an atomic proposition designated by ap.
Definition: twa.hh:723
const state * operator()(const state *s)
Canonicalize state pointer.
Definition: twa.hh:207
void prop_terminal(trival val)
Set the terminal property.
Definition: twa.hh:1095
bool state_based
preserve state-based acceptnace
Definition: twa.hh:1250
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
void release_iter(twa_succ_iterator *i) const
Release an iterator after usage.
Definition: twa.hh:682
A structure for selecting a set of automaton properties to copy.
Definition: twa.hh:1248
const state * is_new(const state *s)
Canonicalize state pointer.
Definition: twa.hh:219
unsigned num_sets() const
Number of acceptance sets used by the automaton.
Definition: twa.hh:841
Hash Function for state*.
Definition: twa.hh:167
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:812
T * get_named_prop(std::string s) const
Retrieve a named property.
Definition: twa.hh:997
void register_aps_from_dict()
Register all atomic propositions that have already be register by the bdd_dict for this automaton...
Definition: twa.hh:757
const std::vector< formula > & ap() const
The vector of atomic propositions registered by this automaton.
Definition: twa.hh:775
void prop_keep(prop_set p)
Keep only a subset of properties of the current automaton.
Definition: twa.hh:1310
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:735
virtual size_t hash() const =0
Hash a state.
trival prop_deterministic() const
Whether the automaton is deterministic.
Definition: twa.hh:1142
void prop_copy(const const_twa_ptr &other, prop_set p)
Copy the properties of another automaton.
Definition: twa.hh:1286
trival is_sba() const
Whether this is a state-based Büchi automaton.
Definition: twa.hh:1042
Strict Weak Ordering for state*.
Definition: twa.hh:120
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: twa.hh:706
acc_cond::mark_t set_buchi()
Set Büchi acceptance.
Definition: twa.hh:915
void copy_ap_of(const const_twa_ptr &a)
Copy the atomic propositions of another TωA.
Definition: twa.hh:874
An Equivalence Relation for shared_state (shared_ptr).
Definition: twa.hh:298