Commit f412fee6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

stutter check: cleanup and add test cases

* src/ltltest/ltlfilt.test: Add more tests.
* src/ltltest/stutter.test: New test.
* src/ltltest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Catch std::runtime_error.
* src/tgba/tgbasl.hh (make_tgbasl): New function.
* src/tgba/tgbagraph.hh (make_tgba_graph): Add another overload.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Take the algorithm version as an
optional integer, and call getenv() only once.
* bench/stutter/stutter_invariance_randomgraph.cc,
bench/stutter/stutter_invariance_formulas.cc: Simplify using the
above functions.
parent fcf6e251
......@@ -29,7 +29,6 @@
#include "ltlvisit/length.hh"
#include "misc/timer.hh"
#include <argp.h>
#include "error.h"
const char argp_program_doc[] ="";
......@@ -75,21 +74,17 @@ namespace
bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a);
bool res;
bool prev = true;
for (char algo = '1'; algo <= '8'; ++algo)
for (int algo = 1; algo <= 8; ++algo)
{
// set SPOT_STUTTER_CHECK environment variable
char algostr[2] = { 0 };
algostr[0] = algo;
setenv("SPOT_STUTTER_CHECK", algostr, true);
auto dup_a = spot::make_tgba_digraph(a);
auto dup_na = spot::make_tgba_digraph(na);
spot::stopwatch sw;
auto dup_a = std::make_shared<spot::tgba_digraph>(a);
auto dup_na = std::make_shared<spot::tgba_digraph>(na);
sw.start();
res = spot::is_stutter_invariant(std::move(dup_a),
std::move(dup_na), apdict);
const double time = sw.stop();
std::move(dup_na),
apdict, algo);
auto time = sw.stop();
std::cout << formula << ", " << algo << ", " << ap->size() << ", "
<< num_states << ", " << res << ", " << time * 1000000 << std::endl;
......@@ -100,7 +95,7 @@ namespace
}
f->destroy();
nf->destroy();
delete(ap);
delete ap;
return 0;
}
};
......
......@@ -73,11 +73,11 @@ main()
vec.push_back(aut_pair_t(a, na));
}
char algostr[2] = { 0, 0 };
for (char algo = '1'; algo <= '8'; ++algo)
{
// Set SPOT_STUTTER_CHECK environment variable.
char algostr[2] = { 0 };
algostr[0] = algo;
// Select the algorithm for checking stutter-invariance
algostr[0] = algo;
setenv("SPOT_STUTTER_CHECK", algostr, true);
// Copy vec, because is_stutter_invariant modifies the
......@@ -86,18 +86,16 @@ main()
spot::stopwatch sw;
sw.start();
bool res;
for (auto& a: vec)
for (auto& a: dup)
res = spot::is_stutter_invariant(std::move(a.first),
std::move(a.second),
apdict);
const double time = sw.stop();
vec = dup;
auto time = sw.stop();
std::cout << algo << ", " << props_n << ", " << states_n
<< ", " << res << ", " << time << std::endl;
}
spot::ltl::destroy_atomic_prop_set(*ap);
delete(ap);
delete ap;
}
}
......
......@@ -453,7 +453,15 @@ namespace
check_cout();
return !quiet;
}
return process_formula(f, filename, linenum);
try
{
return process_formula(f, filename, linenum);
}
catch (const std::runtime_error& e)
{
error_at_line(2, 0, filename, linenum, "%s", e.what());
SPOT_UNREACHABLE();
}
}
int
......
......@@ -112,7 +112,8 @@ TESTS = \
reducpsl.test \
reduccmp.test \
uwrm.test \
eventuniv.test
eventuniv.test \
stutter.test
distclean-local:
rm -rf $(TESTS:.test=.dir)
#! /bin/sh
# Copyright (C) 2013 Laboratoire de Recherche et Developement to
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Developement to
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -41,6 +41,7 @@ F(b W GFa)
GFa | Gb
b W GFa
!{a;b*;c}!
!{a:b*:c}
a U Fb
G(a & Xb)
Xa
......@@ -75,6 +76,7 @@ F(GFa | Gb)
F(b W GFa)
GFa | Gb
b W GFa
!{a:b[*]:c}
a U Fb
F(a & !Xa & Xb)
a & (b | c)
......@@ -87,6 +89,7 @@ F(b W GFa)
GFa | Gb
b W GFa
!a | X(!b R !c)
!{a:b[*]:c}
Fb
G(a & Xb)
Xa
......@@ -110,6 +113,7 @@ EOF
checkopt --obligation <<EOF
!({a;b[*];c}!)
!{a:b[*]:c}
a U Fb
G(a & Xb)
Xa
......@@ -118,6 +122,7 @@ a & (b | c)
EOF
checkopt --guarantee <<EOF
!{a:b[*]:c}
a U Fb
Xa
F(a & !Xa & Xb)
......@@ -126,6 +131,7 @@ EOF
checkopt -v --ltl <<EOF
!({a;b[*];c}!)
!{a:b[*]:c}
EOF
checkopt -v --stutter-invariant <<EOF
......@@ -159,3 +165,16 @@ EOF
run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out
diff exp out
SPOT_STUTTER_CHECK=0 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'non-LTL' stderr
SPOT_STUTTER_CHECK=555 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'invalid' stderr
SPOT_STUTTER_CHECK=5 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}'
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 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/>.
# Check for the stutter-invariant formula detection
. ./defs || exit 1
set -e
randltl=../../bin/randltl
ltlfilt=../../bin/ltlfilt
FILE=formulae
rm -f $FILE
for i in 10 12 14 16 18 20; do
$randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE
$randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
done
# We do not check i=0, it is too slow.
for i in 1 2 3 4 5 6 7 8; do
SPOT_STUTTER_CHECK=$i
export SPOT_STUTTER_CHECK
time $ltlfilt --stutter-invariant -F $FILE > res.$i
done
# All results should be equal
for i in 2 3 4 5 6 7 8; do
diff res.1 res.$i
done
......@@ -450,6 +450,11 @@ namespace spot
return std::make_shared<tgba_digraph>(dict);
}
inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut)
{
return std::make_shared<tgba_digraph>(aut);
}
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut)
{
return std::make_shared<tgba_digraph>(aut);
......
......@@ -44,6 +44,13 @@ namespace spot
const_tgba_ptr a_;
bdd aps_;
};
typedef std::shared_ptr<tgbasl> tgbasl_ptr;
inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap)
{
return std::make_shared<tgbasl>(aut, ap);
}
}
#endif
......@@ -32,102 +32,94 @@
namespace spot
{
// The stutter check algorithm to use can be overridden via an
// environment variable.
static int default_stutter_check_algorithm()
{
static const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
if (stutter_check)
{
char* endptr;
long res = strtol(stutter_check, &endptr, 10);
if (*endptr || res < 0 || res > 8)
throw
std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
return res;
}
else
{
return 8; // The best variant, according to our benchmarks.
}
}
bool
is_stutter_invariant(const ltl::formula* f)
{
const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
char algo = stutter_check ? stutter_check[0] : '1';
if (f->is_ltl_formula() && f->is_X_free())
return true;
{
if (f->is_ltl_formula() && f->is_X_free())
return true;
int algo = default_stutter_check_algorithm();
if (algo == 0) // Etessami's check via syntactic transformation.
{
if (!f->is_ltl_formula())
throw std::runtime_error("Cannot use the syntactic "
"stutter-invariance check "
"for non-LTL formulas");
const ltl::formula* g = remove_x(f);
ltl::ltl_simplifier ls;
bool res = ls.are_equivalent(f, g);
g->destroy();
return res;
}
if (algo == '0')
{
// Syntactic checking.
if (f->is_ltl_formula())
{
const ltl::formula* g = remove_x(f);
ltl::ltl_simplifier ls;
bool res = ls.are_equivalent(f, g);
g->destroy();
return res;
}
else
{
throw std::runtime_error("Cannot use the syntactic-based " \
"approach to stutter-invariance " \
"checking on non-ltl formula");
}
}
const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
translator trans;
tgba_digraph_ptr aut_f = trans.run(f);
tgba_digraph_ptr aut_nf = trans.run(nf);
bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
nf->destroy();
return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps);
}
// Prepare for an automata-based check.
const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
translator trans;
auto aut_f = trans.run(f);
auto aut_nf = trans.run(nf);
bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
nf->destroy();
return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps, algo);
}
bool
is_stutter_invariant(tgba_digraph_ptr&& aut_f,
tgba_digraph_ptr&& aut_nf, bdd aps)
{
const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
char algo = stutter_check ? stutter_check[0] : '8';
tgba_digraph_ptr&& aut_nf, bdd aps, int algo)
{
if (algo == 0)
algo = default_stutter_check_algorithm();
switch (algo)
{
// sl(aut_f) x sl(aut_nf)
case '1':
{
return product(sl(std::move(aut_f), aps),
sl(std::move(aut_nf), aps))->is_empty();
}
// sl(cl(aut_f)) x aut_nf
case '2':
{
return product(sl(closure(std::move(aut_f)), aps),
std::move(aut_nf))->is_empty();
}
// (cl(sl(aut_f)) x aut_nf
case '3':
{
return product(closure(sl(std::move(aut_f), aps)),
std::move(aut_nf))->is_empty();
}
// sl2(aut_f) x sl2(aut_nf)
case '4':
{
return product(sl2(std::move(aut_f), aps),
sl2(std::move(aut_nf), aps))->is_empty();
}
// sl2(cl(aut_f)) x aut_nf
case '5':
{
return product(sl2(closure(std::move(aut_f)), aps),
std::move(aut_nf))->is_empty();
}
// (cl(sl2(aut_f)) x aut_nf
case '6':
{
return product(closure(sl2(std::move(aut_f), aps)),
std::move(aut_nf))->is_empty();
}
// on-the-fly sl(aut_f) x sl(aut_nf)
case '7':
{
auto slf = std::make_shared<tgbasl>(aut_f, aps);
auto slnf = std::make_shared<tgbasl>(aut_nf, aps);
return product(slf, slnf)->is_empty();
}
// cl(aut_f) x cl(aut_nf)
case '8':
{
return product(closure(std::move(aut_f)),
closure(std::move(aut_nf)))->is_empty();
}
default:
throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
break;
}
}
switch (algo)
{
case 1: // sl(aut_f) x sl(aut_nf)
return product(sl(std::move(aut_f), aps),
sl(std::move(aut_nf), aps))->is_empty();
case 2: // sl(cl(aut_f)) x aut_nf
return product(sl(closure(std::move(aut_f)), aps),
std::move(aut_nf))->is_empty();
case 3: // (cl(sl(aut_f)) x aut_nf
return product(closure(sl(std::move(aut_f), aps)),
std::move(aut_nf))->is_empty();
case 4: // sl2(aut_f) x sl2(aut_nf)
return product(sl2(std::move(aut_f), aps),
sl2(std::move(aut_nf), aps))->is_empty();
case 5: // sl2(cl(aut_f)) x aut_nf
return product(sl2(closure(std::move(aut_f)), aps),
std::move(aut_nf))->is_empty();
case 6: // (cl(sl2(aut_f)) x aut_nf
return product(closure(sl2(std::move(aut_f), aps)),
std::move(aut_nf))->is_empty();
case 7: // on-the-fly sl(aut_f) x sl(aut_nf)
return product(make_tgbasl(aut_f, aps),
make_tgbasl(aut_nf, aps))->is_empty();
case 8: // cl(aut_f) x cl(aut_nf)
return product(closure(std::move(aut_f)),
closure(std::move(aut_nf)))->is_empty();
default:
throw std::runtime_error("invalid algorithm number for "
"is_stutter_invariant()");
SPOT_UNREACHABLE();
}
}
}
......@@ -30,7 +30,8 @@ namespace spot
SPOT_API bool
is_stutter_invariant(tgba_digraph_ptr&& aut_f,
tgba_digraph_ptr&& aut_nf, bdd aps);
tgba_digraph_ptr&& aut_nf, bdd aps,
int algo = 0);
}
#endif
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