Skip to content

Commit

Permalink
tested with jump mode AppendDontCarre
Browse files Browse the repository at this point in the history
  • Loading branch information
@koniksedy
koniksedy committed Feb 11, 2025
1 parent a4c9cc8 commit b1e5796
Show file tree
Hide file tree
Showing 2 changed files with 237 additions and 4 deletions.
4 changes: 2 additions & 2 deletions src/nft/operations.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -754,7 +754,7 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
// It is a transition from a nonzero-state (inner state) to a zero-state (tail).
// Map it as transition from the zero-state (head) to that nonzero-state (inner state).
if (jump_mode == JumpMode::AppendDontCares && (aut.num_of_levels - aut.levels[src]) > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - 1));
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
aut_inv.delta.add(renaming[head], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[src]);
} else {
Expand All @@ -764,7 +764,7 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
// It is a transition between two nonzero-states (inner states).
// Just swap the source and target.
if (jump_mode == JumpMode::AppendDontCares && (aut.levels[trg] - aut.levels[src]) > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.levels[trg] - 1));
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
aut_inv.delta.add(renaming[trg], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[src]);
} else {
Expand Down
237 changes: 235 additions & 2 deletions tests/nft/nft.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1978,8 +1978,8 @@ TEST_CASE("mata::nft::Nft::invert_levels()") {
expected.delta.add(0, 'c', 3);
expected.delta.add(3, 'd', 4);

CHECK(aut_new.num_of_states() == 5);
CHECK(aut_new.delta.num_of_transitions() == 5);
CHECK(aut_new.num_of_states() <= 5);
CHECK(aut_new.delta.num_of_transitions() <= 5);
CHECK(are_equivalent(aut_new, expected));
CHECK(are_equivalent(invert_levels(aut_new), aut));
}
Expand Down Expand Up @@ -2076,6 +2076,239 @@ TEST_CASE("mata::nft::Nft::invert_levels()") {
}

}

SECTION("jump mode == AppendDontCares") {
SECTION("empty automaton") {
Nft aut;
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);
CHECK(aut_new.num_of_states() == 0);
CHECK(are_equivalent(aut, aut_new, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("no transition only states") {
Nft aut(3);
aut.initial.insert(1);
aut.final.insert(2);
aut.num_of_levels = 1;
aut.levels = { 1, 0, 0 };
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);
CHECK(aut_new.is_lang_empty());
CHECK(aut_new.delta.num_of_transitions() == 0);
CHECK(are_equivalent(aut, aut_new, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear - 2 levels") {
Nft aut(3);
aut.initial.insert(0);
aut.final.insert(2);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(3);
expected.initial.insert(0);
expected.final.insert(2);
expected.num_of_levels = 2;
expected.levels = { 0, 1, 0 };
expected.delta.add(0, 'b', 1);
expected.delta.add(1, 'a', 2);

CHECK(aut_new.num_of_states() <= 3);
CHECK(aut_new.delta.num_of_transitions() <= 2);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear 2 - 2 levels") {
Nft aut(5);
aut.initial.insert(0);
aut.final.insert(4);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 0, 1, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
aut.delta.add(2, 'c', 3);
aut.delta.add(3, 'd', 4);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(5);
expected.initial.insert(0);
expected.final.insert(4);
expected.num_of_levels = 2;
expected.levels = {0, 1, 0, 1, 0};
expected.delta.add(0, 'b', 1);
expected.delta.add(1, 'a', 2);
expected.delta.add(2, 'd', 3);
expected.delta.add(3, 'c', 4);

CHECK(aut_new.num_of_states() <= 5);
CHECK(aut_new.delta.num_of_transitions() <= 4);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear + long jump - 3 levels") {
Nft aut(4);
aut.initial.insert(0);
aut.final.insert(3);
aut.num_of_levels = 3;
aut.levels = { 0, 1, 2, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
aut.delta.add(2, 'c', 3);
aut.delta.add(0, 'd', 3);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(5);
expected.initial.insert(0);
expected.final.insert(3);
expected.num_of_levels = 3;
expected.levels = {0, 1, 2, 0, 2};
expected.delta.add(0, 'c', 1);
expected.delta.add(0, DONT_CARE, 4);
expected.delta.add(1, 'b', 2);
expected.delta.add(2, 'a', 3);
expected.delta.add(4, 'd', 3);

CHECK(aut_new.num_of_states() <= 5);
CHECK(aut_new.delta.num_of_transitions() <= 5);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear + long jump 2 - 4 levels") {
Nft aut(4);
aut.initial.insert(0);
aut.final.insert(3);
aut.num_of_levels = 4;
aut.levels = { 0, 1, 3, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
aut.delta.add(2, 'c', 3);
aut.delta.add(0, 'd', 2);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(7);
expected.initial.insert(0);
expected.final.insert(4);
expected.num_of_levels = 4;
expected.levels = { 0, 1, 2, 3, 0, 1, 3 };
expected.delta.add(0, 'c', 1);
expected.delta.add(0, 'c', 5);
expected.delta.add(1, DONT_CARE, 2);
expected.delta.add(2, 'b', 3);
expected.delta.add(3, 'a', 4);
expected.delta.add(5, DONT_CARE, 6);
expected.delta.add(6, 'd', 4);

CHECK(aut_new.num_of_states() <= 7);
CHECK(aut_new.delta.num_of_transitions() <= 7);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Complex - 2 levels") {
Nft aut(5);
aut.initial.insert(0);
aut.final.insert(2);
aut.final.insert(4);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 0, 1, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
aut.delta.add(1, 'd', 4);
aut.delta.add(2, 'c', 1);
aut.delta.add(2, 'e', 3);
aut.delta.add(3, 'g', 4);
aut.delta.add(4, 'f', 3);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(9);
expected.initial.insert(0);
expected.final.insert(2);
expected.final.insert(6);
expected.num_of_levels = 2;
expected.levels = { 0, 1, 0, 1, 1, 1, 0, 1, 1 };
expected.delta.add(0, 'b', 1);
expected.delta.add(0, 'd', 8);
expected.delta.add(1, 'a', 2);
expected.delta.add(2, 'b', 3);
expected.delta.add(2, 'g', 4);
expected.delta.add(2, 'd', 5);
expected.delta.add(3, 'c', 2);
expected.delta.add(4, 'e', 6);
expected.delta.add(5, 'c', 6);
expected.delta.add(6, 'g', 7);
expected.delta.add(7, 'f', 6);
expected.delta.add(8, 'a', 6);

CHECK(aut_new.num_of_states() <= 9);
CHECK(aut_new.delta.num_of_transitions() <= 12);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Complex 2 - 3 levels") {
Nft aut(6);
aut.initial.insert(0);
aut.final.insert(3);
aut.final.insert(4);
aut.num_of_levels = 3;
aut.levels = { 0, 1, 2, 0, 0, 2 };
aut.delta.add(0, 'a', 3);
aut.delta.add(0, 'b', 2);
aut.delta.add(0, 'c', 1);
aut.delta.add(1, 'd', 2);
aut.delta.add(1, 'f', 3);
aut.delta.add(1, 'h', 4);
aut.delta.add(1, 'i', 5);
aut.delta.add(2, 'e', 3);
aut.delta.add(2, 'g', 4);
aut.delta.add(5, 'j', 4);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

aut_new.print_to_dot(std::cerr);

Nft expected = Nft(18);
expected.initial.insert(0);
expected.final.insert(10);
expected.final.insert(11);
expected.num_of_levels = 3;
expected.levels = { 0, 1, 1, 2, 2, 2, 1, 2, 1, 2, 0, 0, 1, 2, 2, 1, 1, 2 };
expected.delta.add(0, 'e', 1);
expected.delta.add(0, 'e', 2);
expected.delta.add(0, 'g', 6);
expected.delta.add(0, 'j', 8);
expected.delta.add(0, 'g', 12);
expected.delta.add(0, DONT_CARE, 13);
expected.delta.add(0, DONT_CARE, 15);
expected.delta.add(0, DONT_CARE, 16);
expected.delta.add(1, DONT_CARE, 14);
expected.delta.add(2, 'd', 3);
expected.delta.add(3, 'c', 10);
expected.delta.add(4, 'c', 10);
expected.delta.add(5, 'c', 11);
expected.delta.add(6, 'd', 7);
expected.delta.add(7, 'c', 11);
expected.delta.add(8, 'i', 9);
expected.delta.add(9, 'c', 11);
expected.delta.add(12, DONT_CARE, 17);
expected.delta.add(13, 'a', 10);
expected.delta.add(14, 'b', 10);
expected.delta.add(15, 'f', 4);
expected.delta.add(16, 'h', 5);
expected.delta.add(17, 'b', 11);

CHECK(aut_new.num_of_states() <= 18);
CHECK(aut_new.delta.num_of_transitions() <= 23);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}
}
}


Expand Down

0 comments on commit b1e5796

Please sign in to comment.