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

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.
parent 6a741189
bddprod bddprod
blue_counter blue_counter
checkpsl
complement complement
defs defs
.deps .deps
......
...@@ -33,6 +33,7 @@ check_SCRIPTS = defs ...@@ -33,6 +33,7 @@ check_SCRIPTS = defs
check_PROGRAMS = \ check_PROGRAMS = \
bitvect \ bitvect \
complement \ complement \
checkpsl \
expldot \ expldot \
explprod \ explprod \
intvcomp \ intvcomp \
...@@ -47,6 +48,7 @@ check_PROGRAMS = \ ...@@ -47,6 +48,7 @@ check_PROGRAMS = \
# Keep this sorted alphabetically. # Keep this sorted alphabetically.
bitvect_SOURCES = bitvect.cc bitvect_SOURCES = bitvect.cc
checkpsl_SOURCES = checkpsl.cc
complement_SOURCES = complementation.cc complement_SOURCES = complementation.cc
expldot_SOURCES = powerset.cc expldot_SOURCES = powerset.cc
expldot_CXXFLAGS = -DDOTTY expldot_CXXFLAGS = -DDOTTY
......
// -*- 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 "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;
}
...@@ -26,97 +26,82 @@ ...@@ -26,97 +26,82 @@
set -e set -e
check_psl () cat >check.txt <<\EOF
{ a
# We don't check the output, but just running these might be enough to a U b
# trigger assertions. X a
run 0 ../ltl2tgba -f -FC "$1" a & b & c
# Make cross products with FM a | b | (c U (d & (g U (h ^ i))))
run 0 ../ltl2tgba -f -R3 -b "$1" > out.tgba Xa & (b U !a) & (b U !a)
run 0 ../ltl2tgba -f -R3 -Pout.tgba -E "!($1)" Fa & Xb & GFc & Gd
run 0 ../ltl2tgba -f -x -R3 -b "$1" > out.tgba Fa & Xa & GFc & Gc
run 0 ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)" Fc & X(a | Xb) & GF(a | Xb) & Gc
} a R (b R c)
(a U b) U (c U d)
check_ltl ()
{ ((Xp2)U(X(1)))&(p1 R(p2 R p0))
check_psl "$@"
# Make cross products with TAA {a*;c}<>->GFb
run 0 ../ltl2tgba -taa -R3 -b "$1" > out.tgba {((a*;b;c)*)&((b*;a;c)*)}<>->x
run 0 ../ltl2tgba -taa -R3 -Pout.tgba -E "!($1)" {(g;y;r)*}<>->x
} G({(g;y;r)*}<>->x)
G({(a;b)*}<>->x)&G({(c;d)*}<>->y)
check_ltl a # try sub-braces
check_ltl 'a U b' G({{a;b}*}[]->x)&G({{c;d}*}[]->y)
check_ltl 'X a' {([*0] + a):c*:([*0] + b)}<>->d
check_ltl 'a & b & c' {a;e;f:(g*);h}<>->d
check_ltl 'a | b | (c U (d & (g U (h ^ i))))' {(a:b)* & (c*:d)}<>->e
check_ltl 'Xa & (b U !a) & (b U !a)' {(a:b)*}
check_ltl 'Fa & Xb & GFc & Gd' G{(a:b)*}
check_ltl 'Fa & Xa & GFc & Gc' {a;b}
check_ltl 'Fc & X(a | Xb) & GF(a | Xb) & Gc' {(a;b)*}
check_ltl 'a R (b R c)' G{(a;b)*}
check_ltl '(a U b) U (c U d)' {a*}[]->{b*}
{a*}[]=>{b*}
check_ltl '((Xp2)U(X(1)))&(p1 R(p2 R p0))' {a*&b}
{a*&b*}
check_psl '{a*;c}<>->GFb' {((!c;b*) & d);e}
check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x' {(a* & (c;b*) & d);e}
check_psl '{(g;y;r)*}<>->x' {[*2];a[*2..4]}|->b
check_psl 'G({(g;y;r)*}<>->x)' {a[*2..5] && b[*..3]}|->c
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' {{[+];a;[+]} && {[+];b;[+]}}<>->c
check_psl 'G({{a;b}*}[]->x)&G({{c;d}*}[]->y)' # try sub-braces {(a[->3]) & {[+];b}}<>->c
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'
# This formula (built by a random formula generator), exhibited an # This formula (built by a random formula generator), exhibited an
# infinite recursion in the translation: # infinite recursion in the translation:
check_psl '{(a|[*0])[*];1}' {(a|[*0])[*];1}
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007). # 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" # Examples from "Property-by-Example Guide: a Handbook of PSL Examples"
# by Ben David and Orni (2005)/ # by Ben David and Orni (2005)/
check_psl '{end[=3]}(false)' # 2.27.A # - 2.27.A
check_psl '{[*]; {read[=3]} && {write[=2]}} |=> {end[=3]}(false)
{(!read && !write)[*]; ready}' # 3.5.A # - 3.5.A
check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp; {[*]; {read[=3]} && {write[=2]}} |=> {(!read && !write)[*]; ready}
{status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33 # - 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 # Some tricky cases that require the rational automaton to be pruned
# before it is used in the translation. # before it is used in the translation.
check_psl '{{b[*];c} | {{a && !a}}[=2]}' {{b[*];c} | {{a && !a}}[=2]}
check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}' {((a&!b);((!a&!b)*))&&(!b*;(!a&b))}
# When translating this formula, we expect the translator to ignore # 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 # `a;(f&!f)[=2];c' on one side because it as already seen it on the
# other side. # 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 # these were mis-translated in Spot 0.9
check_psl 'G!{(b;1)*;a}' G!{(b;1)*;a}
check_psl '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!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: # 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}' # (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. # 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}))' 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, # Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization. # before and after degeneralization.
for opt in '' -DT -DS; do for opt in '' -DT -DS; do
......
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