Skip to content

Commit cc8ccca

Browse files
alan23273850cursoragent
alan23273850
and
cursoragent
committed
Refactor reduce and LTS: split by responsibility
Reduce: - reduce_common.hh: shared reindex_aut_states, compact_aut, find_index, aut_is_single_occurrence - reduce_sim.cc: LTS-based sim_reduce (compute_down_sim + reindex) - reduce.cc: light/bottom-up/remove_useless/fraction_simplification/k_unification, uses reduce_detail:: LTS: - explicit_lts_build.cc: ExplicitLTS::addTransition (LTS construction) - explicit_lts_sim.cc: computeSimulation, Block, SimulationEngine only Co-authored-by: Cursor <cursoragent@cursor.com>
1 parent cab4856 commit cc8ccca

5 files changed

Lines changed: 198 additions & 178 deletions

File tree

‎include/autoq/reduce_common.hh‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
/**
2+
* Shared helpers for automata reduction: reindexing, compaction, single-occurrence check.
3+
* Used by reduce.cc (light/bottom-up/remove_useless) and reduce_sim.cc (sim_reduce).
4+
*/
5+
#ifndef AUTOQ_REDUCE_COMMON_HH
6+
#define AUTOQ_REDUCE_COMMON_HH
7+
8+
#include "autoq/aut_description.hh"
9+
#include "autoq/simulation/transl_weak.hh"
10+
#include <unordered_map>
11+
#include <set>
12+
#include <algorithm>
13+
14+
namespace AUTOQ {
15+
namespace reduce_detail {
16+
17+
template <class Index, typename Symbol>
18+
void reindex_aut_states(Automata<Symbol>& aut, Index& index)
19+
{
20+
using State = typename Automata<Symbol>::State;
21+
using StateVector = typename Automata<Symbol>::StateVector;
22+
23+
StateVector newFinal;
24+
for (const State& state : aut.finalStates) {
25+
if (newFinal.end() == std::find(newFinal.begin(), newFinal.end(), index[state])) {
26+
newFinal.push_back(index[state]);
27+
}
28+
}
29+
typename Automata<Symbol>::TopDownTransitions transitions_new;
30+
for (const auto &t : aut.transitions) {
31+
for (const auto &out_ins : t.second) {
32+
const auto &out = out_ins.first;
33+
for (auto in : out_ins.second) {
34+
for (auto &e : in) {
35+
e = index[e];
36+
}
37+
transitions_new[t.first][index[out]].insert(in);
38+
}
39+
}
40+
}
41+
aut.finalStates = newFinal;
42+
aut.transitions = transitions_new;
43+
}
44+
45+
template <class T>
46+
int find_index(const std::vector<T> &arr, T item) {
47+
for (int i = 0; i < static_cast<int>(arr.size()); ++i) {
48+
if (arr[i] == item)
49+
return i;
50+
}
51+
std::__throw_out_of_range("[ERROR] find_index: item not found.");
52+
}
53+
54+
/// Checks that a state is at most once on the right-hand (parent) side of any rule.
55+
template <typename Symbol>
56+
bool aut_is_single_occurrence(const Automata<Symbol>& aut)
57+
{
58+
using State = typename Automata<Symbol>::State;
59+
std::set<State> occurrences;
60+
for (auto symbMapPair : aut.transitions) {
61+
for (auto vecSetPair : symbMapPair.second) {
62+
for (auto state : vecSetPair.second) {
63+
auto itBoolPair = occurrences.insert(state);
64+
if (!itBoolPair.second) { return false; }
65+
}
66+
}
67+
}
68+
return true;
69+
}
70+
71+
/// Makes a TA compact (states renumbered from 0 consecutively).
72+
template <typename Symbol>
73+
void compact_aut(Automata<Symbol>& aut)
74+
{
75+
using State = typename Automata<Symbol>::State;
76+
using StateToStateMap = std::unordered_map<State, State>;
77+
using StateToStateTranslWeak = Util::TranslatorWeak<StateToStateMap>;
78+
StateToStateMap translMap;
79+
size_t stateCnt = 0;
80+
StateToStateTranslWeak transl(translMap,
81+
[&stateCnt](const State&) {return stateCnt++;});
82+
reindex_aut_states(aut, transl);
83+
aut.stateNum = stateCnt;
84+
}
85+
86+
} // namespace reduce_detail
87+
} // namespace AUTOQ
88+
89+
#endif

‎src/explicit_lts_build.cc‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/**
2+
* LTS construction: add transitions and grow the LTS structure.
3+
* Simulation algorithm (computeSimulation, Block, SimulationEngine) is in explicit_lts_sim.cc.
4+
*/
5+
#include "autoq/simulation/explicit_lts.hh"
6+
7+
void AUTOQ::ExplicitLTS::addTransition(
8+
size_t q,
9+
size_t a,
10+
size_t r)
11+
{
12+
if (a >= this->data_.size())
13+
{
14+
this->data_.resize(a + 1);
15+
}
16+
17+
if (q >= this->data_[a].first.size())
18+
{
19+
if (q >= this->states_)
20+
{
21+
this->states_ = q + 1;
22+
}
23+
24+
this->data_[a].first.resize(q + 1);
25+
}
26+
27+
if (r >= this->data_[a].second.size())
28+
{
29+
if (r >= this->states_)
30+
{
31+
this->states_ = r + 1;
32+
}
33+
34+
this->data_[a].second.resize(r + 1);
35+
}
36+
37+
this->data_[a].first[q].push_back(r);
38+
this->data_[a].second[r].push_back(q);
39+
40+
++this->transitions_;
41+
}

‎src/explicit_lts_sim.cc‎

Lines changed: 0 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -917,40 +917,3 @@ BinaryRelation AUTOQ::ExplicitLTS::computeSimulation()
917917
{
918918
return this->computeSimulation(this->states_);
919919
}
920-
921-
922-
void AUTOQ::ExplicitLTS::addTransition(
923-
size_t q,
924-
size_t a,
925-
size_t r)
926-
{
927-
if (a >= this->data_.size())
928-
{
929-
this->data_.resize(a + 1);
930-
}
931-
932-
if (q >= this->data_[a].first.size())
933-
{
934-
if (q >= this->states_)
935-
{
936-
this->states_ = q + 1;
937-
}
938-
939-
this->data_[a].first.resize(q + 1);
940-
}
941-
942-
if (r >= this->data_[a].second.size())
943-
{
944-
if (r >= this->states_)
945-
{
946-
this->states_ = r + 1;
947-
}
948-
949-
this->data_[a].second.resize(r + 1);
950-
}
951-
952-
this->data_[a].first[q].push_back(r);
953-
this->data_[a].second[r].push_back(q);
954-
955-
++this->transitions_;
956-
}

‎src/reduce.cc‎

Lines changed: 8 additions & 141 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
/**
2-
* Automata reduction and LTS-based simulation.
3-
* - sim_reduce uses LTS build (simulation::translate_to_lts_downward, count_aut_states) and compute_down_sim.
4-
* - Light reduce up/down, bottom-up reduce, reduce(), remove_useless().
5-
* - Helpers: reindex_aut_states, compact_aut, state_renumbering, fraction_simplification, k_unification.
2+
* Automata reduction: light reduce, bottom-up reduce, remove_useless, fraction_simplification, k_unification.
3+
* LTS-based sim_reduce is in reduce_sim.cc. Shared helpers in reduce_common.hh.
64
*/
75
#include <queue>
86

@@ -11,143 +9,12 @@
119
#include "autoq/symbol/symbolic.hh"
1210
#include "autoq/symbol/predicate.hh"
1311
#include "autoq/symbol/constrained.hh"
14-
#include "autoq/simulation/explicit_lts.hh"
15-
#include "autoq/simulation/automata_to_lts.hh"
12+
#include "autoq/reduce_common.hh"
1613

