Skip to content

Commit

Permalink
Fixed bug in nft::insert_levels(). All tests for mata::nft::replace_r…
Browse files Browse the repository at this point in the history 
…eluctant_literal() uncommented and passing. (#393)
  • Loading branch information
@koniksedy @Adda0
koniksedy authored and Adda0 committed Nov 22, 2024
1 parent 0de7e91 commit fabe030
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 30 deletions.
2 changes: 1 addition & 1 deletion src/nft/operations.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,7 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask,
}

// Construct an empty automaton with updated levels.
Nft result(Delta{}, nft.initial, nft.final, new_state_levels, static_cast<unsigned int>(new_levels_mask.size()), nft.alphabet);
Nft result(Delta(nft.num_of_states()), nft.initial, nft.final, new_state_levels, static_cast<unsigned int>(new_levels_mask.size()), nft.alphabet);

// Function to create a transition between source and target states.
// The transition symbol is determined based on the parameters:
Expand Down
67 changes: 38 additions & 29 deletions tests/nft/strings.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -617,11 +617,11 @@ TEST_CASE("mata::nft::replace_reluctant_literal()") {
Nft nft{};
Nft expected{};
EnumAlphabet alphabet{ 'a', 'b', 'c' };
ReluctantReplaceSUT reluctant_replace;

SECTION("'abcc' replace with 'a' replace all") {
nft = nft::strings::replace_reluctant_literal(Word{ 'a', 'b', 'c', 'c' }, Word{ 'a' }, &alphabet, ReplaceMode::All);
// std::cout << "result\n";
// std::cout << nft.print_to_DOT();

CHECK(nft.is_tuple_in_lang({ { 'a', 'b', 'c', 'c' },
{ 'a' } }));
CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'b', 'c', 'c' },
Expand All @@ -634,33 +634,42 @@ TEST_CASE("mata::nft::replace_reluctant_literal()") {
{ 'c', 'a', 'a', 'a' } }));
CHECK(nft.is_tuple_in_lang({ { 'a', 'c', 'a', 'b', 'c', 'c', 'a', 'a', 'b', 'c', 'c' },
{ 'a', 'c', 'a', 'a', 'a' } }));
// FIXME(nft): Bug in `is_tuple_in_lang()`: infinite loop.
// CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'b', 'c', 'c', 'a' },
// { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'a', 'a', 'a' } }));
// expected = nft::builder::parse_from_mata(std::string(
// "@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q35\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:1 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:0 q18:1 q19:0 q20:1 q21:1 q22:1 q23:0 q24:1 q25:0 q26:1 q27:1 q28:0 q29:1 q30:0 q31:1 q32:0 q33:1 q34:1 q35:0 q36:1 q37:1 q38:1 q39:1 q40:0 q41:1 q42:1 q43:0 q44:1 q45:0 q46:1\n%LevelsCnt 2\nq0 97 q5\nq0 98 q6\nq0 99 q7\nq0 4294967196 q37\nq1 97 q8\nq1 98 q9\nq1 99 q10\nq1 4294967196 q38\nq2 97 q13\nq2 98 q16\nq2 99 q21\nq2 4294967196 q39\nq3 97 q22\nq3 98 q27\nq3 99 q34\nq3 4294967196 q42\nq4 4294967295 q36\nq5 4294967295 q1\nq6 98 q0\nq7 99 q0\nq8 97 q1\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 99 q0\nq13 97 q14\nq14 4294967295 q15\nq15 98 q1\nq16 97 q17\nq17 4294967295 q18\nq18 98 q19\nq19 4294967295 q20\nq20 98 q0\nq21 4294967295 q3\nq22 97 q23\nq23 4294967295 q24\nq24 98 q25\nq25 4294967295 q26\nq26 99 q1\nq27 97 q28\nq28 4294967295 q29\nq29 98 q30\nq30 4294967295 q31\nq31 99 q32\nq32 4294967295 q33\nq33 98 q0\nq34 4294967295 q4\nq36 97 q0\nq37 4294967295 q35\nq38 97 q35\nq39 97 q40\nq40 4294967295 q41\nq41 98 q35\nq42 97 q43\nq43 4294967295 q44\nq44 98 q45\nq45 4294967295 q46\nq46 99 q35\n"
// ));
// CHECK(nft::are_equivalent(nft, expected));
CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'b', 'c', 'c', 'a' },
{ 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'a', 'a', 'a' } }));
expected = nft::builder::parse_from_mata(std::string(
"@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q35\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:1 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:0 q18:1 q19:0 q20:1 q21:1 q22:1 q23:0 q24:1 q25:0 q26:1 q27:1 q28:0 q29:1 q30:0 q31:1 q32:0 q33:1 q34:1 q35:0 q36:1 q37:1 q38:1 q39:1 q40:0 q41:1 q42:1 q43:0 q44:1 q45:0 q46:1\n%LevelsCnt 2\nq0 97 q5\nq0 98 q6\nq0 99 q7\nq0 4294967295 q37\nq1 97 q8\nq1 98 q9\nq1 99 q10\nq1 4294967295 q38\nq2 97 q13\nq2 98 q16\nq2 99 q21\nq2 4294967295 q39\nq3 97 q22\nq3 98 q27\nq3 99 q34\nq3 4294967295 q42\nq4 4294967295 q36\nq5 4294967295 q1\nq6 98 q0\nq7 99 q0\nq8 97 q1\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 99 q0\nq13 97 q14\nq14 4294967295 q15\nq15 98 q1\nq16 97 q17\nq17 4294967295 q18\nq18 98 q19\nq19 4294967295 q20\nq20 98 q0\nq21 4294967295 q3\nq22 97 q23\nq23 4294967295 q24\nq24 98 q25\nq25 4294967295 q26\nq26 99 q1\nq27 97 q28\nq28 4294967295 q29\nq29 98 q30\nq30 4294967295 q31\nq31 99 q32\nq32 4294967295 q33\nq33 98 q0\nq34 4294967295 q4\nq36 97 q0\nq37 4294967295 q35\nq38 97 q35\nq39 97 q40\nq40 4294967295 q41\nq41 98 q35\nq42 97 q43\nq43 4294967295 q44\nq44 98 q45\nq45 4294967295 q46\nq46 99 q35\n"
));

// NOTE(nft): It appears that the END_MARKER is left in the resulting transducer.
// This transducer should not contain END_MARKER, as it exists only at the synchronization
// levels (of lhs and rhs) and will be projected out at the end of the composition.
// Moreover, this transducer represents the ReplaceAll procedure, therefore it should not contain any END_MARKER.
//
// expected = nft::builder::parse_from_mata(std::string(
// "@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q35\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:1 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:0 q18:1 q19:0 q20:1 q21:1 q22:1 q23:0 q24:1 q25:0 q26:1 q27:1 q28:0 q29:1 q30:0 q31:1 q32:0 q33:1 q34:1 q35:0 q36:1 q37:1 q38:1 q39:1 q40:0 q41:1 q42:1 q43:0 q44:1 q45:0 q46:1\n%LevelsCnt 2\nq0 97 q5\nq0 98 q6\nq0 99 q7\nq0 4294967196 q37\nq1 97 q8\nq1 98 q9\nq1 99 q10\nq1 4294967196 q38\nq2 97 q13\nq2 98 q16\nq2 99 q21\nq2 4294967196 q39\nq3 97 q22\nq3 98 q27\nq3 99 q34\nq3 4294967196 q42\nq4 4294967295 q36\nq5 4294967295 q1\nq6 98 q0\nq7 99 q0\nq8 97 q1\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 99 q0\nq13 97 q14\nq14 4294967295 q15\nq15 98 q1\nq16 97 q17\nq17 4294967295 q18\nq18 98 q19\nq19 4294967295 q20\nq20 98 q0\nq21 4294967295 q3\nq22 97 q23\nq23 4294967295 q24\nq24 98 q25\nq25 4294967295 q26\nq26 99 q1\nq27 97 q28\nq28 4294967295 q29\nq29 98 q30\nq30 4294967295 q31\nq31 99 q32\nq32 4294967295 q33\nq33 98 q0\nq34 4294967295 q4\nq36 97 q0\nq37 4294967295 q35\nq38 97 q35\nq39 97 q40\nq40 4294967295 q41\nq41 98 q35\nq42 97 q43\nq43 4294967295 q44\nq44 98 q45\nq45 4294967295 q46\nq46 99 q35\n"
// ));

CHECK(nft::are_equivalent(nft, expected));
}

