From ef6d175acea6aff5a293ce7d90809d2a7843bfa5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Jan 2015 20:43:21 +0100 Subject: [PATCH] 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. --- src/ltltest/consterm.cc | 46 ++++++-- src/ltltest/consterm.test | 50 ++++---- src/ltltest/kind.cc | 48 ++++++-- src/ltltest/kind.test | 238 +++++++++++++++++--------------------- 4 files changed, 210 insertions(+), 172 deletions(-) diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc index 53ab45286..de49de882 100644 --- a/src/ltltest/consterm.cc +++ b/src/ltltest/consterm.cc @@ -1,5 +1,5 @@ // -*- 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 . #include +#include +#include #include #include #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; } diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index d1b840a8f..f95a1710f 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -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 <. #include +#include +#include #include #include #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); diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 8d1d78812..e7dc64ff5 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -25,135 +25,111 @@ set -e -check() -{ - run 0 ../kind "$1" >out - read word rest input<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