tgbatest: rewrite emptchk.test in C++
So that its run time goes from 10min+ to ~5s. * src/tgbatest/emptchk.cc: New file. * src/tgbatest/Makefile.am: Add it. * src/tgbatest/emptchk.test: Use it.
This commit is contained in:
Alexandre Duret-Lutz
parent
b360b02290
commit
bc2e68f85c
4 changed files with 239 additions and 70 deletions
1
src/tgbatest/.gitignore
vendored
1
src/tgbatest/.gitignore
vendored
|
|
@ -6,6 +6,7 @@ defs
|
|||
.deps
|
||||
*.dot
|
||||
eltl2tgba
|
||||
emptchk
|
||||
expldot
|
||||
explicit
|
||||
explicit2
|
||||
|
|
|
|||
|
|
@ -35,6 +35,7 @@ check_PROGRAMS = \
|
|||
complement \
|
||||
checkpsl \
|
||||
checkta \
|
||||
emptchk \
|
||||
expldot \
|
||||
explprod \
|
||||
intvcomp \
|
||||
|
|
@ -52,6 +53,7 @@ bitvect_SOURCES = bitvect.cc
|
|||
checkpsl_SOURCES = checkpsl.cc
|
||||
checkta_SOURCES = checkta.cc
|
||||
complement_SOURCES = complementation.cc
|
||||
emptchk_SOURCES = emptchk.cc
|
||||
expldot_SOURCES = powerset.cc
|
||||
expldot_CXXFLAGS = -DDOTTY
|
||||
explprod_SOURCES = explprod.cc
|
||||
|
|
|
|||
221
src/tgbatest/emptchk.cc
Normal file
221
src/tgbatest/emptchk.cc
Normal file
|
|
@ -0,0 +1,221 @@
|
|||
// -*- 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#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 "tgbaalgos/degen.hh"
|
||||
#include "tgba/tgbaproduct.hh"
|
||||
#include "tgbaalgos/gtec/gtec.hh"
|
||||
#include "tgbaalgos/dotty.hh"
|
||||
#include "tgbaalgos/dupexp.hh"
|
||||
#include "tgbaalgos/emptiness.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::cout << "========================================================\n";
|
||||
std::cout << line << ": " << s << '\n';
|
||||
if (s.empty() || s[0] == '#') // Skip comments
|
||||
continue;
|
||||
|
||||
std::vector<std::string> tokens;
|
||||
{
|
||||
std::istringstream ss(s);
|
||||
std::string form;
|
||||
while (std::getline(ss, form, ','))
|
||||
{
|
||||
std::string tmp;
|
||||
while (form.size() > 0 && form.back() == '\\'
|
||||
&& std::getline(ss, tmp, ','))
|
||||
{
|
||||
form.back() = ',';
|
||||
form += tmp;
|
||||
}
|
||||
tokens.push_back(form);
|
||||
}
|
||||
}
|
||||
|
||||
if (tokens.size() != 2)
|
||||
{
|
||||
std::cerr << "Expecting two tokens on input line.\n";
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int runs = atoi(tokens[0].c_str());
|
||||
|
||||
spot::ltl::parse_error_list pe;
|
||||
auto f = spot::ltl::parse(tokens[1], pe);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, tokens[1], pe))
|
||||
return 2;
|
||||
|
||||
auto d = spot::make_bdd_dict();
|
||||
|
||||
// Build many different automata from this formula.
|
||||
spot::const_tgba_ptr aut[4];
|
||||
{
|
||||
auto a = spot::ltl_to_taa(f, d);
|
||||
aut[0] = a;
|
||||
aut[1] = spot::degeneralize_tba(a);
|
||||
}
|
||||
{
|
||||
auto a = spot::ltl_to_tgba_fm(f, d);
|
||||
aut[2] = a;
|
||||
aut[3] = spot::degeneralize(a);
|
||||
}
|
||||
|
||||
const char* algos[] = {
|
||||
"Cou99", "Cou99(shy)",
|
||||
"CVWY90", "CVWY90(bsh=10M)", "CVWY90(repeated)",
|
||||
"SE05", "SE05(bsh=10M)", "SE05(repeated)",
|
||||
"Tau03_opt", "GV04",
|
||||
};
|
||||
|
||||
for (auto& algo: algos)
|
||||
{
|
||||
const char* err;
|
||||
auto i = spot::emptiness_check_instantiator::construct(algo, &err);
|
||||
if (!i)
|
||||
{
|
||||
std::cerr << "Failed to parse `" << err << '\'' << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
for (unsigned j = 0; j < sizeof(aut)/sizeof(*aut); ++j)
|
||||
{
|
||||
auto a = aut[j];
|
||||
std::cout << "** Testing aut[" << j << "] using " << algo << '\n';
|
||||
unsigned n_acc = a->number_of_acceptance_conditions();
|
||||
unsigned n_max = i->max_acceptance_conditions();
|
||||
if (n_max < n_acc)
|
||||
{
|
||||
std::cout << "Skipping because automaton has " << n_acc
|
||||
<< " acceptance sets, and " << algo
|
||||
<< " accepts at most " << n_max << ".\n";
|
||||
continue;
|
||||
}
|
||||
unsigned n_min = i->min_acceptance_conditions();
|
||||
if (n_min > n_acc)
|
||||
{
|
||||
std::cout << "Skipping because automaton has " << n_acc
|
||||
<< " acceptance sets, and " << algo
|
||||
<< " wants at least " << n_min << ".\n";
|
||||
continue;
|
||||
}
|
||||
|
||||
auto ec = i->instantiate(a);
|
||||
bool search_many = i->options().get("repeated");
|
||||
assert(ec);
|
||||
int ce_found = 0;
|
||||
do
|
||||
{
|
||||
auto res = ec->check();
|
||||
if (res)
|
||||
{
|
||||
++ce_found;
|
||||
std::cout << ce_found << " counterexample found\n";
|
||||
auto run = res->accepting_run();
|
||||
if (run)
|
||||
{
|
||||
auto ar = spot::tgba_run_to_tgba(a, run);
|
||||
spot::dotty_reachable(std::cout, ar, false);
|
||||
delete run;
|
||||
}
|
||||
std::cout << '\n';
|
||||
if (runs == 0)
|
||||
{
|
||||
std::cerr << "ERROR: Expected no counterexample.\n";
|
||||
exit(1);
|
||||
}
|
||||
delete res;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (ce_found)
|
||||
std::cout << "No more counterexample found.\n\n";
|
||||
else
|
||||
std::cout << "No counterexample found.\n\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
while (search_many);
|
||||
|
||||
// The expected number of runs is only for TAA translations
|
||||
if (search_many && runs > ce_found && j < 2)
|
||||
{
|
||||
std::cerr << "ERROR: only " << ce_found
|
||||
<< " counterexamples founds, expected at least "
|
||||
<< runs << '\n';
|
||||
exit(1);
|
||||
}
|
||||
if (!search_many && ec->safe() && runs && !ce_found)
|
||||
{
|
||||
std::cerr << "ERROR: expected a counterexample.\n";
|
||||
exit(1);
|
||||
}
|
||||
|
||||
delete ec;
|
||||
}
|
||||
delete i;
|
||||
}
|
||||
f->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;
|
||||
}
|
||||
|
|
@ -26,74 +26,19 @@
|
|||
|
||||
set -e
|
||||
|
||||
expect_ce_do()
|
||||
{
|
||||
run 0 ../ltl2tgba "$@"
|
||||
run 0 ../ltl2tgba -g "$@"
|
||||
}
|
||||
cat > emptchk.txt <<EOF
|
||||
1, a
|
||||
1, a U b
|
||||
1, X a
|
||||
1, a & b & c
|
||||
1, a | b | (c U (d & (g U (h ^ i))))
|
||||
1, Xa & (b U !a) & (b U !a)
|
||||
1, Fa & Xb & GFc & Gd
|
||||
2, Fa & Xa & GFc & Gc
|
||||
1, Fc & X(a | Xb) & GF(a | Xb) & Gc
|
||||
2, !((FF a) <=> (F x))
|
||||
0, Xa && (!a U b) && !b && X!b
|
||||
0, (a U !b) && Gb
|
||||
EOF
|
||||
|
||||
expect_ce()
|
||||
{
|
||||
expect_ce_do -CR -e -taa "$1"
|
||||
expect_ce_do -CR -e -taa -DT "$1"
|
||||
expect_ce_do -CR -e -f "$1"
|
||||
expect_ce_do -CR -e -f -DT "$1"
|
||||
expect_ce_do -CR -e'Cou99(shy)' -taa "$1"
|
||||
expect_ce_do -CR -e'Cou99(shy)' -taa -DT "$1"
|
||||
expect_ce_do -CR -e'Cou99(shy)' -f "$1"
|
||||
expect_ce_do -CR -e'Cou99(shy)' -f -DT "$1"
|
||||
expect_ce_do -CR -eCVWY90 -taa "$1"
|
||||
expect_ce_do -CR -eCVWY90 -f "$1"
|
||||
run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -f "$1"
|
||||
run 0 ../ltl2tgba -CR -eSE05 -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -eSE05 -f "$1"
|
||||
run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -f "$1"
|
||||
run 0 ../ltl2tgba -CR -eTau03_opt -f "$1"
|
||||
run 0 ../ltl2tgba -CR -eGV04 -f "$1"
|
||||
# Expect multiple accepting runs
|
||||
test `../ltl2tgba -C -e'CVWY90(repeated)' -taa "$1" |
|
||||
grep Prefix: | wc -l` -ge $2
|
||||
test `../ltl2tgba -C -e'SE05(repeated)' -taa "$1" |
|
||||
grep Prefix: | wc -l` -ge $2
|
||||
}
|
||||
|
||||
expect_no()
|
||||
{
|
||||
run 0 ../ltl2tgba -CR -E -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -E -taa -DT "$1"
|
||||
run 0 ../ltl2tgba -CR -E -f "$1"
|
||||
run 0 ../ltl2tgba -CR -E -f -DT "$1"
|
||||
run 0 ../ltl2tgba -CR -E'Cou99(shy)' -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -E'Cou99(shy)' -taa -DT "$1"
|
||||
run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f "$1"
|
||||
run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f -DT "$1"
|
||||
run 0 ../ltl2tgba -CR -ECVWY90 -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -ECVWY90 -f "$1"
|
||||
run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -f "$1"
|
||||
run 0 ../ltl2tgba -CR -ESE05 -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -ESE05 -f "$1"
|
||||
run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -taa "$1"
|
||||
run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -f "$1"
|
||||
run 0 ../ltl2tgba -CR -ETau03_opt -f "$1"
|
||||
run 0 ../ltl2tgba -CR -EGV04 -f "$1"
|
||||
test `../ltl2tgba -C -e'CVWY90(repeated)' -taa "!($1)" |
|
||||
grep Prefix: | wc -l` -ge $2
|
||||
test `../ltl2tgba -C -e'SE05(repeated)' -taa "!($1)" |
|
||||
grep Prefix: | wc -l` -ge $2
|
||||
}
|
||||
|
||||
expect_ce 'a' 1
|
||||
expect_ce 'a U b' 1
|
||||
expect_ce 'X a' 1
|
||||
expect_ce 'a & b & c' 1
|
||||
expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 1
|
||||
expect_ce 'Xa & (b U !a) & (b U !a)' 1
|
||||
expect_ce 'Fa & Xb & GFc & Gd' 1
|
||||
expect_ce 'Fa & Xa & GFc & Gc' 2
|
||||
expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1
|
||||
expect_ce '!((FF a) <=> (F x))' 2
|
||||
expect_no 'Xa && (!a U b) && !b && X!b' 2
|
||||
expect_no '(a U !b) && Gb' 2
|
||||
run 0 ../emptchk emptchk.txt
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue