acc: add a parser for string -> acc_code
* src/tgba/acc.cc, src/tgba/acc.hh (parse_acc_code): New function. * src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
This commit is contained in:
parent
c65bf731fd
commit
dfd080e005
4 changed files with 174 additions and 0 deletions
133
src/tgba/acc.cc
133
src/tgba/acc.cc
|
|
@ -19,7 +19,10 @@
|
||||||
|
|
||||||
|
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
#include <sstream>
|
||||||
#include <set>
|
#include <set>
|
||||||
|
#include <cctype>
|
||||||
|
#include <cstring>
|
||||||
#include "acc.hh"
|
#include "acc.hh"
|
||||||
#include "priv/bddalloc.hh"
|
#include "priv/bddalloc.hh"
|
||||||
#include "misc/minato.hh"
|
#include "misc/minato.hh"
|
||||||
|
|
@ -879,4 +882,134 @@ namespace spot
|
||||||
{
|
{
|
||||||
return code.to_text(os);
|
return code.to_text(os);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
namespace
|
||||||
|
{
|
||||||
|
|
||||||
|
/// acc ::= term | term "|" acc
|
||||||
|
/// term := "t" | "f" | "Inf" "(" num ")"
|
||||||
|
/// | "Fin" "(" num ") " | "(" acc ")
|
||||||
|
/// | term "&" term
|
||||||
|
|
||||||
|
static void skip_space(const char*& input)
|
||||||
|
{
|
||||||
|
while (std::isspace(*input))
|
||||||
|
++input;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Eat c and remove the following spaces.
|
||||||
|
// Complain if there is no c.
|
||||||
|
void expect(const char*& input, char c)
|
||||||
|
{
|
||||||
|
if (*input != c)
|
||||||
|
{
|
||||||
|
std::ostringstream s;
|
||||||
|
s << "syntax error at '" << input << "', was expecting " << c << '.';
|
||||||
|
throw parse_error(s.str());
|
||||||
|
}
|
||||||
|
++input;
|
||||||
|
skip_space(input);
|
||||||
|
}
|
||||||
|
|
||||||
|
static acc_cond::acc_code parse_term(const char*& input);
|
||||||
|
|
||||||
|
static acc_cond::acc_code parse_acc(const char*& input)
|
||||||
|
{
|
||||||
|
auto t = parse_term(input);
|
||||||
|
skip_space(input);
|
||||||
|
while (*input == '|')
|
||||||
|
{
|
||||||
|
++input;
|
||||||
|
skip_space(input);
|
||||||
|
t.append_or(parse_term(input));
|
||||||
|
}
|
||||||
|
return t;
|
||||||
|
}
|
||||||
|
|
||||||
|
static unsigned parse_num(const char*& input)
|
||||||
|
{
|
||||||
|
skip_space(input);
|
||||||
|
expect(input, '(');
|
||||||
|
|
||||||
|
errno = 0;
|
||||||
|
char* end;
|
||||||
|
unsigned long n = strtoul(input, &end, 10);
|
||||||
|
unsigned num = n;
|
||||||
|
if (errno || num != n)
|
||||||
|
{
|
||||||
|
std::ostringstream s;
|
||||||
|
s << "syntax error at '" << input << "': value too large.";
|
||||||
|
throw parse_error(s.str());
|
||||||
|
}
|
||||||
|
input = end;
|
||||||
|
|
||||||
|
skip_space(input);
|
||||||
|
expect(input, ')');
|
||||||
|
return num;
|
||||||
|
}
|
||||||
|
|
||||||
|
static acc_cond::acc_code parse_term(const char*& input)
|
||||||
|
{
|
||||||
|
acc_cond::acc_code res;
|
||||||
|
if (*input == 't')
|
||||||
|
{
|
||||||
|
++input;
|
||||||
|
res = acc_cond::acc_code::t();
|
||||||
|
}
|
||||||
|
else if (*input == 'f')
|
||||||
|
{
|
||||||
|
++input;
|
||||||
|
res = acc_cond::acc_code::f();
|
||||||
|
}
|
||||||
|
else if (*input == '(')
|
||||||
|
{
|
||||||
|
++input;
|
||||||
|
skip_space(input);
|
||||||
|
res = parse_acc(input);
|
||||||
|
skip_space(input);
|
||||||
|
expect(input, ')');
|
||||||
|
}
|
||||||
|
else if (!strncmp(input, "Inf", 3))
|
||||||
|
{
|
||||||
|
input += 3;
|
||||||
|
res = acc_cond::acc_code::inf({parse_num(input)});
|
||||||
|
}
|
||||||
|
else if (!strncmp(input, "Fin", 3))
|
||||||
|
{
|
||||||
|
input += 3;
|
||||||
|
res = acc_cond::acc_code::fin({parse_num(input)});
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
std::ostringstream s;
|
||||||
|
s << "syntax error at '" << input << "', unexpected character.";
|
||||||
|
throw parse_error(s.str());
|
||||||
|
}
|
||||||
|
|
||||||
|
skip_space(input);
|
||||||
|
while (*input == '&')
|
||||||
|
{
|
||||||
|
++input;
|
||||||
|
skip_space(input);
|
||||||
|
res.append_and(parse_term(input));
|
||||||
|
}
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
acc_cond::acc_code parse_acc_code(const char* input)
|
||||||
|
{
|
||||||
|
skip_space(input);
|
||||||
|
acc_cond::acc_code c = parse_acc(input);
|
||||||
|
if (*input)
|
||||||
|
{
|
||||||
|
std::ostringstream s;
|
||||||
|
s << "syntax error at '" << input << "', unexpected character.";
|
||||||
|
throw parse_error(s.str());
|
||||||
|
}
|
||||||
|
return c;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -968,6 +968,25 @@ namespace spot
|
||||||
bool uses_fin_acceptance_ = false;
|
bool uses_fin_acceptance_ = false;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
/// \brief Parse a string into an acc_code
|
||||||
|
///
|
||||||
|
/// The string should follow the following grammar:
|
||||||
|
///
|
||||||
|
/// <pre>
|
||||||
|
/// acc ::= "t"
|
||||||
|
/// | "f"
|
||||||
|
/// | "Inf" "(" num ")"
|
||||||
|
/// | "Fin" "(" num ")"
|
||||||
|
/// | "(" acc ")"
|
||||||
|
/// | acc "&" acc
|
||||||
|
/// | acc "|" acc
|
||||||
|
/// </pre>
|
||||||
|
///
|
||||||
|
/// Where num is an integer and "&" has priority over "|". Note that
|
||||||
|
/// "Fin(!x)" and "Inf(!x)" are not supported by this parser.
|
||||||
|
///
|
||||||
|
/// A spot::parse_error is thrown on syntax error.
|
||||||
|
SPOT_API acc_cond::acc_code parse_acc_code(const char* input);
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace std
|
namespace std
|
||||||
|
|
|
||||||
|
|
@ -127,4 +127,18 @@ int main()
|
||||||
auto code3 = ac.inf({0, 1});
|
auto code3 = ac.inf({0, 1});
|
||||||
code3.append_and(ac.fin({2, 3}));
|
code3.append_and(ac.fin({2, 3}));
|
||||||
std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n';
|
std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n';
|
||||||
|
|
||||||
|
|
||||||
|
std::cout << spot::parse_acc_code("t") << '\n';
|
||||||
|
std::cout << spot::parse_acc_code("f") << '\n';
|
||||||
|
std::cout << spot::parse_acc_code("Fin(2)") << '\n';
|
||||||
|
std::cout << spot::parse_acc_code("Inf(2)") << '\n';
|
||||||
|
std::cout << spot::parse_acc_code("Fin(2) | Inf(2)") << '\n';
|
||||||
|
std::cout << spot::parse_acc_code("Inf(2) & Fin(2)") << '\n';
|
||||||
|
auto c1 = spot::parse_acc_code("Fin(0)|Inf(1)&Fin(2)|Fin(3)");
|
||||||
|
auto c2 = spot::parse_acc_code
|
||||||
|
("( Fin ( 0 )) | (Inf ( 1) & Fin(2 ))| Fin (3) ");
|
||||||
|
std::cout << c1 << '\n';
|
||||||
|
std::cout << c2 << '\n';
|
||||||
|
assert(c1 == c2);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -68,6 +68,14 @@ stripping
|
||||||
2 f 1
|
2 f 1
|
||||||
9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
|
||||||
5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
|
5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
|
||||||
|
t
|
||||||
|
f
|
||||||
|
Fin(2)
|
||||||
|
Inf(2)
|
||||||
|
Inf(2) | Fin(2)
|
||||||
|
Fin(2) & Inf(2)
|
||||||
|
Fin(3) | (Fin(2) & Inf(1)) | Fin(0)
|
||||||
|
Fin(3) | (Fin(2) & Inf(1)) | Fin(0)
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
run 0 ../acc | tee stdout
|
run 0 ../acc | tee stdout
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue