Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proper handling of constants (true/false) #330

Merged
merged 1 commit into from
Sep 13, 2023
Merged

Proper handling of constants (true/false) #330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions include/mata/parser/inter-aut.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ public:
SYMBOL,
STATE,
NODE,
TRUE,
FALSE,
NOT_OPERAND
};

Expand Down Expand Up @@ -88,9 +90,9 @@ public:
bool is_neg() const { return type == Type::OPERATOR && operator_type == OperatorType::NEG; }

// TODO: should constant be its own operand type?
bool is_constant() const { return type == Type::OPERAND && (name == "true" || name == "false"); }
bool is_true() const { return type == Type::OPERAND && name == "true"; }
bool is_false() const { return type == Type::OPERAND && name == "false"; }
bool is_constant() const { return is_true() || is_false(); }
bool is_true() const { return is_operand() && operand_type == OperandType::TRUE; }
bool is_false() const { return is_operand() && operand_type == OperandType::FALSE; }

FormulaNode()
: type(Type::UNKNOWN), raw(), name(), operator_type(OperatorType::NOT_OPERATOR),
Expand Down
8 changes: 4 additions & 4 deletions src/inter-aut.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,12 +149,12 @@
return { mata::FormulaNode::Type::LEFT_PARENTHESIS, token};
} else if (token == ")") {
return { mata::FormulaNode::Type::RIGHT_PARENTHESIS, token};
} else if (token == "true") {
} else if (token == "\\true") {
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
} else if (token == "false") {
mata::FormulaNode::OperandType::TRUE};
} else if (token == "\\false") {
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
mata::FormulaNode::OperandType::FALSE};
} else if (is_naming_enum(mata.state_naming) && contains(mata.states_names, token)) {
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::STATE};
Expand All @@ -168,7 +168,7 @@
return { mata::FormulaNode::Type::OPERAND, token, token.substr(1),
mata::FormulaNode::OperandType::STATE};
} else if (is_naming_marker(mata.node_naming) && token[0] == 'n') {
return { mata::FormulaNode::Type::OPERAND, token, token.substr(1),

Check warning on line 171 in src/inter-aut.cc

View check run for this annotation

Codecov / codecov/patch

src/inter-aut.cc#L171 

Added line #L171 was not covered by tests
mata::FormulaNode::OperandType::NODE};
} else if (is_naming_marker(mata.symbol_naming) && token[0] == 'a') {
return { mata::FormulaNode::Type::OPERAND, token, token.substr(1),
Expand Down
8 changes: 4 additions & 4 deletions src/mintermization.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,8 +153,8 @@ mata::Mintermization::OptionalBdd mata::Mintermization::graph_to_bdd_afa(const F
if (symbol_to_bddvar.count(node.name)) {
return OptionalBdd(symbol_to_bddvar.at(node.name));
} else {
BDD res = (node.name == "true") ? bdd_mng.bddOne() :
(node.name == "false" ? bdd_mng.bddZero() : bdd_mng.bddVar());
BDD res = (node.is_true()) ? bdd_mng.bddOne() :
(node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar());
symbol_to_bddvar[node.name] = res;
return OptionalBdd(res);
}
Expand Down Expand Up @@ -189,8 +189,8 @@ BDD mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph &graph)
if (symbol_to_bddvar.count(node.name)) {
return symbol_to_bddvar.at(node.name);
} else {
BDD res = (node.name == "true") ? bdd_mng.bddOne() :
(node.name == "false" ? bdd_mng.bddZero() : bdd_mng.bddVar());
BDD res = (node.is_true()) ? bdd_mng.bddOne() :
(node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar());
symbol_to_bddvar[node.name] = res;
return res;
}
Expand Down
20 changes: 10 additions & 10 deletions tests/mintermization.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ TEST_CASE("mata::Mintermization::mintermization")
std::string file =
"@AFA-bits\n"
"%Initial (q0) & ((q1 & q1' & q3 & q3'))\n"
"%Final true & (!q3' | (!q1))\n"
"%Final \\true & (!q3' | (!q1))\n"
"q1 (!a0 & !a1 & (q2))\n"
"q1 (a1 & !a2 & (q3))\n"
"q1' q1'\n"
Expand Down Expand Up @@ -244,7 +244,7 @@ TEST_CASE("mata::Mintermization::mintermization")
std::string file =
"@AFA-bits\n"
"%Initial (q0) & ((q1 & q1' & q3 & q3'))\n"
"%Final true & (!q3' | (!q1))\n"
"%Final \\true & (!q3' | (!q1))\n"
"q1 (!a0 & !a1 & !a2 & !a3 & (q2))\n"
"q0 (a4 & !a5 & !a6 & !a7 & (q0)) | (!a4 & a5 & !a6 & !a7 & (q1)) | (a4 & a5 & !a6 & !a7 & (q2))\n"
"q1' q1'\n"
Expand Down Expand Up @@ -287,7 +287,7 @@ TEST_CASE("mata::Mintermization::mintermization")
std::string file =
"@AFA-bits\n"
"%Initial (q0) & ((q1 & q1' & q3 & q3'))\n"
"%Final true & (!q3' | (!q1))\n"
"%Final \\true & (!q3' | (!q1))\n"
"q1 (!a0 & !a1 & !a2 & !a3 & (q2))\n"
"q0 (a4 & !a5 & !a6 & !a7 & (q0)) | (!a4 & a5 & !a6 & !a7 & (q0)) | (a4 & a5 & !a6 & !a7 & (q0)) | (!a4 & !a5 & a6 & !a7 & (q0)) | (a4 & !a5 & a6 & !a7 & (q0)) | (!a4 & a5 & a6 & !a7 & (q0)) | (a4 & a5 & a6 & !a7 & (q0)) | (!a4 & !a5 & !a6 & a7 & (q0)) | (a4 & !a5 & !a6 & a7 & (q0)) | (!a4 & a5 & !a6 & a7 & (q0)) | (a4 & a5 & !a6 & a7 & (q0)) | (!a4 & !a5 & a6 & a7 & (q0)) | (!a4 & !a5 & !a6 & !a7 & (q0)) | (a4 & !a5 & a6 & a7 & (q0))\n"
"q3 (a8 & !a9 & !a10 & !a11 & (q3)) | (!a8 & a9 & !a10 & !a11 & (q3)) | (a8 & a9 & !a10 & !a11 & (q3)) | (!a8 & !a9 & a10 & !a11 & (q3)) | (a8 & !a9 & a10 & !a11 & (q3)) | (!a8 & a9 & a10 & !a11 & (q3)) | (a8 & a9 & a10 & !a11 & (q3)) | (!a8 & !a9 & !a10 & a11 & (q3)) | (a8 & !a9 & !a10 & a11 & (q3)) | (!a8 & a9 & !a10 & a11 & (q3)) | (a8 & a9 & !a10 & a11 & (q3)) | (!a8 & !a9 & a10 & a11 & (q3)) | (!a8 & !a9 & !a10 & !a11 & (q3)) | (a8 & !a9 & a10 & a11 & (q3))\n"
Expand All @@ -312,7 +312,7 @@ TEST_CASE("mata::Mintermization::mintermization")
std::string file =
"@AFA-bits\n"
"%Initial (q0) & ((q1 & q1' & q3 & q3'))\n"
"%Final true & (!q3' | (!q1))\n"
"%Final \\true & (!q3' | (!q1))\n"
"q1 (!a0 & !a1 & !a2 & !a3 & (q2 & q3 & q0))\n"
"q0 (a4 & !a5 & !a6 & !a7 & (q0 & q1 & q1')) | (!a4 & a5 & !a6 & !a7 & (q1)) | (a4 & a5 & !a6 & !a7 & q2 & q1')\n"
"q1' q1'\n"
Expand Down Expand Up @@ -388,15 +388,15 @@ TEST_CASE("mata::Mintermization::mintermization")
"%Alphabet-auto\n"
"%Initial q\n"
"%Final r\n"
"q true r\n"
"q \\true r\n"
"r a1 & a2 s\n"
"s false s\n";
"s \\false s\n";

parsed = parse_mf(file);
std::vector<mata::IntermediateAut> auts = mata::IntermediateAut::parse_from_mf(parsed);
const auto &aut = auts[0];
REQUIRE(aut.transitions[0].second.children[0].node.is_operand());
REQUIRE(aut.transitions[0].second.children[0].node.raw == "true");
REQUIRE(aut.transitions[0].second.children[0].node.raw == "\\true");
REQUIRE(aut.transitions[0].second.children[1].node.is_operand());
REQUIRE(aut.transitions[0].second.children[1].node.raw == "r");

Expand All @@ -413,10 +413,10 @@ TEST_CASE("mata::Mintermization::mintermization")
"@AFA-bits\n"
"%Initial q0\n"
"%Final q3\n"
"q0 (true & q2 & q3 & q0) | (a4 & !a5 & !a6 & !a7 & q0 & q1 & q2)\n"
"q1 false\n"
"q0 (\\true & q2 & q3 & q0) | (a4 & !a5 & !a6 & !a7 & q0 & q1 & q2)\n"
"q1 \\false\n"
"q2 q1\n"
"q3 true\n";
"q3 \\true\n";

parsed = parse_mf(file);
std::vector<mata::IntermediateAut> auts = mata::IntermediateAut::parse_from_mf(parsed);
Expand Down
4 changes: 2 additions & 2 deletions tests/nfa/nfa.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -765,7 +765,7 @@ TEST_CASE("mata::nfa::construct() from IntermediateAut correct calls")
"@NFA-bits\n"
"%Alphabet-auto\n"
"%Initial q0 q8\n"
"%Final true\n"
"%Final \\true\n"
"q0 a1 q1\n"
"q1 a2 q2\n"
"q2 a3 q3\n"
Expand Down Expand Up @@ -797,7 +797,7 @@ TEST_CASE("mata::nfa::construct() from IntermediateAut correct calls")
"@NFA-bits\n"
"%Alphabet-auto\n"
"%Initial q0 q8\n"
"%Final false\n"
"%Final \\false\n"
"q0 a1 q1\n"
"q1 a2 q2\n"
"q2 a3 q3\n"
Expand Down
19 changes: 19 additions & 0 deletions tests/parser.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -833,6 +833,25 @@ TEST_CASE("parsing automata to intermediate representation")
REQUIRE(final_states.count("8"));
}

SECTION("NFA - true/false constants")
{
std::string file =
R"(@NFA-bits
%Alphabet-auto
%Initial q1
%Final \true
q0 \true q1
q1 \false q2
)";

const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file));
const mata::IntermediateAut inter_aut = auts[0];

CHECK(inter_aut.final_formula.node.is_true());
CHECK(inter_aut.transitions.at(0).second.children.at(0).node.is_true());
CHECK(inter_aut.transitions.at(1).second.children.at(0).node.is_false());
}

SECTION("AFA explicit")
{
std::string file =
Expand Down
Loading