From 9502266f9516d9c1757bd9ff6f10417aa6e167db Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 17 Aug 2014 19:43:54 +0200 Subject: [PATCH] tgbatest: implement a large part of ltl2tgba.test in c++ So that running valgrind is a lot more efficient. Running ltl2tgba.test using to take more than 15min. We are now down to 25sec. * src/tgbatest/checkpsl.cc: New file. * src/tgbatest/Makefile.am: Add it. * src/tgbatest/ltl2tgba.test: Adjust. --- src/tgbatest/.gitignore | 1 + src/tgbatest/Makefile.am | 2 + src/tgbatest/checkpsl.cc | 132 +++++++++++++++++++++++++++++++++++++ src/tgbatest/ltl2tgba.test | 125 ++++++++++++++++------------------- 4 files changed, 190 insertions(+), 70 deletions(-) create mode 100644 src/tgbatest/checkpsl.cc diff --git a/src/tgbatest/.gitignore b/src/tgbatest/.gitignore index 36469b686..7ea3d63dc 100644 --- a/src/tgbatest/.gitignore +++ b/src/tgbatest/.gitignore @@ -1,5 +1,6 @@ bddprod blue_counter +checkpsl complement defs .deps diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index dd375089a..e81e7cf7d 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -33,6 +33,7 @@ check_SCRIPTS = defs check_PROGRAMS = \ bitvect \ complement \ + checkpsl \ expldot \ explprod \ intvcomp \ @@ -47,6 +48,7 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bitvect_SOURCES = bitvect.cc +checkpsl_SOURCES = checkpsl.cc complement_SOURCES = complementation.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc new file mode 100644 index 000000000..7767ffd14 --- /dev/null +++ b/src/tgbatest/checkpsl.cc @@ -0,0 +1,132 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include +#include +#include +#include +#include +#include "ltlparse/public.hh" +#include "ltlast/allnodes.hh" +#include "tgba/futurecondcol.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/ltl2taa.hh" +#include "tgbaalgos/sccfilter.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/dupexp.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " file" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + if (argc != 2) + syntax(argv[0]); + std::ifstream input(argv[1]); + if (!input) + { + std::cerr << "failed to open " << argv[1] << '\n'; + return 2; + } + + + auto d = spot::make_bdd_dict(); + + std::string s; + unsigned line = 0; + while (std::getline(input, s)) + { + ++line; + std::cerr << line << ": " << s << '\n'; + if (s.empty() || s[0] == '#') // Skip comments + continue; + + spot::ltl::parse_error_list pe; + auto fpos = spot::ltl::parse(s, pe); + + if (spot::ltl::format_parse_errors(std::cerr, s, pe)) + return 2; + + auto fneg = + spot::ltl::unop::instance(spot::ltl::unop::Not, fpos->clone()); + + { + auto apos = scc_filter(ltl_to_tgba_fm(fpos, d)); + auto aneg = scc_filter(ltl_to_tgba_fm(fneg, d)); + auto ec = spot::couvreur99(spot::product(apos, aneg)); + auto res = ec->check(); + if (res) + { + std::cerr << "non-empty intersection between pos and neg (FM)\n"; + exit(2); + } + delete ec; + + // Run make_future_conditions_collector, without testing the output. + auto fc = spot::make_future_conditions_collector(apos, true); + spot::dotty_reachable(std::cout, fc); + } + + { + auto apos = scc_filter(ltl_to_tgba_fm(fpos, d, true)); + auto aneg = scc_filter(ltl_to_tgba_fm(fneg, d, true)); + auto ec = spot::couvreur99(spot::product(apos, aneg)); + auto res = ec->check(); + if (res) + { + std::cerr << "non-empty intersection between pos and neg (FM -x)\n"; + exit(2); + } + delete ec; + } + + if (fpos->is_ltl_formula()) + { + auto apos = scc_filter(spot::tgba_dupexp_dfs(ltl_to_taa(fpos, d))); + auto aneg = scc_filter(spot::tgba_dupexp_dfs(ltl_to_taa(fneg, d))); + auto ec = spot::couvreur99(spot::product(apos, aneg)); + auto res = ec->check(); + if (res) + { + std::cerr << "non-empty intersection between pos and neg (TAA)\n"; + exit(2); + } + delete ec; + } + fpos->destroy(); + fneg->destroy(); + } + + spot::ltl::atomic_prop::dump_instances(std::cerr); + spot::ltl::unop::dump_instances(std::cerr); + spot::ltl::binop::dump_instances(std::cerr); + spot::ltl::multop::dump_instances(std::cerr); + 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::multop::instance_count() == 0); + return 0; +} diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index ce0e62159..7724f2cf0 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -26,97 +26,82 @@ set -e -check_psl () -{ - # We don't check the output, but just running these might be enough to - # trigger assertions. - run 0 ../ltl2tgba -f -FC "$1" - # Make cross products with FM - run 0 ../ltl2tgba -f -R3 -b "$1" > out.tgba - run 0 ../ltl2tgba -f -R3 -Pout.tgba -E "!($1)" - run 0 ../ltl2tgba -f -x -R3 -b "$1" > out.tgba - run 0 ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)" -} +cat >check.txt <<\EOF +a +a U b +X a +a & b & c +a | b | (c U (d & (g U (h ^ i)))) +Xa & (b U !a) & (b U !a) +Fa & Xb & GFc & Gd +Fa & Xa & GFc & Gc +Fc & X(a | Xb) & GF(a | Xb) & Gc +a R (b R c) +(a U b) U (c U d) -check_ltl () -{ - check_psl "$@" - # Make cross products with TAA - run 0 ../ltl2tgba -taa -R3 -b "$1" > out.tgba - run 0 ../ltl2tgba -taa -R3 -Pout.tgba -E "!($1)" -} +((Xp2)U(X(1)))&(p1 R(p2 R p0)) -check_ltl a -check_ltl 'a U b' -check_ltl 'X a' -check_ltl 'a & b & c' -check_ltl 'a | b | (c U (d & (g U (h ^ i))))' -check_ltl 'Xa & (b U !a) & (b U !a)' -check_ltl 'Fa & Xb & GFc & Gd' -check_ltl 'Fa & Xa & GFc & Gc' -check_ltl 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check_ltl 'a R (b R c)' -check_ltl '(a U b) U (c U d)' - -check_ltl '((Xp2)U(X(1)))&(p1 R(p2 R p0))' - -check_psl '{a*;c}<>->GFb' -check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x' -check_psl '{(g;y;r)*}<>->x' -check_psl 'G({(g;y;r)*}<>->x)' -check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' -check_psl 'G({{a;b}*}[]->x)&G({{c;d}*}[]->y)' # try sub-braces -check_psl '{([*0] + a):c*:([*0] + b)}<>->d' -check_psl '{a;e;f:(g*);h}<>->d' -check_psl '{(a:b)* & (c*:d)}<>->e' -check_psl '{(a:b)*}' -check_psl 'G{(a:b)*}' -check_psl '{a;b}' -check_psl '{(a;b)*}' -check_psl 'G{(a;b)*}' -check_psl '{a*}[]->{b*}' -check_psl '{a*}[]=>{b*}' -check_psl '{a*&b}' -check_psl '{a*&b*}' -check_psl '{((!c;b*) & d);e}' -check_psl '{(a* & (c;b*) & d);e}' -check_psl '{[*2];a[*2..4]}|->b' -check_psl '{a[*2..5] && b[*..3]}|->c' -check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c' -check_psl '{(a[->3]) & {[+];b}}<>->c' +{a*;c}<>->GFb +{((a*;b;c)*)&((b*;a;c)*)}<>->x +{(g;y;r)*}<>->x +G({(g;y;r)*}<>->x) +G({(a;b)*}<>->x)&G({(c;d)*}<>->y) +# try sub-braces +G({{a;b}*}[]->x)&G({{c;d}*}[]->y) +{([*0] + a):c*:([*0] + b)}<>->d +{a;e;f:(g*);h}<>->d +{(a:b)* & (c*:d)}<>->e +{(a:b)*} +G{(a:b)*} +{a;b} +{(a;b)*} +G{(a;b)*} +{a*}[]->{b*} +{a*}[]=>{b*} +{a*&b} +{a*&b*} +{((!c;b*) & d);e} +{(a* & (c;b*) & d);e} +{[*2];a[*2..4]}|->b +{a[*2..5] && b[*..3]}|->c +{{[+];a;[+]} && {[+];b;[+]}}<>->c +{(a[->3]) & {[+];b}}<>->c # This formula (built by a random formula generator), exhibited an # infinite recursion in the translation: -check_psl '{(a|[*0])[*];1}' +{(a|[*0])[*];1} # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). -check_psl '{[*];req;ack}|=>{start;busy[*];done}' +{[*];req;ack}|=>{start;busy[*];done} # Examples from "Property-by-Example Guide: a Handbook of PSL Examples" # by Ben David and Orni (2005)/ -check_psl '{end[=3]}(false)' # 2.27.A -check_psl '{[*]; {read[=3]} && {write[=2]}} |=> - {(!read && !write)[*]; ready}' # 3.5.A -check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp; - {status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33 +# - 2.27.A +{end[=3]}(false) +# - 3.5.A +{[*]; {read[=3]} && {write[=2]}} |=> {(!read && !write)[*]; ready} +# - 2.33 (abridged to fit in 80 cols) +{[*];st&&comp_d_en;!comp_d_en&&good_c;{st_v[->]}&&{stop[=0];true}}|->{!d_out} # Some tricky cases that require the rational automaton to be pruned # before it is used in the translation. -check_psl '{{b[*];c} | {{a && !a}}[=2]}' -check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}' +{{b[*];c} | {{a && !a}}[=2]} +{((a&!b);((!a&!b)*))&&(!b*;(!a&b))} # When translating this formula, we expect the translator to ignore # `a;(f&!f)[=2];c' on one side because it as already seen it on the # other side. -check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}' - +{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c} # these were mis-translated in Spot 0.9 -check_psl 'G!{(b;1)*;a}' -check_psl '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' +G!{(b;1)*;a} +(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a})) +EOF + +run 0 ../checkpsl check.txt + # In particular, Spot 0.9 would incorrectly reject the sequence: # (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}' # This means the following automaton was incorrectly empty in Spot 0.9. run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' - # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization. for opt in '' -DT -DS; do