Skip to content

Commit c1702be

Browse files
committed
feat(nft): Implement complement for NFTs
1 parent 5fdd710 commit c1702be

7 files changed

Lines changed: 251 additions & 249 deletions

File tree

include/mata/nft/algorithms.hh

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,15 +35,17 @@ Nft minimize_brzozowski(const Nft& aut);
3535

3636
/**
3737
* Complement implemented by determization, adding sink state and making automaton complete. Then it adds final states
38-
* which were non final in the original automaton.
38+
* which were non-final in the original automaton.
3939
* @param[in] aut Automaton to be complemented.
4040
* @param[in] symbols Symbols needed to make the automaton complete.
41+
* @param[in] epsilons Epsilon symbols to include when complementing; they are handled as normal alphabet symbols during complementation. *
4142
* @param[in] minimize_during_determinization Whether the determinized automaton is computed by (brzozowski)
4243
* minimization.
4344
* @return Complemented automaton.
4445
*/
45-
Nft complement_classical(const Nft& aut, const mata::utils::OrdVector<Symbol>& symbols,
46-
bool minimize_during_determinization = false);
46+
Nft complement_classical(
47+
const Nft& aut, const mata::utils::OrdVector<Symbol>& symbols,
48+
const utils::OrdVector<unsigned>& epsilons, bool minimize_during_determinization = false);
4749

4850
/**
4951
* Inclusion implemented by complementation of bigger automaton, intersecting it with smaller and then it checks
@@ -53,6 +55,8 @@ Nft complement_classical(const Nft& aut, const mata::utils::OrdVector<Symbol>& s
5355
* @param[in] alphabet Alphabet of both automata (it is computed automatically, but it is more efficient to set it if
5456
* you have it).
5557
* @param[out] cex A potential counterexample word which breaks inclusion
58+
* @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
59+
* is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
5660
* @return True if smaller language is included,
5761
* i.e., if the final intersection of smaller complement of bigger is empty.
5862
*/
@@ -64,6 +68,8 @@ bool is_included_naive(const Nft& smaller, const Nft& bigger, const Alphabet* al
6468
* @param[in] bigger Automaton which language should include the smaller one
6569
* @param[in] alphabet Alphabet of both automata (not needed for antichain algorithm)
6670
* @param[out] cex A potential counterexample word which breaks inclusion
71+
* @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
72+
* is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE.
6773
* @return True if smaller language is included,
6874
* i.e., if the final intersection of smaller complement of bigger is empty.
6975
*/
@@ -74,7 +80,7 @@ bool is_included_antichains(const Nft& smaller, const Nft& bigger, const Alphabe
7480
* @param[in] aut Automaton which universality is checked
7581
* @param[in] alphabet Alphabet of the automaton
7682
* @param[out] cex Counterexample word which eventually breaks the universality
77-
* @return True if the complemented automaton has non empty language, i.e., the original one is not universal
83+
* @return True if the complemented automaton has non-empty language, i.e., the original one is not universal
7884
*/
7985
bool is_universal_naive(const Nft& aut, const Alphabet& alphabet, Run* cex);
8086

include/mata/nft/nft.hh

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -906,20 +906,18 @@ Nft compose(const Nft& lhs, const Nft& rhs, Level lhs_sync_level = 1, Level rhs_
906906
Nft concatenate(const Nft& lhs, const Nft& rhs, bool use_epsilon = false,
907907
StateRenaming* lhs_state_renaming = nullptr, StateRenaming* rhs_state_renaming = nullptr);
908908

909-
910-
#ifdef MATA_NFT_NOT_IMPLEMENTED
911-
// TODO(nft): Implement for NFTs.
912909
/**
913910
* @brief Compute automaton accepting complement of @p aut.
914911
*
915-
* @param[in] aut Automaton whose complement to compute.
912+
* @param[in] nft Automaton whose complement to compute.
916913
* @param[in] alphabet Alphabet used for complementation.
914+
* @param[in] epsilons Epsilon symbols to include when complementing. Epsilon symbols are handled as normal alphabet symbols.
917915
* @param[in] params Optional parameters to control the complementation algorithm:
918916
* - "algorithm": "classical" (classical algorithm determinizes the automaton, makes it complete and swaps final and non-final states);
919-
* - "minimize": "true"/"false" (whether to compute minimal deterministic automaton for classical algorithm);
917+
* - "minimize": (TODO: unimplemented) "true"/"false" (whether to compute minimal deterministic automaton for classical algorithm);
920918
* @return Complemented automaton.
921919
*/
922-
Nft complement(const Nft& aut, const Alphabet& alphabet,
920+
Nft complement(const Nft& nft, const Alphabet& alphabet, const utils::OrdVector<Symbol>& epsilons = {},
923921
const ParameterMap& params = {{ "algorithm", "classical" }, { "minimize", "false" }});
924922

925923
/**
@@ -930,16 +928,19 @@ Nft complement(const Nft& aut, const Alphabet& alphabet,
930928
* automata over the same set of @c symbols: the function does not need to compute the ordered set of symbols from
931929
* the alphabet again (and for each automaton).
932930
*
933-
* @param[in] aut Automaton whose complement to compute.
931+
* @param[in] nft Automaton whose complement to compute.
934932
* @param[in] symbols Symbols to complement over.
933+
* @param[in] epsilons Epsilon symbols to include when complementing. Epsilon symbols are handled as normal alphabet symbols.
935934
* @param[in] params Optional parameters to control the complementation algorithm:
936935
* - "algorithm": "classical" (classical algorithm determinizes the automaton, makes it complete and swaps final and non-final states);
937-
* - "minimize": "true"/"false" (whether to compute minimal deterministic automaton for classical algorithm);
936+
* - "minimize": (TODO: unimplemented) "true"/"false" (whether to compute minimal deterministic automaton for classical algorithm);
938937
* @return Complemented automaton.
939938
*/
940-
Nft complement(const Nft& aut, const utils::OrdVector<Symbol>& symbols,
939+
Nft complement(const Nft& nft, const utils::OrdVector<Symbol>& symbols, const utils::OrdVector<Symbol>& epsilons = {},
941940
const ParameterMap& params = {{ "algorithm", "classical" }, { "minimize", "false" }});
942941

942+
#ifdef MATA_NFT_NOT_IMPLEMENTED
943+
// TODO(nft): Implement for NFTs.
943944
/**
944945
* @brief Compute minimal deterministic automaton.
945946
*

src/nfa/universal.cc

Lines changed: 3 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,20 +12,11 @@ using namespace mata::utils;
1212
//TODO: this could be merged with inclusion, or even removed, universality could be implemented using inclusion,
1313
// it is not something needed in practice, so some little overhead is ok
1414

15-
16-
/// naive universality check (complementation + emptiness)
1715
bool mata::nfa::algorithms::is_universal_naive(
18-
const Nfa& aut,
19-
const Alphabet& alphabet,
20-
Run* cex)
21-
{ // {{{
22-
Nfa cmpl = complement(aut, alphabet);
23-
24-
return cmpl.is_lang_empty(cex);
25-
} // is_universal_naive }}}
26-
16+
const Nfa& aut,
17+
const Alphabet& alphabet,
18+
Run* cex) { return complement(aut, alphabet).is_lang_empty(cex); }
2719

28-
/// universality check using Antichains
2920
bool mata::nfa::algorithms::is_universal_antichains(
3021
const Nfa& aut,
3122
const Alphabet& alphabet,

src/nft/complement.cc

Lines changed: 58 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -8,70 +8,81 @@
88
using namespace mata::nft;
99
using namespace mata::utils;
1010

11-
#ifdef MATA_NFT_NOT_IMPLEMENTED
12-
Nft mata::nft::algorithms::complement_classical(const Nft& aut, const OrdVector<Symbol>& symbols,
13-
const bool minimize_during_determinization) {
11+
Nft algorithms::complement_classical(
12+
const Nft& aut, const OrdVector<Symbol>& symbols, const OrdVector<Symbol>& epsilons,
13+
const bool minimize_during_determinization) {
1414
Nft result;
15-
State sink_state;
1615
if (minimize_during_determinization) {
17-
result = minimize_brzozowski(aut); // brzozowski minimization makes it deterministic
18-
if (result.final.empty() && !result.initial.empty()) {
19-
assert(result.initial.size() == 1);
20-
// if automaton does not accept anything, then there is only one (initial) state
21-
// which can be the sink state (so we do not create unnecessary one)
22-
sink_state = *result.initial.begin();
23-
} else {
24-
sink_state = result.num_of_states();
25-
}
26-
} else {
27-
std::unordered_map<StateSet, State> subset_map;
28-
result = determinize(aut, &subset_map);
29-
// check if a sink state was not created during determinization
30-
if (const auto sink_state_iter = subset_map.find({}); sink_state_iter != subset_map.end()) {
31-
sink_state = sink_state_iter->second;
32-
} else {
33-
sink_state = result.num_of_states();
34-
}
35-
}
36-
37-
result.make_complete(symbols, sink_state);
38-
result.final.complement(result.num_of_states());
16+
throw std::runtime_error(
17+
std::string(__func__) +
18+
": unimplemented option 'minimize' = 'true' for the complementation algorithm on NFTs."
19+
);
20+
// TODO(nft): implement minimization for NFTs.
21+
// result = determinize_and_minimize(aut);
22+
// result = minimize_brzozowski(aut); // brzozowski minimization makes it deterministic
23+
// if (result.final.empty() && !result.initial.empty()) {
24+
// assert(result.initial.size() == 1);
25+
// // if automaton does not accept anything, then there is only one (initial) state
26+
// // which can be the sink state (so we do not create unnecessary one)
27+
// sink_state = *result.initial.begin();
28+
// } else {
29+
// sink_state = result.num_of_states();
30+
// }
31+
} else { result = determinize(aut); }
3932

33+
result.make_complete(symbols, epsilons);
34+
// TODO(nft): Should empty nft produce a complement with one initial and final state accepting { {epsilon}, {epsilon}, {epsilon} }?
35+
if (result.initial.empty()) {
36+
const State initial{ result.add_state() };
37+
result.initial.insert(initial);
38+
}
39+
SparseSet<State> new_final_states{};
40+
const size_t num_of_states{ result.num_of_states() };
41+
for (State state{ 0 }; state < num_of_states; ++state) {
42+
if (result.levels[state] == 0 && !result.final.contains(state)) { new_final_states.insert(state); }
43+
}
44+
result.final = new_final_states;
4045
return result;
4146
}
4247

43-
Nft mata::nft::complement(const Nft& aut, const Alphabet& alphabet, const ParameterMap& params) {
44-
return mata::nft::complement(aut, alphabet.get_alphabet_symbols(), params);
48+
Nft mata::nft::complement(const Nft& nft, const Alphabet& alphabet, const OrdVector<Symbol>& epsilons, const ParameterMap& params) {
49+
return complement(nft, alphabet.get_alphabet_symbols(), epsilons, params);
4550
}
4651

47-
Nft mata::nft::complement(const Nft& aut, const mata::utils::OrdVector<mata::Symbol>& symbols, const ParameterMap& params) {
48-
Nft result;
52+
Nft mata::nft::complement(const Nft& nft, const OrdVector<Symbol>& symbols, const OrdVector<Symbol>& epsilons, const ParameterMap& params) {
4953
// Setting the requested algorithm.
5054
decltype(algorithms::complement_classical)* algo = algorithms::complement_classical;
5155
if (!haskey(params, "algorithm")) {
52-
throw std::runtime_error(std::to_string(__func__) +
53-
" requires setting the \"algorithm\" key in the \"params\" argument; "
54-
"received: " + std::to_string(params));
56+
throw std::runtime_error(
57+
std::to_string(__func__) +
58+
" requires setting the 'algorithm' key in the 'params' argument; "
59+
"received: " + std::to_string(params)
60+
);
5561
}
5662

5763
const std::string& str_algo = params.at("algorithm");
58-
if ("classical" == str_algo) { /* default */ }
59-
else {
60-
throw std::runtime_error(std::to_string(__func__) +
61-
" received an unknown value of the \"algorithm\" key: " + str_algo);
64+
if ("classical" == str_algo) { /* default */ } else {
65+
throw std::runtime_error(
66+
std::to_string(__func__) +
67+
" received an unknown value of the 'algorithm' key: " + str_algo
68+
);
6269
}
6370

64-
bool minimize_during_determinization = false;
71+
bool minimize_during_determinization{ false };
6572
if (params.contains("minimize")) {
66-
const std::string& minimize_arg = params.at("minimize");
67-
if ("true" == minimize_arg) { minimize_during_determinization = true; }
68-
else if ("false" == minimize_arg) { minimize_during_determinization = false; }
69-
else {
70-
throw std::runtime_error(std::to_string(__func__) +
71-
" received an unknown value of the \"minimize\" key: " + str_algo);
73+
if (const std::string& minimize_arg = params.at("minimize");
74+
"true" == minimize_arg) {
75+
throw std::runtime_error(
76+
std::to_string(__func__) +
77+
" received unimplemented option 'minimize' = 'true' for the complementation algorithm on NFTs."
78+
);
79+
// TODO(nft): implement minimization for NFTs.
80+
// minimize_during_determinization = true;
81+
} else if ("false" == minimize_arg) { minimize_during_determinization = false; } else {
82+
throw std::runtime_error(
83+
std::to_string(__func__) + " received an unknown value of the 'minimize' key: " + minimize_arg
84+
);
7285
}
7386
}
74-
75-
return algo(aut, symbols, minimize_during_determinization);
87+
return algo(nft, symbols, epsilons, minimize_during_determinization);
7688
}
77-
#endif

tests/CMakeLists.txt

Lines changed: 28 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,32 @@
11
add_executable(tests
2-
ord-vector.cc
3-
sparse-set.cc
4-
synchronized-iterator.cc
5-
two-dimensional-map.cc
6-
alphabet.cc
7-
parser.cc
8-
re2parser.cc
9-
mintermization.cc
10-
nfa/delta.cc
11-
nfa/nfa.cc
12-
nfa/builder.cc
13-
nfa/nfa-concatenation.cc
14-
nfa/nfa-product.cc
15-
nfa/nfa-profiling.cc
16-
nfa/nfa-plumbing.cc
17-
nft/delta.cc
18-
nft/nft.cc
19-
nft/builder.cc
20-
nft/nft-composition.cc
21-
nft/nft-concatenation.cc
22-
nft/nft-intersection.cc
23-
nft/nft-profiling.cc
24-
nft/nft-plumbing.cc
25-
applications/strings/noodlification.cc
26-
applications/strings/segmentation.cc
27-
applications/strings/string-solving.cc
28-
applications/strings/replace.cc
2+
ord-vector.cc
3+
sparse-set.cc
4+
synchronized-iterator.cc
5+
two-dimensional-map.cc
6+
alphabet.cc
7+
parser.cc
8+
re2parser.cc
9+
mintermization.cc
10+
nfa/delta.cc
11+
nfa/nfa.cc
12+
nfa/builder.cc
13+
nfa/nfa-concatenation.cc
14+
nfa/nfa-product.cc
15+
nfa/nfa-profiling.cc
16+
nfa/nfa-plumbing.cc
17+
nft/delta.cc
18+
nft/nft.cc
19+
nft/builder.cc
20+
nft/complement.cc
21+
nft/nft-composition.cc
22+
nft/nft-concatenation.cc
23+
nft/nft-intersection.cc
24+
nft/nft-profiling.cc
25+
nft/nft-plumbing.cc
26+
applications/strings/noodlification.cc
27+
applications/strings/segmentation.cc
28+
applications/strings/string-solving.cc
29+
applications/strings/replace.cc
2930
)
3031

3132
target_link_libraries(tests PRIVATE libmata Catch2::Catch2WithMain)

0 commit comments

Comments
 (0)