1714
using namespace AUTOQ;
1815
using namespace AUTOQ::Util;
1916

20-
namespace { // anonymous namespace
21-
22-
// --- LTS-based simulation (used by sim_reduce) ---
23-
24-
template <typename Symbol>
25-
typename Util::DiscontBinaryRelation<typename Automata<Symbol>::State> compute_down_sim(const AUTOQ::Automata<Symbol>& aut)
26-
{
27-
using State = typename Automata<Symbol>::State;
28-
using StateToIndexMap = typename std::unordered_map<State, size_t>;
29-
using StateToIndexTranslWeak = typename Util::TranslatorWeak<StateToIndexMap>;
30-
using DiscontBinaryRelOnStates = typename Util::DiscontBinaryRelation<State>;
31-
32-
StateToIndexMap translMap;
33-
size_t stateCnt = 0;
34-
StateToIndexTranslWeak transl(translMap,
35-
[&stateCnt](const State&) {return stateCnt++;});
36-
37-
size_t num_states = simulation::count_aut_states(aut);
38-
AUTOQ::ExplicitLTS lts = simulation::translate_to_lts_downward(aut, num_states, transl);
39-
BinaryRelation ltsSim = lts.computeSimulation(num_states);
40-
return DiscontBinaryRelOnStates(ltsSim, translMap);
41-
}
42-
43-
// --- Reindexing and compaction helpers ---
44-
45-
template <class Index, typename Symbol>
46-
void reindex_aut_states(Automata<Symbol>& aut, Index& index)
47-
{
48-
using State = typename Automata<Symbol>::State;
49-
using StateVector = typename Automata<Symbol>::StateVector;
50-
51-
StateVector newFinal;
52-
53-
for (const State& state : aut.finalStates) { // process final states
54-
if (newFinal.end() == std::find(newFinal.begin(), newFinal.end(), index[state])) {
55-
newFinal.push_back(index[state]);
56-
}
57-
}
58-
typename Automata<Symbol>::TopDownTransitions transitions_new;
59-
for (const auto &t : aut.transitions) {
60-
for (const auto &out_ins : t.second) {
61-
const auto &out = out_ins.first;
62-
for (auto in : out_ins.second) {
63-
for (auto &e : in) {
64-
e = index[e];
65-
}
66-
transitions_new[t.first][index[out]].insert(in);
67-
}
68-
}
69-
}
70-
71-
aut.finalStates = newFinal;
72-
aut.transitions = transitions_new;
73-
}
74-
75-
template <class T>
76-
int findIndex(const std::vector<T> &arr, T item) {
77-
for (int i = 0; i < static_cast<int>(arr.size()); ++i) {
78-
if (arr[i] == item)
79-
return i;
80-
}
81-
std::__throw_out_of_range("[ERROR] findIndex: item not found.");
82-
}
83-
84-
/// Checks that a state is at most once on the right-hand (parent) side of
85-
/// any rule.
86-
template <typename Symbol>
87-
bool aut_is_single_occurrence(const Automata<Symbol>& aut)
88-
{
89-
using State = typename Automata<Symbol>::State;
90-
91-
std::set<State> occurrences;
92-
for (auto symbMapPair : aut.transitions) {
93-
for (auto vecSetPair : symbMapPair.second) {
94-
for (auto state : vecSetPair.second) {
95-
auto itBoolPair = occurrences.insert(state);
96-
if (!itBoolPair.second) { return false; }
97-
}
98-
}
99-
}
100-
101-
return true;
102-
}
103-
104-
// Makes a TA compact (states are renumbered to start from 0 and go consecutively up
105-
template <typename Symbol>
106-
void compact_aut(Automata<Symbol>& aut)
107-
{
108-
using State = typename Automata<Symbol>::State;
109-
using StateToStateMap = typename std::unordered_map<State, State>;
110-
using StateToStateTranslWeak = typename Util::TranslatorWeak<StateToStateMap>;
111-
StateToStateMap translMap;
112-
size_t stateCnt = 0;
113-
StateToStateTranslWeak transl(translMap,
114-
[&stateCnt](const State&) {return stateCnt++;});
115-
116-
// AUTOQ_DEBUG("Before compact stateNum = " + Convert::ToString(aut.stateNum));
117-
reindex_aut_states(aut, transl);
118-
aut.stateNum = stateCnt;
119-
// AUTOQ_DEBUG("After compact stateNum = " + Convert::ToString(aut.stateNum));
120-
}
121-
} // anonymous namespace
122-
123-
// --- Reduction API: sim_reduce, light_reduce_*, bottom_up_reduce, reduce ---
124-
125-
template <typename Symbol>
126-
void AUTOQ::Automata<Symbol>::sim_reduce()
127-
{
128-
using State = typename Automata<Symbol>::State;
129-
using DiscontBinaryRelOnStates = typename Util::DiscontBinaryRelation<State>;
130-
using StateToStateMap = typename std::unordered_map<State, State>;
131-
132-
DiscontBinaryRelOnStates sim = compute_down_sim(*this);
133-
134-
// TODO: this is probably not optimal, we could probably get the mapping of
135-
// states for collapsing in a faster way
136-
sim.RestrictToSymmetric(); // sim is now an equivalence relation
137-
138-
StateToStateMap collapseMap;
139-
sim.GetQuotientProjection(collapseMap);
140-
141-
// Automata old = *this;
142-
reindex_aut_states(*this, collapseMap);
143-
144-
// if (!check_equal_aut(*this, old)) {
145-
// AUTOQ_DEBUG("wrong simulation result!");
146-
// AUTOQ_DEBUG("old: " + old.ToString());
147-
// AUTOQ_DEBUG("new: " + this->ToString());
148-
// AUTOQ_DEBUG("simulation: " + sim.ToString());
149-
// }
150-
}
17+
// --- Reduction API: light_reduce_*, bottom_up_reduce, reduce, remove_useless, etc. ---
15118