// SECTION("'abcc' replace with 'bbb' replace single") {
// nft = reluctant_replace.replace_literal_nft(Word{ 'a', 'b', 'c', 'c' }, Word{ 'b', 'b', 'b' }, &alphabet, END_MARKER, ReplaceMode::Single);
// CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'b', 'c', 'c', END_MARKER },
// { 'a', 'a', 'a', 'b', 'a', 'a', 'b', 'b', 'b', 'a', 'a', 'b', 'c', 'c' } }));
// expected = nft::builder::parse_from_mata(std::string(
// "@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q45 q46\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:1 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:0 q18:1 q19:0 q20:1 q21:1 q22:1 q23:0 q24:1 q25:0 q26:1 q27:1 q28:0 q29:1 q30:0 q31:1 q32:0 q33:1 q34:1 q35:1 q36:0 q37:1 q38:0 q39:1 q40:0 q41:1 q42:1 q43:1 q44:1 q45:0 q46:0 q47:1 q48:1 q49:1 q50:0 q51:1 q52:1 q53:0 q54:1 q55:0 q56:1\n%LevelsCnt 2\nq0 97 q5\nq0 98 q6\nq0 99 q7\nq0 4294967196 q47\nq1 97 q8\nq1 98 q9\nq1 99 q10\nq1 4294967196 q48\nq2 97 q13\nq2 98 q16\nq2 99 q21\nq2 4294967196 q49\nq3 97 q22\nq3 98 q27\nq3 99 q34\nq3 4294967196 q52\nq4 4294967295 q35\nq5 4294967295 q1\nq6 98 q0\nq7 99 q0\nq8 97 q1\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 99 q0\nq13 97 q14\nq14 4294967295 q15\nq15 98 q1\nq16 97 q17\nq17 4294967295 q18\nq18 98 q19\nq19 4294967295 q20\nq20 98 q0\nq21 4294967295 q3\nq22 97 q23\nq23 4294967295 q24\nq24 98 q25\nq25 4294967295 q26\nq26 99 q1\nq27 97 q28\nq28 4294967295 q29\nq29 98 q30\nq30 4294967295 q31\nq31 99 q32\nq32 4294967295 q33\nq33 98 q0\nq34 4294967295 q4\nq35 98 q36\nq36 4294967295 q37\nq37 98 q38\nq38 4294967295 q39\nq39 98 q40\nq40 97 q41\nq40 98 q42\nq40 99 q43\nq40 4294967196 q44\nq41 97 q40\nq42 98 q40\nq43 99 q40\nq44 4294967295 q45\nq47 4294967295 q46\nq48 97 q46\nq49 97 q50\nq50 4294967295 q51\nq51 98 q46\nq52 97 q53\nq53 4294967295 q54\nq54 98 q55\nq55 4294967295 q56\nq56 99 q46\n"
// ));
// CHECK(nft::are_equivalent(nft, expected));
// }

// SECTION("'aabac' replace with 'd' replace all") {
// nft = reluctant_replace.replace_literal_nft(Word{ 'a', 'a', 'b', 'a', 'c' }, Word{ 'd' }, &alphabet, END_MARKER,
// ReplaceMode::All);
// CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'a', 'c', 'a', END_MARKER },
// { 'a', 'a', 'a', 'b', 'a', 'd', 'a' } }));
// expected = nft::builder::parse_from_mata(std::string(
// "@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q54\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:0 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:1 q18:1 q19:0 q20:1 q21:0 q22:1 q23:1 q24:1 q25:0 q26:1 q27:0 q28:1 q29:0 q30:1 q31:1 q32:0 q33:1 q34:0 q35:1 q36:0 q37:1 q38:1 q39:0 q40:1 q41:0 q42:1 q43:1 q44:0 q45:1 q46:0 q47:1 q48:0 q49:1 q50:0 q51:1 q52:1 q53:1 q54:0 q55:1 q56:1 q57:1 q58:0 q59:1 q60:1 q61:0 q62:1 q63:0 q64:1 q65:1 q66:0 q67:1 q68:0 q69:1 q70:0 q71:1\n%LevelsCnt 2\nq0 97 q6\nq0 98 q7\nq0 99 q8\nq0 4294967196 q55\nq1 97 q9\nq1 98 q10\nq1 99 q13\nq1 4294967196 q56\nq2 97 q16\nq2 98 q17\nq2 99 q18\nq2 4294967196 q57\nq3 97 q23\nq3 98 q24\nq3 99 q31\nq3 4294967196 q60\nq4 97 q38\nq4 98 q43\nq4 99 q52\nq4 4294967196 q65\nq5 4294967295 q53\nq6 4294967295 q1\nq7 98 q0\nq8 99 q0\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 98 q0\nq13 97 q14\nq14 4294967295 q15\nq15 99 q0\nq16 97 q2\nq17 4294967295 q3\nq18 97 q19\nq19 4294967295 q20\nq20 97 q21\nq21 4294967295 q22\nq22 99 q0\nq23 4294967295 q4\nq24 97 q25\nq25 4294967295 q26\nq26 97 q27\nq27 4294967295 q28\nq28 98 q29\nq29 4294967295 q30\nq30 98 q0\nq31 97 q32\nq32 4294967295 q33\nq33 97 q34\nq34 4294967295 q35\nq35 98 q36\nq36 4294967295 q37\nq37 99 q0\nq38 97 q39\nq39 4294967295 q40\nq40 97 q41\nq41 4294967295 q42\nq42 98 q2\nq43 97 q44\nq44 4294967295 q45\nq45 97 q46\nq46 4294967295 q47\nq47 98 q48\nq48 4294967295 q49\nq49 97 q50\nq50 4294967295 q51\nq51 98 q0\nq52 4294967295 q5\nq53 100 q0\nq55 4294967295 q54\nq56 97 q54\nq57 97 q58\nq58 4294967295 q59\nq59 97 q54\nq60 97 q61\nq61 4294967295 q62\nq62 97 q63\nq63 4294967295 q64\nq64 98 q54\nq65 97 q66\nq66 4294967295 q67\nq67 97 q68\nq68 4294967295 q69\nq69 98 q70\nq70 4294967295 q71\nq71 97 q54\n"
// ));
// CHECK(nft::are_equivalent(nft, expected));
// }
SECTION("'abcc' replace with 'bbb' replace single") {
nft = reluctant_replace.replace_literal_nft(Word{ 'a', 'b', 'c', 'c' }, Word{ 'b', 'b', 'b' }, &alphabet, END_MARKER, ReplaceMode::Single);
CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'b', 'c', 'c', END_MARKER },
{ 'a', 'a', 'a', 'b', 'a', 'a', 'b', 'b', 'b', 'a', 'a', 'b', 'c', 'c' } }));
expected = nft::builder::parse_from_mata(std::string(
"@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q45 q46\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:1 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:0 q18:1 q19:0 q20:1 q21:1 q22:1 q23:0 q24:1 q25:0 q26:1 q27:1 q28:0 q29:1 q30:0 q31:1 q32:0 q33:1 q34:1 q35:1 q36:0 q37:1 q38:0 q39:1 q40:0 q41:1 q42:1 q43:1 q44:1 q45:0 q46:0 q47:1 q48:1 q49:1 q50:0 q51:1 q52:1 q53:0 q54:1 q55:0 q56:1\n%LevelsCnt 2\nq0 97 q5\nq0 98 q6\nq0 99 q7\nq0 4294967196 q47\nq1 97 q8\nq1 98 q9\nq1 99 q10\nq1 4294967196 q48\nq2 97 q13\nq2 98 q16\nq2 99 q21\nq2 4294967196 q49\nq3 97 q22\nq3 98 q27\nq3 99 q34\nq3 4294967196 q52\nq4 4294967295 q35\nq5 4294967295 q1\nq6 98 q0\nq7 99 q0\nq8 97 q1\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 99 q0\nq13 97 q14\nq14 4294967295 q15\nq15 98 q1\nq16 97 q17\nq17 4294967295 q18\nq18 98 q19\nq19 4294967295 q20\nq20 98 q0\nq21 4294967295 q3\nq22 97 q23\nq23 4294967295 q24\nq24 98 q25\nq25 4294967295 q26\nq26 99 q1\nq27 97 q28\nq28 4294967295 q29\nq29 98 q30\nq30 4294967295 q31\nq31 99 q32\nq32 4294967295 q33\nq33 98 q0\nq34 4294967295 q4\nq35 98 q36\nq36 4294967295 q37\nq37 98 q38\nq38 4294967295 q39\nq39 98 q40\nq40 97 q41\nq40 98 q42\nq40 99 q43\nq40 4294967196 q44\nq41 97 q40\nq42 98 q40\nq43 99 q40\nq44 4294967295 q45\nq47 4294967295 q46\nq48 97 q46\nq49 97 q50\nq50 4294967295 q51\nq51 98 q46\nq52 97 q53\nq53 4294967295 q54\nq54 98 q55\nq55 4294967295 q56\nq56 99 q46\n"
));
CHECK(nft::are_equivalent(nft, expected));
}

SECTION("'aabac' replace with 'd' replace all") {
nft = reluctant_replace.replace_literal_nft(Word{ 'a', 'a', 'b', 'a', 'c' }, Word{ 'd' }, &alphabet, END_MARKER,
ReplaceMode::All);
CHECK(nft.is_tuple_in_lang({ { 'a', 'a', 'a', 'b', 'a', 'a', 'a', 'b', 'a', 'c', 'a', END_MARKER },
{ 'a', 'a', 'a', 'b', 'a', 'd', 'a' } }));
expected = nft::builder::parse_from_mata(std::string(
"@NFT-explicit\n%Alphabet-auto\n%Initial q0\n%Final q54\n%Levels q0:0 q1:0 q2:0 q3:0 q4:0 q5:0 q6:1 q7:1 q8:1 q9:1 q10:1 q11:0 q12:1 q13:1 q14:0 q15:1 q16:1 q17:1 q18:1 q19:0 q20:1 q21:0 q22:1 q23:1 q24:1 q25:0 q26:1 q27:0 q28:1 q29:0 q30:1 q31:1 q32:0 q33:1 q34:0 q35:1 q36:0 q37:1 q38:1 q39:0 q40:1 q41:0 q42:1 q43:1 q44:0 q45:1 q46:0 q47:1 q48:0 q49:1 q50:0 q51:1 q52:1 q53:1 q54:0 q55:1 q56:1 q57:1 q58:0 q59:1 q60:1 q61:0 q62:1 q63:0 q64:1 q65:1 q66:0 q67:1 q68:0 q69:1 q70:0 q71:1\n%LevelsCnt 2\nq0 97 q6\nq0 98 q7\nq0 99 q8\nq0 4294967196 q55\nq1 97 q9\nq1 98 q10\nq1 99 q13\nq1 4294967196 q56\nq2 97 q16\nq2 98 q17\nq2 99 q18\nq2 4294967196 q57\nq3 97 q23\nq3 98 q24\nq3 99 q31\nq3 4294967196 q60\nq4 97 q38\nq4 98 q43\nq4 99 q52\nq4 4294967196 q65\nq5 4294967295 q53\nq6 4294967295 q1\nq7 98 q0\nq8 99 q0\nq9 4294967295 q2\nq10 97 q11\nq11 4294967295 q12\nq12 98 q0\nq13 97 q14\nq14 4294967295 q15\nq15 99 q0\nq16 97 q2\nq17 4294967295 q3\nq18 97 q19\nq19 4294967295 q20\nq20 97 q21\nq21 4294967295 q22\nq22 99 q0\nq23 4294967295 q4\nq24 97 q25\nq25 4294967295 q26\nq26 97 q27\nq27 4294967295 q28\nq28 98 q29\nq29 4294967295 q30\nq30 98 q0\nq31 97 q32\nq32 4294967295 q33\nq33 97 q34\nq34 4294967295 q35\nq35 98 q36\nq36 4294967295 q37\nq37 99 q0\nq38 97 q39\nq39 4294967295 q40\nq40 97 q41\nq41 4294967295 q42\nq42 98 q2\nq43 97 q44\nq44 4294967295 q45\nq45 97 q46\nq46 4294967295 q47\nq47 98 q48\nq48 4294967295 q49\nq49 97 q50\nq50 4294967295 q51\nq51 98 q0\nq52 4294967295 q5\nq53 100 q0\nq55 4294967295 q54\nq56 97 q54\nq57 97 q58\nq58 4294967295 q59\nq59 97 q54\nq60 97 q61\nq61 4294967295 q62\nq62 97 q63\nq63 4294967295 q64\nq64 98 q54\nq65 97 q66\nq66 4294967295 q67\nq67 97 q68\nq68 4294967295 q69\nq69 98 q70\nq70 4294967295 q71\nq71 97 q54\n"
));
CHECK(nft::are_equivalent(nft, expected));
}
}

0 comments on commit fabe030

Please sign in to comment.