tests: rewrite the syntimpl test
* tests/core/syntimpl.cc: Rewrite to test multiple formulas at once, and test them with three different implication checks. * tests/core/syntimpl.test: Adjust the test to execute syntimpl only once.
This commit is contained in:
Alexandre Duret-Lutz
parent
99a622059c
commit
4ccdcb4a5b
2 changed files with 109 additions and 131 deletions
|
|
@ -18,85 +18,74 @@
|
||||||
|
|
||||||
#include "config.h"
|
#include "config.h"
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
#include <fstream>
|
||||||
|
#include <sstream>
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
#include <cstdlib>
|
#include <cstdlib>
|
||||||
|
#include <cstring>
|
||||||
#include <spot/tl/parse.hh>
|
#include <spot/tl/parse.hh>
|
||||||
#include <spot/tl/print.hh>
|
|
||||||
#include <spot/tl/simplify.hh>
|
|
||||||
#include <spot/tl/nenoform.hh>
|
#include <spot/tl/nenoform.hh>
|
||||||
|
#include <spot/tl/simplify.hh>
|
||||||
|
#include <spot/tl/print.hh>
|
||||||
|
|
||||||
static void
|
static void
|
||||||
syntax(char* prog)
|
syntax(char* prog)
|
||||||
{
|
{
|
||||||
std::cerr << prog << " formula1 formula2?\n";
|
std::cerr << prog << " file\n";
|
||||||
exit(2);
|
exit(2);
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
if (argc < 4)
|
if (argc != 2)
|
||||||
syntax(argv[0]);
|
syntax(argv[0]);
|
||||||
|
std::ifstream input(argv[1]);
|
||||||
int opt = atoi(argv[1]);
|
if (!input)
|
||||||
int exit_return = 0;
|
{
|
||||||
|
std::cerr << "failed to open " << argv[1] << '\n';
|
||||||
{
|
|
||||||
auto ftmp1 = spot::parse_infix_psl(argv[2]);
|
|
||||||
|
|
||||||
if (ftmp1.format_errors(std::cerr))
|
|
||||||
return 2;
|
return 2;
|
||||||
|
}
|
||||||
|
|
||||||
auto ftmp2 = spot::parse_infix_psl(argv[3]);
|
spot::tl_simplifier* c = new spot::tl_simplifier;
|
||||||
|
std::string s;
|
||||||
|
unsigned line = 0;
|
||||||
|
while (std::getline(input, s))
|
||||||
|
{
|
||||||
|
++line;
|
||||||
|
std::cerr << line << ": " << s << '\n';
|
||||||
|
if (s[0] == '#') // Skip comments
|
||||||
|
continue;
|
||||||
|
|
||||||
if (ftmp2.format_errors(std::cerr))
|
spot::formula f[2];
|
||||||
return 2;
|
std::istringstream ss(s);
|
||||||
|
for (unsigned i = 0; i < 2; ++i)
|
||||||
spot::formula f1 = spot::negative_normal_form(ftmp1.f);
|
{
|
||||||
spot::formula f2 = spot::negative_normal_form(ftmp2.f);
|
std::string form;
|
||||||
|
if (!std::getline(ss, form, ','))
|
||||||
std::string f1s = spot::str_psl(f1);
|
{
|
||||||
std::string f2s = spot::str_psl(f2);
|
std::cerr << "missing first formula\n";
|
||||||
|
exit(2);
|
||||||
spot::tl_simplifier* c = new spot::tl_simplifier;
|
}
|
||||||
|
std::string tmp;
|
||||||
switch (opt)
|
while (form.size() > 0 && form.back() == '\\'
|
||||||
{
|
&& std::getline(ss, tmp, ','))
|
||||||
case 0:
|
{
|
||||||
std::cout << "Test f1 < f2" << std::endl;
|
form.back() = ',';
|
||||||
if (c->syntactic_implication(f1, f2))
|
form += tmp;
|
||||||
{
|
}
|
||||||
std::cout << f1s << " < " << f2s << '\n';
|
auto pf = spot::parse_infix_psl(form);
|
||||||
exit_return = 1;
|
if (pf.format_errors(std::cerr))
|
||||||
}
|
return 2;
|
||||||
break;
|
f[i] = spot::negative_normal_form(pf.f);
|
||||||
|
}
|
||||||
case 1:
|
// ignore the rest of the line
|
||||||
std::cout << "Test !f1 < f2" << std::endl;
|
std::cout << spot::str_psl(f[0]) << ',' << spot::str_psl(f[1]) << ','
|
||||||
if (c->syntactic_implication_neg(f1, f2, false))
|
<< c->syntactic_implication(f[0], f[1]) << ','
|
||||||
{
|
<< c->syntactic_implication_neg(f[0], f[1], false) << ','
|
||||||
std::cout << "!(" << f1s << ") < " << f2s << '\n';
|
<< c->syntactic_implication_neg(f[0], f[1], true) << '\n';
|
||||||
exit_return = 1;
|
}
|
||||||
}
|
delete c;
|
||||||
break;
|
|
||||||
|
|
||||||
case 2:
|
|
||||||
std::cout << "Test f1 < !f2" << std::endl;
|
|
||||||
if (c->syntactic_implication_neg(f1, f2, true))
|
|
||||||
{
|
|
||||||
std::cout << f1s << " < !(" << f2s << ")\n";
|
|
||||||
exit_return = 1;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
f1.dump(std::cout) << '\n';
|
|
||||||
f2.dump(std::cout) << '\n';
|
|
||||||
|
|
||||||
delete c;
|
|
||||||
}
|
|
||||||
assert(spot::fnode::instances_check());
|
assert(spot::fnode::instances_check());
|
||||||
return exit_return;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -22,74 +22,63 @@
|
||||||
|
|
||||||
. ./defs || exit 1
|
. ./defs || exit 1
|
||||||
|
|
||||||
#
|
|
||||||
#GFa && GFb && FG(!a && !b)
|
|
||||||
run 1 ../syntimpl 0 'a' 'a | b'
|
|
||||||
run 1 ../syntimpl 0 'F(a)' 'F(a | b)'
|
|
||||||
run 1 ../syntimpl 0 'G(a)' 'G(a | b)'
|
|
||||||
run 1 ../syntimpl 0 'GF(a)' 'GF(a | b)'
|
|
||||||
run 1 ../syntimpl 0 'GF(a)' '!FG(!a && !b)'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'Xa' 'X(b U a)'
|
cat >input <<EOF
|
||||||
run 1 ../syntimpl 0 'XXa' 'XX(b U a)'
|
a,a | b,1,0,0
|
||||||
|
Fa,F(a | b),1,0,0
|
||||||
|
Ga,G(a | b),1,0,0
|
||||||
|
GFa,GF(a | b),1,0,0
|
||||||
|
GFa,GF(a | b),1,0,0
|
||||||
|
Xa,X(b U a),1,0,0
|
||||||
|
XXa,XX(b U a),1,0,0
|
||||||
|
e R f,g U f,1,0,0
|
||||||
|
X(a | b),X(a | b | c | d),1,0,0
|
||||||
|
X(a | b) U (e R f),X(a | b | c | d) U (g U f),1,0,0
|
||||||
|
1,1,1,1,0
|
||||||
|
0,0,1,0,1
|
||||||
|
a,1,1,1,0
|
||||||
|
a,a,1,0,0
|
||||||
|
a,!a,0,1,1
|
||||||
|
!a,1,1,1,0
|
||||||
|
a,a,1,0,0
|
||||||
|
a & b,b,1,0,0
|
||||||
|
a & b,a,1,0,0
|
||||||
|
!a,a & b,0,0,1
|
||||||
|
a,a & b,0,0,0
|
||||||
|
a,!a | !b,0,1,0
|
||||||
|
a,a | b,1,0,0
|
||||||
|
b,a | b,1,0,0
|
||||||
|
a | b,1,1,1,0
|
||||||
|
a,b U a,1,0,0
|
||||||
|
a,1,1,1,0
|
||||||
|
a U b,1,1,1,0
|
||||||
|
a,a,1,0,0
|
||||||
|
a,1,1,1,0
|
||||||
|
a R b,b,1,0,0
|
||||||
|
a R b,1,1,1,0
|
||||||
|
Xa,X(b U a),1,0,0
|
||||||
|
X(a R b),Xb,1,0,0
|
||||||
|
a U b,1 U b,1,0,0
|
||||||
|
a R b,b,1,0,0
|
||||||
|
b & (a U b),a U b,1,0,0
|
||||||
|
a U b,c | (a U b),1,0,0
|
||||||
|
Xa,XX(b U a),0,0,0
|
||||||
|
XXa,X(b U a),0,0,0
|
||||||
|
X(a | b),X(c | d | X(a | b)),0,0,0
|
||||||
|
X(a | b) U (e R f),X(c | d | X(a | b)) U (g U f),0,0,0
|
||||||
|
a,b,0,0,0
|
||||||
|
a,b | c,0,0,0
|
||||||
|
a | b,a,0,0,0
|
||||||
|
a,a & c,0,0,0
|
||||||
|
a & b,c,0,0,0
|
||||||
|
a,a U b,0,0,0
|
||||||
|
a,a R b,0,0,0
|
||||||
|
a R b,a,0,0,0
|
||||||
|
p2,p3 | G(p2 & p5),0,0,0
|
||||||
|
!p3 & F(!p2 | !p5),!p2,0,0,0
|
||||||
|
Xc W 0,Xc R b,0,0,0
|
||||||
|
(b & c) W (a & b),a R b,1,0,0
|
||||||
|
EOF
|
||||||
|
|
||||||
run 1 ../syntimpl 0 '(e R f)' '(g U f)'
|
run 0 ../syntimpl input > output
|
||||||
run 1 ../syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
|
diff input output
|
||||||
run 1 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 '1' '1'
|
|
||||||
run 1 ../syntimpl 0 '0' '0'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a' '1'
|
|
||||||
run 1 ../syntimpl 0 'a' 'a'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a' 'a & 1'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a & b' 'b'
|
|
||||||
run 1 ../syntimpl 0 'a & b' 'a'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a' 'a + b'
|
|
||||||
run 1 ../syntimpl 0 'b' 'a + b'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a + b' '1'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a' 'b U a'
|
|
||||||
run 1 ../syntimpl 0 'a' 'b U 1'
|
|
||||||
run 1 ../syntimpl 0 'a U b' '1'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a' '1 R a'
|
|
||||||
run 1 ../syntimpl 0 'a' 'a R 1'
|
|
||||||
run 1 ../syntimpl 0 'a R b' 'b'
|
|
||||||
run 1 ../syntimpl 0 'a R b' '1'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'Xa' 'X(b U a)'
|
|
||||||
run 1 ../syntimpl 0 'X(a R b)' 'Xb'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'a U b' '1 U b'
|
|
||||||
run 1 ../syntimpl 0 'a R b' '1 R b'
|
|
||||||
|
|
||||||
run 1 ../syntimpl 0 'b & (a U b)' 'a U b'
|
|
||||||
run 1 ../syntimpl 0 'a U b' 'c + (a U b)'
|
|
||||||
|
|
||||||
run 0 ../syntimpl 0 'Xa' 'XX(b U a)'
|
|
||||||
run 0 ../syntimpl 0 'XXa' 'X(b U a)'
|
|
||||||
|
|
||||||
run 0 ../syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
|
|
||||||
run 0 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
|
|
||||||
|
|
||||||
run 0 ../syntimpl 0 'a' 'b'
|
|
||||||
run 0 ../syntimpl 0 'a' 'b + c'
|
|
||||||
run 0 ../syntimpl 0 'a + b' 'a'
|
|
||||||
run 0 ../syntimpl 0 'a' 'a & c'
|
|
||||||
run 0 ../syntimpl 0 'a & b' 'c'
|
|
||||||
run 0 ../syntimpl 0 'a' 'a U b'
|
|
||||||
run 0 ../syntimpl 0 'a' 'a R b'
|
|
||||||
run 0 ../syntimpl 0 'a R b' 'a'
|
|
||||||
|
|
||||||
run 0 ../syntimpl 0 'p2' 'p3 || G(p2 && p5)'
|
|
||||||
run 0 ../syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
|
|
||||||
|
|
||||||
run 0 ../syntimpl 0 'Xc W 0' 'Xc R b'
|
|
||||||
run 1 ../syntimpl 0 '(c&b) W (b&a)' 'a R b'
|
|
||||||
|
|
||||||
exit 0
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue