From f412fee6f3cdfcbc1b6859c806b03cffd57fded4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 12 Nov 2014 18:29:54 +0100 Subject: [PATCH] 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. --- bench/stutter/stutter_invariance_formulas.cc | 19 +- .../stutter/stutter_invariance_randomgraph.cc | 14 +- src/bin/ltlfilt.cc | 10 +- src/ltltest/Makefile.am | 3 +- src/ltltest/ltlfilt.test | 21 ++- src/ltltest/stutter.test | 47 +++++ src/tgba/tgbagraph.hh | 5 + src/tgba/tgbasl.hh | 7 + src/tgbaalgos/stutter_invariance.cc | 174 +++++++++--------- src/tgbaalgos/stutter_invariance.hh | 3 +- 10 files changed, 188 insertions(+), 115 deletions(-) create mode 100755 src/ltltest/stutter.test diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index 66e7b22af..f9407ad0c 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -29,7 +29,6 @@ #include "ltlvisit/length.hh" #include "misc/timer.hh" #include -#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(a); - auto dup_na = std::make_shared(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; } }; diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index 80a5a9197..4920e72ea 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -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; } } diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 954872306..0eaf15281 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -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 diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index eab5011e3..b9758f9c9 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -112,7 +112,8 @@ TESTS = \ reducpsl.test \ reduccmp.test \ uwrm.test \ - eventuniv.test + eventuniv.test \ + stutter.test distclean-local: rm -rf $(TESTS:.test=.dir) diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index 1e2f11c4c..d8751d364 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -1,5 +1,5 @@ #! /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 <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}' diff --git a/src/ltltest/stutter.test b/src/ltltest/stutter.test new file mode 100755 index 000000000..a2b7c144d --- /dev/null +++ b/src/ltltest/stutter.test @@ -0,0 +1,47 @@ +#! /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 . + + +# 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 diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index c2be1f406..688746012 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -450,6 +450,11 @@ namespace spot return std::make_shared(dict); } + inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut) + { + return std::make_shared(aut); + } + inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut) { return std::make_shared(aut); diff --git a/src/tgba/tgbasl.hh b/src/tgba/tgbasl.hh index dc5040917..00195c717 100644 --- a/src/tgba/tgbasl.hh +++ b/src/tgba/tgbasl.hh @@ -44,6 +44,13 @@ namespace spot const_tgba_ptr a_; bdd aps_; }; + + typedef std::shared_ptr tgbasl_ptr; + + inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap) + { + return std::make_shared(aut, ap); + } } #endif diff --git a/src/tgbaalgos/stutter_invariance.cc b/src/tgbaalgos/stutter_invariance.cc index 326ca7f72..3e0e0e778 100644 --- a/src/tgbaalgos/stutter_invariance.cc +++ b/src/tgbaalgos/stutter_invariance.cc @@ -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; - 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); - } + 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; + } + + // 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(aut_f, aps); - auto slnf = std::make_shared(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(); + } + } } diff --git a/src/tgbaalgos/stutter_invariance.hh b/src/tgbaalgos/stutter_invariance.hh index 95133eccc..24f3431e5 100644 --- a/src/tgbaalgos/stutter_invariance.hh +++ b/src/tgbaalgos/stutter_invariance.hh @@ -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