Commit ef6d175a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltltest: speed kind.test and consterm.test up

Fixes #52.

* src/ltltest/consterm.cc, src/ltltest/kind.cc: Rewrite to read a list
of input and expected output.
* src/ltltest/kind.test, src/ltltest/consterm.test: Adjust.
parent 2fc816c8
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
// Dévelopement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -18,6 +18,8 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include <fstream>
#include <sstream>
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
......@@ -36,21 +38,47 @@ main(int argc, char **argv)
if (argc != 2)
syntax(argv[0]);
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1);
std::ifstream input(argv[1]);
if (!input)
{
std::cerr << "failed to open " << argv[1] << '\n';
return 2;
}
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2;
std::string s;
while (std::getline(input, s))
{
if (s[0] == '#') // Skip comments
{
std::cerr << s << '\n';
continue;
}
std::istringstream ss(s);
std::string form;
bool expected;
std::getline(ss, form, ',');
ss >> expected;
bool b = f1->accepts_eword();
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse_sere(form, p1);
if (spot::ltl::format_parse_errors(std::cerr, form, p1))
return 2;
std::cout << b << std::endl;
bool b = f1->accepts_eword();
std::cout << form << ',' << b << '\n';
if (b != expected)
{
std::cerr << "computed '" << b
<< "' but expected '" << expected << "'\n";
return 2;
}
f1->destroy();
}
f1->destroy();
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::bunop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
return b;
return 0;
}
......@@ -25,26 +25,30 @@
set -e
run 0 ../consterm 'a'
run 0 ../consterm '1'
run 0 ../consterm '0'
run 1 ../consterm '[*0]'
run 1 ../consterm 'a*'
run 1 ../consterm '0*'
run 1 ../consterm 'a[*0]'
run 1 ../consterm 'a[*0..]'
run 1 ../consterm 'a[*0..3]'
run 0 ../consterm 'a[*1..3]'
run 0 ../consterm 'a[*3]'
run 1 ../consterm 'a[*..4][*3]'
run 0 ../consterm 'a[*1..4][*3]'
run 1 ../consterm 'a[*1..4][*0..3]'
run 0 ../consterm '((a ; b) + c)'
run 1 ../consterm '((a ; b) + [*0])'
run 0 ../consterm '((a ; b) + [*0]) & e'
run 1 ../consterm '((a ; b) + [*0]) & [*0]'
run 1 ../consterm '((a ; b) + [*0]) & (a* + b)'
run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}' # test braces
run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])'
run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])'
run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])'
cat >input2 <<EOF
1,0
0,0
[*0],1
a*,1
0*,1
a[*0],1
a[*0..],1
a[*0..3],1
a[*1..3],0
a[*3],0
a[*..4][*3],1
a[*1..4][*3],0
a[*1..4][*0..3],1
((a ; b) + c),0
((a ; b) + [*0]),1
((a ; b) + [*0]) & e,0
((a ; b) + [*0]) & [*0],1
((a ; b) + [*0]) & (a* + b),1
# test braces
{{a ; b} + {[*0]}} & {a* + b},1
(a + [*0]);(b + [*0]);(c + [*0]),1
(a + [*0]);(b + e);(c + [*0]),0
(a + [*0]);(b + e)*;(c + [*0]),1
EOF
run 0 ../consterm input2
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developement de
// l'Epita (LRDE).
// Copyright (C) 2010, 2012, 2015 Laboratoire de Recherche et
// Developement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -18,6 +18,8 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include <fstream>
#include <sstream>
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
......@@ -36,16 +38,44 @@ main(int argc, char **argv)
if (argc != 2)
syntax(argv[0]);
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
std::ifstream input(argv[1]);
if (!input)
{
std::cerr << "failed to open " << argv[1] << '\n';
return 2;
}
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2;
std::string s;
while (std::getline(input, s))
{
if (s[0] == '#') // Skip comments
{
std::cerr << s << '\n';
continue;
}
std::istringstream ss(s);
std::string form;
std::string expected;
std::getline(ss, form, ',');
std::getline(ss, expected);
spot::ltl::print_formula_props(std::cout, f1, true) << " = ";
spot::ltl::print_formula_props(std::cout, f1, false) << std::endl;
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse(form, p1);
if (spot::ltl::format_parse_errors(std::cerr, form, p1))
return 2;
f1->destroy();
std::ostringstream so;
spot::ltl::print_formula_props(so, f1, true);
auto sost = so.str();
std::cout << form << ',' << sost << '\n';
if (sost != expected)
{
std::cerr << "computed '" << sost
<< "' but expected '" << expected << "'\n";
return 2;
}
f1->destroy();
}
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
......
......@@ -25,135 +25,111 @@
set -e
check()
{
run 0 ../kind "$1" >out
read word rest <out
test "$word" = "$2"
}
cat >input<<EOF
a,B&!xfLEPSFsgopr
a<->b,BxfLEPSFsgopr
!a,B&!xfLEPSFsgopr
!(a|b),B&xfLEPSFsgopr
F(a),&!xLPegopr
G(a),&!xLPusopr
a U b,&!xfLPgopr
a U Fb,&!xLPegopr
Ga U b,&!xLPopr
1 U a,&!xfLPegopr
a W b,&!xfLPsopr
a W 0,&!xfLPusopr
a M b,&!xfLPgopr
a M 1,&!xfLPegopr
a R b,&!xfLPsopr
0 R b,&!xfLPusopr
a R (b R (c R d)),&!xfLPsopr
a U (b U (c U d)),&!xfLPgopr
a W (b W (c W d)),&!xfLPsopr
a M (b M (c M d)),&!xfLPgopr
Fa -> Fb,xLPopr
Ga -> Fb,xLPgopr
Fa -> Gb,xLPsopr
(Ga|Fc) -> Fb,xLPopr
(Ga|Fa) -> Gb,xLPopr
{a;c*;b}|->!Xb,&fPsopr
{a;c*;b}|->X!b,&!fPsopr
{a;c*;b}|->!Fb,&Psopr
{a;c*;b}|->G!b,&!Psopr
{a;c*;b}|->!Gb,&Pr
{a;c*;b}|->F!b,&!Pr
{a;c*;b}|->GFa,&!Pr
{a;c*;b}|->FGa,&!P
{a[+];c[+];b*}|->!Fb,&xPsopr
{a[+];c*;b[+]}|->G!b,&!xPsopr
{a*;c[+];b[+]}|->!Gb,&xPr
{a[+];c*;b[+]}|->F!b,&!xPr
{a[+];c[+];b*}|->GFa,&!xPr
{a*;c[+];b[+]}|->FGa,&!xP
{a;c;b|(d;e)}|->!Xb,&fPFsgopr
{a;c;b|(d;e)}|->X!b,&!fPFsgopr
{a;c;b|(d;e)}|->!Fb,&Psopr
{a;c;b|(d;e)}|->G!b,&!Psopr
{a;c;b|(d;e)}|->!Gb,&Pgopr
{a;c;b|(d;e)}|->F!b,&!Pgopr
{a;c;b|(d;e)}|->GFa,&!Pr
{a;c;b|(d;e)}|->FGa,&!Pp
{a[+] && c[+]}|->!Xb,&fPsopr
{a[+] && c[+]}|->X!b,&!fPsopr
{a[+] && c[+]}|->!Fb,&xPsopr
{a[+] && c[+]}|->G!b,&!xPsopr
{a[+] && c[+]}|->!Gb,&xPr
{a[+] && c[+]}|->F!b,&!xPr
{a[+] && c[+]}|->GFa,&!xPr
{a[+] && c[+]}|->FGa,&!xP
{a;c*;b}<>->!Gb,&Pgopr
{a;c*;b}<>->F!b,&!Pgopr
{a;c*;b}<>->FGb,&!Pp
{a;c*;b}<>->!GFb,&Pp
{a;c*;b}<>->GFb,&!P
{a;c*;b}<>->!FGb,&P
{a*;c[+];b[+]}<>->!FGb,&xP
{a;c|d;b}<>->!Gb,&Pgopr
{a;c|d;b}<>->G!b,&!Psopr
{a;c|d;b}<>->FGb,&!Pp
{a;c|d;b}<>->!GFb,&Pp
{a;c|d;b}<>->GFb,&!Pr
{a;c|d;b}<>->!FGb,&Pr
# Equivalent to a&b&c&d
{a:b:c:d}!,B&!xfLEPSFsgopr
a&b&c&d,B&!xfLEPSFsgopr
(Xa <-> XXXc) U (b & Fe),LPgopr
(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopr
(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopr
(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopr
(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopr
(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPp
(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPr
(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPp
(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPup
(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPr
(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPer
(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPep
(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LP
(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPur
(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LP
GFa M GFb,&!xLPeu
FGa M FGb,&!xLPeup
Fa M GFb,&!xLPer
GFa W GFb,&!xLPeur
FGa W FGb,&!xLPeu
Ga W FGb,&!xLPup
Ga W b,&!xLPsopr
Fa M b,&!xLPgopr
{a;b*;c},&!fPsopr
{a;b*;c}!,&!fPgopr
# The negative normal form is {a;b*;c}[]->1
!{a;b*;c}!,&fPsopr
{a;b*;c}[]->0,&!fPsopr
!{a;b*;c},&!fPgopr
!{a[+];b*;c[+]},&!xfPgopr
{a[+];b*;c[+]},&!xfPsopr
{a[+] && b || c[+]},&!fPsopr
{a[+] && b[+] || c[+]},&!xfPsopr
EOF
check 'a' 'B&!xfLEPSFsgopr'
check 'a<->b' 'BxfLEPSFsgopr'
check '!a' 'B&!xfLEPSFsgopr'
check '!(a|b)' 'B&xfLEPSFsgopr'
check 'F(a)' '&!xLPegopr'
check 'G(a)' '&!xLPusopr'
check 'a U b' '&!xfLPgopr'
check 'a U Fb' '&!xLPegopr'
check 'Ga U b' '&!xLPopr'
check '1 U a' '&!xfLPegopr'
check 'a W b' '&!xfLPsopr'
check 'a W 0' '&!xfLPusopr'
check 'a M b' '&!xfLPgopr'
check 'a M 1' '&!xfLPegopr'
check 'a R b' '&!xfLPsopr'
check '0 R b' '&!xfLPusopr'
check 'a R (b R (c R d))' '&!xfLPsopr'
check 'a U (b U (c U d))' '&!xfLPgopr'
check 'a W (b W (c W d))' '&!xfLPsopr'
check 'a M (b M (c M d))' '&!xfLPgopr'
check 'Fa -> Fb' 'xLPopr'
check 'Ga -> Fb' 'xLPgopr'
check 'Fa -> Gb' 'xLPsopr'
check '(Ga|Fc) -> Fb' 'xLPopr'
check '(Ga|Fa) -> Gb' 'xLPopr'
check '{a;c*;b}|->!Xb' '&fPsopr'
check '{a;c*;b}|->X!b' '&!fPsopr'
check '{a;c*;b}|->!Fb' '&Psopr'
check '{a;c*;b}|->G!b' '&!Psopr'
check '{a;c*;b}|->!Gb' '&Pr'
check '{a;c*;b}|->F!b' '&!Pr'
check '{a;c*;b}|->GFa' '&!Pr'
check '{a;c*;b}|->FGa' '&!P'
check '{a[+];c[+];b*}|->!Fb' '&xPsopr'
check '{a[+];c*;b[+]}|->G!b' '&!xPsopr'
check '{a*;c[+];b[+]}|->!Gb' '&xPr'
check '{a[+];c*;b[+]}|->F!b' '&!xPr'
check '{a[+];c[+];b*}|->GFa' '&!xPr'
check '{a*;c[+];b[+]}|->FGa' '&!xP'
check '{a;c;b|(d;e)}|->!Xb' '&fPFsgopr'
check '{a;c;b|(d;e)}|->X!b' '&!fPFsgopr'
check '{a;c;b|(d;e)}|->!Fb' '&Psopr'
check '{a;c;b|(d;e)}|->G!b' '&!Psopr'
check '{a;c;b|(d;e)}|->!Gb' '&Pgopr'
check '{a;c;b|(d;e)}|->F!b' '&!Pgopr'
check '{a;c;b|(d;e)}|->GFa' '&!Pr'
check '{a;c;b|(d;e)}|->FGa' '&!Pp'
check '{a[+] && c[+]}|->!Xb' '&fPsopr'
check '{a[+] && c[+]}|->X!b' '&!fPsopr'
check '{a[+] && c[+]}|->!Fb' '&xPsopr'
check '{a[+] && c[+]}|->G!b' '&!xPsopr'
check '{a[+] && c[+]}|->!Gb' '&xPr'
check '{a[+] && c[+]}|->F!b' '&!xPr'
check '{a[+] && c[+]}|->GFa' '&!xPr'
check '{a[+] && c[+]}|->FGa' '&!xP'
check '{a;c*;b}<>->!Gb' '&Pgopr'
check '{a;c*;b}<>->F!b' '&!Pgopr'
check '{a;c*;b}<>->FGb' '&!Pp'
check '{a;c*;b}<>->!GFb' '&Pp'
check '{a;c*;b}<>->GFb' '&!P'
check '{a;c*;b}<>->!FGb' '&P'
check '{a*;c[+];b[+]}<>->!FGb' '&xP'
check '{a;c|d;b}<>->!Gb' '&Pgopr'
check '{a;c|d;b}<>->G!b' '&!Psopr'
check '{a;c|d;b}<>->FGb' '&!Pp'
check '{a;c|d;b}<>->!GFb' '&Pp'
check '{a;c|d;b}<>->GFb' '&!Pr'
check '{a;c|d;b}<>->!FGb' '&Pr'
check '{a:b:c:d}!' 'B&!xfLEPSFsgopr' # Equivalent to a&b&c&d
check 'a&b&c&d' 'B&!xfLEPSFsgopr'
check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr'
check '(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b))' 'LPegopr'
check '(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b))' 'LPusopr'
check '(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b))' 'LPeopr'
check '(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b))' 'LPuopr'
check '(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b))' 'LPp'
check '(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b))' 'LPr'
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b))' 'LPp'
check '(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b))' 'LPup'
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b))' 'LPr'
check '(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b))' 'LPer'
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb))' 'LPep'
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb))' 'LP'
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb))' 'LPur'
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb))' 'LP'
check 'GFa M GFb' '&!xLPeu'
check 'FGa M FGb' '&!xLPeup'
check 'Fa M GFb' '&!xLPer'
check 'GFa W GFb' '&!xLPeur'
check 'FGa W FGb' '&!xLPeu'
check 'Ga W FGb' '&!xLPup'
check 'Ga W b' '&!xLPsopr'
check 'Fa M b' '&!xLPgopr'
check '{a;b*;c}' '&!fPsopr'
check '{a;b*;c}!' '&!fPgopr'
check '!{a;b*;c}!' '&fPsopr' # The negative normal form is {a;b*;c}[]->0
check '{a;b*;c}[]->0' '&!fPsopr'
check '!{a;b*;c}' '&!fPgopr'
check '!{a[+];b*;c[+]}' '&!xfPgopr'
check '{a[+];b*;c[+]}' '&!xfPsopr'
check '{a[+] && b || c[+]}' '&!fPsopr'
check '{a[+] && b[+] || c[+]}' '&!xfPsopr'
run 0 ../consterm '1'
run 0 ../consterm '0'
run 1 ../consterm '[*0]'
run 1 ../consterm 'a*'
run 1 ../consterm '0*'
run 1 ../consterm 'a[*0]'
run 1 ../consterm 'a[*0..]'
run 1 ../consterm 'a[*0..3]'
run 0 ../consterm 'a[*1..3]'
run 0 ../consterm 'a[*3]'
run 1 ../consterm 'a[*..4][*3]'
run 0 ../consterm 'a[*1..4][*3]'
run 1 ../consterm 'a[*1..4][*0..3]'
run 0 ../consterm '((a ; b) + c)'
run 1 ../consterm '((a ; b) + [*0])'
run 0 ../consterm '((a ; b) + [*0]) & e'
run 1 ../consterm '((a ; b) + [*0]) & [*0]'
run 1 ../consterm '((a ; b) + [*0]) & (a* + b)'
run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}' # test braces
run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])'
run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])'
run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])'
run 0 ../kind input
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment