Skip to content

Commit

Permalink
s/spot::acc_cond::mark_t::value_t/acc_mark/
Browse files Browse the repository at this point in the history 
which is an alias to unsigned

Temporarily solves issue #2 until we rewrite
the entire code to support mark_t interfaces.
  • Loading branch information
Juraj Major committed May 24, 2018
1 parent 49141a6 commit 571ed2c
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 39 deletions.
4 changes: 2 additions & 2 deletions alternating.cpp
View file
Expand Up @@ -161,7 +161,7 @@ unsigned make_alternating_recursive(SLAA* slaa, spot::formula f) {
// φ is U subformula
// copy each edge for φ
// each edge that is not a loop gets an Inf mark
spot::acc_cond::mark_t::value_t inf = slaa->acc[phi].inf;
acc_mark inf = slaa->acc[phi].inf;

for (auto& edge_id : slaa->get_state_edges(phi_state)) {
auto edge = slaa->get_edge(edge_id);
Expand Down Expand Up @@ -299,7 +299,7 @@ unsigned make_alternating_recursive(SLAA* slaa, spot::formula f) {
mark = ac.add_sets(f_dnf_size);
// now we have marks in range mark .. mark + f_dnf_size - 1
// each set of edges gets all but its number
for (spot::acc_cond::mark_t::value_t i = mark; i < mark + f_dnf_size; ++i) {
for (acc_mark i = mark; i < mark + f_dnf_size; ++i) {
slaa->acc[f].fin_disj.insert(i);
}
}
Expand Down
34 changes: 17 additions & 17 deletions automaton.cpp
View file
Expand Up @@ -86,7 +86,7 @@ template<typename T> unsigned Automaton<T>::create_edge(bdd label) {
return edges.size() - 1;
}

template<typename T> void Automaton<T>::add_edge(unsigned from, bdd label, std::set<unsigned> to, std::set<spot::acc_cond::mark_t::value_t> marks) {
template<typename T> void Automaton<T>::add_edge(unsigned from, bdd label, std::set<unsigned> to, std::set<acc_mark> marks) {
if (label == bddfalse) {
return;
}
Expand Down Expand Up @@ -193,15 +193,15 @@ template<typename T> void Automaton<T>::remove_edge(unsigned state_id, unsigned
state_edges[state_id].erase(edge_id);
}

template<typename T> std::set<spot::acc_cond::mark_t::value_t> Automaton<T>::get_inf_marks() const {
template<typename T> std::set<acc_mark> Automaton<T>::get_inf_marks() const {
return inf_marks;
}

template<typename T> void Automaton<T>::remember_inf_mark(spot::acc_cond::mark_t::value_t mark) {
template<typename T> void Automaton<T>::remember_inf_mark(acc_mark mark) {
inf_marks.insert(mark);
}

template<typename T> void Automaton<T>::remember_inf_mark(std::set<spot::acc_cond::mark_t::value_t> marks) {
template<typename T> void Automaton<T>::remember_inf_mark(std::set<acc_mark> marks) {
inf_marks.insert(marks.begin(), marks.end());
}

Expand Down Expand Up @@ -388,10 +388,10 @@ void SLAA::remove_unnecessary_marks() {
}
}

SLAA::ac_representation SLAA::mark_transformation(std::map<spot::acc_cond::mark_t::value_t, unsigned>& tgba_mark_owners) {
SLAA::ac_representation SLAA::mark_transformation(std::map<acc_mark, unsigned>& tgba_mark_owners) {
// get a set of all Inf marks; also remember marks having escaping Inf
std::map<spot::acc_cond::mark_t::value_t, bool> inf_marks;
std::map<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t> orig_sibling_of;
std::map<acc_mark, bool> inf_marks;
std::map<acc_mark, acc_mark> orig_sibling_of;
for (auto& ac : acc) {
if (ac.second.inf != -1U) {
inf_marks[ac.second.inf] = true;
Expand All @@ -404,18 +404,18 @@ SLAA::ac_representation SLAA::mark_transformation(std::map<spot::acc_cond::mark_
}

// map of escaping marks
std::map<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t> sibling_of;
std::map<acc_mark, acc_mark> sibling_of;

// this maps each old mark to map { state => 'new mark for this state' }
std::map<spot::acc_cond::mark_t::value_t, std::map<unsigned, spot::acc_cond::mark_t::value_t>> mark_owners;
std::map<acc_mark, std::map<unsigned, acc_mark>> mark_owners;

for (unsigned state_id = 0, states_count = states.size(); state_id < states_count; ++state_id) {
std::map<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t> marks_to_escape;
std::map<acc_mark, acc_mark> marks_to_escape;

for (auto& edge_id : state_edges[state_id]) {
auto edge = get_edge(edge_id);

std::set<spot::acc_cond::mark_t::value_t> new_edge_marks;
std::set<acc_mark> new_edge_marks;
for (auto& mark : edge->get_marks()) {

// is this the first time we see this mark?
Expand Down Expand Up @@ -511,11 +511,11 @@ SLAA::ac_representation SLAA::mark_transformation(std::map<spot::acc_cond::mark_
// iterate through original acc_phi structures
for (auto& ac : acc) {
// these are 2 conjuncts for AC
std::set<std::set<std::pair<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t>>> fin_xs_disj;
std::set<std::set<std::pair<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t>>> fin_ys_disj;
std::set<std::set<std::pair<acc_mark, acc_mark>>> fin_xs_disj;
std::set<std::set<std::pair<acc_mark, acc_mark>>> fin_ys_disj;

// Fin(x) -> (Fin(x_s1) & ... & Fin(x_sn)) plus their escaping Infs
std::set<std::pair<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t>> fin_xs;
std::set<std::pair<acc_mark, acc_mark>> fin_xs;

for (auto& state_mark : mark_owners[ac.second.fin]) {
fin_xs.insert(std::make_pair(state_mark.second, sibling_of[state_mark.second]));
Expand All @@ -528,7 +528,7 @@ SLAA::ac_representation SLAA::mark_transformation(std::map<spot::acc_cond::mark_

for (auto& y : ac.second.fin_disj) {
// Fin(y_i1) & ... & Fin(y_ij)
std::set<std::pair<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t>> fin_ys;
std::set<std::pair<acc_mark, acc_mark>> fin_ys;

for (auto& state_mark : mark_owners[y]) {
fin_ys.insert(std::make_pair(state_mark.second, sibling_of[state_mark.second]));
Expand Down Expand Up @@ -1029,7 +1029,7 @@ std::set<unsigned> Edge::get_marks() const {
// else returns 2
// else returns 0
// where edge 1 is this edge and edge 2 is the other edge
int Edge::dominates(Edge* other, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const {
int Edge::dominates(Edge* other, std::set<acc_mark> inf_marks) const {
auto o1 = get_targets();
auto j1 = get_marks();

Expand Down Expand Up @@ -1064,7 +1064,7 @@ int Edge::dominates(Edge* other, std::set<spot::acc_cond::mark_t::value_t> inf_m
}
}

int Edge::dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const {
int Edge::dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<acc_mark> inf_marks) const {
// t1 kills t2 if O1 ⊆ O2 & a2 => a1
auto j1 = get_marks();
auto j2 = other->get_marks();
Expand Down
28 changes: 15 additions & 13 deletions automaton.hpp
View file
Expand Up @@ -39,13 +39,15 @@
#include <spot/twaalgos/sccfilter.hh>
#include "utils.hpp"

typedef unsigned acc_mark;

class Edge {
protected:
// target set of the edge
std::set<unsigned> targets;

// the acceptance label
std::set<spot::acc_cond::mark_t::value_t> marks;
std::set<acc_mark> marks;

// the transition labels in BDD
bdd label;
Expand Down Expand Up @@ -84,8 +86,8 @@ class Edge {
// sets the transition label
void set_label(bdd l);

int dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const;
int dominates(Edge* other, std::set<spot::acc_cond::mark_t::value_t> inf_marks) const;
int dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<acc_mark> inf_marks) const;
int dominates(Edge* other, std::set<acc_mark> inf_marks) const;
};

template<typename T> class Automaton {
Expand All @@ -102,7 +104,7 @@ template<typename T> class Automaton {
std::vector<std::set<unsigned>>* spot_id_to_slaa_set = nullptr; // this has to be nullptr for SLAA

// a set of Inf-marks used in the automaton
std::set<spot::acc_cond::mark_t::value_t> inf_marks;
std::set<acc_mark> inf_marks;

// the set of initial configurations
std::set<std::set<unsigned>> init_sets;
Expand All @@ -124,7 +126,7 @@ template<typename T> class Automaton {
unsigned create_edge(bdd label);

// creates an edge with given source state, labels and target set
void add_edge(unsigned from, bdd label, std::set<unsigned> to, std::set<spot::acc_cond::mark_t::value_t> marks = std::set<spot::acc_cond::mark_t::value_t>());
void add_edge(unsigned from, bdd label, std::set<unsigned> to, std::set<acc_mark> marks = std::set<acc_mark>());

// copies the given edge to the source `from'
void add_edge(unsigned from, unsigned edge_id);
Expand All @@ -142,11 +144,11 @@ template<typename T> class Automaton {
std::set<unsigned> get_state_edges(unsigned state_id) const;

// returns the registered Inf-marks
std::set<spot::acc_cond::mark_t::value_t> get_inf_marks() const;
std::set<acc_mark> get_inf_marks() const;

// registers the marks in the set `inf_marks'
void remember_inf_mark(spot::acc_cond::mark_t::value_t mark);
void remember_inf_mark(std::set<spot::acc_cond::mark_t::value_t> marks);
void remember_inf_mark(acc_mark mark);
void remember_inf_mark(std::set<acc_mark> marks);

// removes states unreachable from the initial states
void remove_unreachable_states();
Expand All @@ -173,13 +175,13 @@ class SLAA : public Automaton<spot::formula> {
// the condition changes to (...) | Inf(z)
// this z is stored in inf
typedef struct {
spot::acc_cond::mark_t::value_t fin;
spot::acc_cond::mark_t::value_t inf;
std::set<spot::acc_cond::mark_t::value_t> fin_disj;
acc_mark fin;
acc_mark inf;
std::set<acc_mark> fin_disj;
} acc_phi;

// the set representation of resultant acceptance condition
typedef std::set<std::set<std::set<std::pair<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t>>>> ac_representation;
typedef std::set<std::set<std::set<std::pair<acc_mark, acc_mark>>>> ac_representation;

// Spot structures
spot::twa_graph_ptr spot_aut;
Expand All @@ -206,7 +208,7 @@ class SLAA : public Automaton<spot::formula> {
// converts the automaton to single-owner
// the output argument tgba_mark_owners contains pairs of mark j and its owner q
// such that all loops over q contain j as the only mark
ac_representation mark_transformation(std::map<spot::acc_cond::mark_t::value_t, unsigned>& tgba_mark_owners);
ac_representation mark_transformation(std::map<acc_mark, unsigned>& tgba_mark_owners);

// prints the automaton in HOA format
void print_hoaf();
Expand Down
14 changes: 7 additions & 7 deletions nondeterministic.cpp
View file
Expand Up @@ -74,7 +74,7 @@ spot::twa_graph_ptr make_nondeterministic(SLAA* slaa) {

// a map { mark => SLAA state } of Fin-marks removed from NA
// filled only if -t flag is active
std::map<spot::acc_cond::mark_t::value_t, unsigned> tgba_mark_owners;
std::map<acc_mark, unsigned> tgba_mark_owners;
// acr is a representation of the final acceptance condition
auto acr = slaa->mark_transformation(tgba_mark_owners);

Expand All @@ -100,10 +100,10 @@ spot::twa_graph_ptr make_nondeterministic(SLAA* slaa) {
}

// map { mark => set of owner SLAA states } of Fin-marks removed from NA
std::map<spot::acc_cond::mark_t::value_t, std::set<unsigned>> removed_fin_marks;
std::map<acc_mark, std::set<unsigned>> removed_fin_marks;

// map { mark => mark } of the siblings of removed Fin-marks
std::map<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t> sibling_of_removed_fin;
std::map<acc_mark, acc_mark> sibling_of_removed_fin;
for (auto& disj : acr) {
auto disj_f = spot::acc_cond::acc_code::f();

Expand Down Expand Up @@ -259,7 +259,7 @@ spot::twa_graph_ptr make_nondeterministic(SLAA* slaa) {
nha->remove_unreachable_states();

// count all used marks to remove the unused ones
std::set<spot::acc_cond::mark_t::value_t> used_marks;
std::set<acc_mark> used_marks;

for (unsigned st_id = 0, st_count = nha->states_count(); st_id < st_count; ++st_id) {
for (auto& edge_id : nha->get_state_edges(st_id)) {
Expand All @@ -269,8 +269,8 @@ spot::twa_graph_ptr make_nondeterministic(SLAA* slaa) {
}

// create a conversion table { old mark => new mark }
std::map<spot::acc_cond::mark_t::value_t, spot::acc_cond::mark_t::value_t> mark_conversion;
spot::acc_cond::mark_t::value_t mark_counter = 0;
std::map<acc_mark, acc_mark> mark_conversion;
acc_mark mark_counter = 0;
for (auto old_mark : used_marks) {
mark_conversion[old_mark] = mark_counter;
++mark_counter;
Expand Down Expand Up @@ -330,7 +330,7 @@ spot::twa_graph_ptr make_nondeterministic(SLAA* slaa) {
auto label = edge->get_label();
auto marks = edge->get_marks();

std::set<spot::acc_cond::mark_t::value_t> marks_relabelled;
std::set<acc_mark> marks_relabelled;
for (auto mark : marks) {
marks_relabelled.insert(mark_conversion[mark]);
}
Expand Down

0 comments on commit 571ed2c

Please sign in to comment.