15219
template <typename Symbol>
15320
bool AUTOQ::Automata<Symbol>::light_reduce_up()
@@ -194,7 +61,7 @@ bool AUTOQ::Automata<Symbol>::light_reduce_up()
19461
// AUTOQ_DEBUG("index: " + Convert::ToString(index));
19562
if (changed) {
19663
// Automata old = *this;
197-
reindex_aut_states(*this, index);
64+
reduce_detail::reindex_aut_states(*this, index);
19865
// assert(check_equal_aut(old, *this));
19966
}
20067

@@ -247,7 +114,7 @@ bool AUTOQ::Automata<Symbol>::light_reduce_down()
247114

248115
StateToStateTranslWeak transl(index, [](const State& state) {return state;});
249116

250-
reindex_aut_states(*this, transl);
117+
reduce_detail::reindex_aut_states(*this, transl);
251118
return true;
252119
}
253120

@@ -333,7 +200,7 @@ bool AUTOQ::Automata<Symbol>::light_reduce_down()
333200
}
334201

335202
StateToStateTranslWeak transl(index, [](const State& state) { return state; });
336-
reindex_aut_states(*this, transl);
203+
reduce_detail::reindex_aut_states(*this, transl);
337204
return true;
338205
}
339206
}
@@ -573,7 +440,7 @@ void AUTOQ::Automata<Symbol>::reduce() {
573440
this->light_reduce_down_iter();
574441
// AUTOQ_DEBUG("after light_reduce_down: " + Convert::ToString(count_aut_states(*this)));
575442

576-
compact_aut(*this);
443+
reduce_detail::compact_aut(*this);
577444
// assert(check_equal_aut(old, *this));
578445

579446
auto a = transitions; //count_transitions();

0 commit comments

Comments
 (0)