From 717c857794536c04465409a14a498bfca0ea1487 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Feb 2015 08:57:49 +0100 Subject: [PATCH] ltlcross: adjust to work with generic acceptance * src/bin/ltlcross.cc: Remove Fin-acceptance before doing checks. More --verbose output. * src/tgba/acc.cc, src/tgba/acc.hh: Add an eval_sets() function to find the set of acceptance sets needed to satisfy the condition in an accepting SCC. * src/tgbaalgos/gtec/ce.cc: Use eval_sets() when computing a counter example. * src/tgbaalgos/gtec/gtec.cc: Raise an exception when called on an acceptance that contains Fin. * src/tgbatest/ltl2dstar3.test, src/tgbatest/ltlcrossce2.test: New files. * src/tgbatest/Makefile.am: Add them. * src/tgba/tgba.cc (is_empty): Call remove_fin if needed. * src/tgbaalgos/product.cc, src/tgbaalgos/dtgbacomp.cc: Adjust to work with generic acceptance. --- src/bin/ltlcross.cc | 68 ++++++++++++++++++++++++++++----- src/tgba/acc.cc | 56 +++++++++++++++++++++++++++ src/tgba/acc.hh | 1 + src/tgba/tgba.cc | 12 +++++- src/tgbaalgos/dtgbacomp.cc | 21 ++++++++-- src/tgbaalgos/gtec/ce.cc | 5 ++- src/tgbaalgos/gtec/gtec.cc | 19 ++++++++- src/tgbaalgos/product.cc | 6 ++- src/tgbatest/Makefile.am | 2 + src/tgbatest/ltl2dstar3.test | 48 +++++++++++++++++++++++ src/tgbatest/ltlcrossce2.test | 72 +++++++++++++++++++++++++++++++++++ 11 files changed, 293 insertions(+), 17 deletions(-) create mode 100755 src/tgbatest/ltl2dstar3.test create mode 100755 src/tgbatest/ltlcrossce2.test diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 9289131df..c72b4a625 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -47,6 +47,7 @@ #include "ltlvisit/lbt.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/product.hh" +#include "tgbaalgos/remfin.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/sccinfo.hh" @@ -54,6 +55,7 @@ #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/word.hh" #include "tgbaalgos/dtgbacomp.hh" +#include "tgbaalgos/cleanacc.hh" #include "misc/formater.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/isdet.hh" @@ -481,7 +483,7 @@ namespace has_sr = has('D'); } - spot::const_tgba_digraph_ptr + spot::tgba_digraph_ptr translate(unsigned int translator_num, char l, statistics_formula* fstats, bool& problem) { @@ -502,7 +504,7 @@ namespace const char* status_str = 0; - spot::const_tgba_digraph_ptr res = 0; + spot::tgba_digraph_ptr res = 0; if (timed_out) { // This is not considered to be a global error. @@ -698,7 +700,6 @@ namespace size_t i, size_t j, bool icomp, bool jcomp) { auto prod = spot::product(aut_i, aut_j); - auto res = spot::couvreur99(prod)->check(); if (verbose) { @@ -714,6 +715,7 @@ namespace std::cerr << '\n'; } + auto res = spot::couvreur99(prod)->check(); if (res) { std::ostream& err = global_error(); @@ -1019,12 +1021,12 @@ namespace // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); - std::vector pos(m); - std::vector neg(m); + std::vector pos(m); + std::vector neg(m); // These store the complement of the above results, when we can // compute it easily. - std::vector comp_pos(m); - std::vector comp_neg(m); + std::vector comp_pos(m); + std::vector comp_neg(m); unsigned n = vstats.size(); @@ -1101,6 +1103,37 @@ namespace std::cerr << "Performing sanity checks and gathering statistics..." << std::endl; + if (verbose) + std::cerr << "info: getting rid of any Inf acceptance...\n"; + for (unsigned i = 0; i < m; ++i) + { +#define DO(x, prefix, suffix) if (x[i]) \ + { \ + cleanup_acceptance(x[i]); \ + if (x[i]->acc().uses_fin_acceptance()) \ + { \ + auto st = x[i]->num_states(); \ + auto tr = x[i]->num_transitions(); \ + auto ac = x[i]->acc().num_sets(); \ + x[i] = remove_fin(x[i]); \ + if (verbose) \ + std::cerr << "info:\t" prefix << i \ + << suffix << "\t(" \ + << st << " st., " \ + << tr << " ed., " \ + << ac << " sets) -> (" \ + << x[i]->num_states() << " st., " \ + << x[i]->num_transitions() << " ed., " \ + << x[i]->acc().num_sets() << " sets)\n"; \ + } \ + } + DO(pos, " P", " "); + DO(neg, " N", " "); + DO(comp_pos, "Comp(P", ")"); + DO(comp_neg, "Comp(N", ")"); +#undef DO + } + // intersection test for (size_t i = 0; i < m; ++i) if (pos[i]) @@ -1168,10 +1201,16 @@ namespace if (verbose) std::cerr << "info: building state-space #" << p << '/' << products - << " with seed " << seed << '\n'; + << " of " << states << " states with seed " << seed + << '\n'; auto statespace = spot::random_graph(states, density, ap, dict); + if (verbose) + std::cerr << "info: state-space has " + << statespace->num_transitions() + << " edges\n"; + // Products of the state space with the positive automata. std::vector pos_prod(m); // Products of the state space with the negative automata. @@ -1182,6 +1221,11 @@ namespace for (size_t i = 0; i < m; ++i) if (pos[i]) { + if (verbose) + std::cerr << ("info: building product between state-space and" + " P") << i + << " (" << pos[i]->num_states() << " st., " + << pos[i]->num_transitions() << " ed.)\n"; auto p = spot::product(pos[i], statespace); pos_prod[i] = p; auto sm = new spot::scc_info(p); @@ -1201,7 +1245,13 @@ namespace for (size_t i = 0; i < m; ++i) if (neg[i]) { - auto p = spot::product(neg[i], statespace); + if (verbose) + std::cerr << ("info: building product between state-space and" + " N") << i + << " (" << neg[i]->num_states() << " st., " + << neg[i]->num_transitions() << " ed.)\n"; + + auto p = spot::product(neg[i], statespace); neg_prod[i] = p; auto sm = new spot::scc_info(p); neg_map[i] = sm; diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index c33591a1f..84250c426 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -188,6 +188,52 @@ namespace spot SPOT_UNREACHABLE(); return false; } + + static acc_cond::mark_t + eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + { + auto sub = pos - pos->size; + acc_cond::mark_t m = 0U; + while (sub < pos) + { + --pos; + if (auto s = eval_sets(inf, pos)) + m |= s; + else + return 0U; + pos -= pos->size; + } + return m; + } + case acc_cond::acc_op::Or: + { + auto sub = pos - pos->size; + while (sub < pos) + { + --pos; + if (auto s = eval_sets(inf, pos)) + return s; + pos -= pos->size; + } + return 0U; + } + case acc_cond::acc_op::Inf: + if ((pos[-1].mark & inf) == pos[-1].mark) + return pos[-1].mark; + else + return 0U; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + } + SPOT_UNREACHABLE(); + return false; + } } bool acc_cond::accepting(mark_t inf) const @@ -197,6 +243,16 @@ namespace spot return eval(inf, &code_.back()); } + acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const + { + if (uses_fin_acceptance()) + throw std::runtime_error + ("Fin acceptance is not supported by this code path."); + if (code_.empty()) + return 0U; + return eval_sets(inf, &code_.back()); + } + bool acc_cond::check_fin_acceptance() const { if (code_.empty()) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 4a6f3fc3a..83ccd514c 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -748,6 +748,7 @@ namespace spot } bool accepting(mark_t inf) const; + mark_t accepting_sets(mark_t inf) const; std::ostream& format(std::ostream& os, mark_t m) const { diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 8d6aafa54..91b286c4c 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -21,7 +21,9 @@ // along with this program. If not, see . #include "tgba.hh" +#include "tgbagraph.hh" #include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/remfin.hh" #include namespace spot @@ -80,7 +82,15 @@ namespace spot // FIXME: This should be improved based on properties of the // automaton. For instance we do not need couvreur99 is we know // the automaton is weak. - return !couvreur99(shared_from_this())->check(); + auto a = shared_from_this(); + if (a->acc().uses_fin_acceptance()) + { + auto aa = std::dynamic_pointer_cast(a); + if (!aa) + aa = make_tgba_digraph(a, prop_set::all()); + a = remove_fin(aa); + } + return !couvreur99(a)->check(); } void diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index a0b6e49de..c732dbe8c 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -19,6 +19,8 @@ #include "dtgbacomp.hh" #include "sccinfo.hh" +#include "complete.hh" +#include "cleanacc.hh" namespace spot { @@ -160,9 +162,22 @@ namespace spot tgba_digraph_ptr dtgba_complement(const const_tgba_digraph_ptr& aut) { - if (aut->is_inherently_weak()) - return dtgba_complement_weak(aut); + if (aut->acc().is_generalized_buchi()) + { + if (aut->is_inherently_weak()) + return dtgba_complement_weak(aut); + else + return dtgba_complement_nonweak(aut); + } else - return dtgba_complement_nonweak(aut); + { + // Simply complete the automaton, and complement its + // acceptance. + auto res = tgba_complete(aut); + cleanup_acceptance(res); + res->set_acceptance(res->acc().num_sets(), + res->get_acceptance().complement()); + return res; + } } } diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 63deb497f..d72b7fd9e 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -149,7 +149,8 @@ namespace spot void couvreur99_check_result::accepting_cycle() { - acc_cond::mark_t acc_to_traverse = ecs_->aut->acc().all_sets(); + acc_cond::mark_t acc_to_traverse = + ecs_->aut->acc().accepting_sets(ecs_->root.top().condition); // Compute an accepting cycle using successive BFS that are // restarted from the point reached after we have discovered a // transition with a new acceptance conditions. diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 69485bba8..997b02864 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014 Laboratoire de Recherche et +// Copyright (C) 2008, 2011, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -131,6 +131,15 @@ namespace spot emptiness_check_result_ptr couvreur99_check::check() { + { + auto acc = ecs_->aut->acc(); + if (acc.get_acceptance().is_false()) + return nullptr; + if (acc.uses_fin_acceptance()) + throw std::runtime_error + ("Fin acceptance is not supported by couvreur99()"); + } + // We use five main data in this algorithm: // * couvreur99_check::root, a stack of strongly connected components (SCC), // * couvreur99_check::h, a hash of all visited nodes, with their order, @@ -384,6 +393,14 @@ namespace spot emptiness_check_result_ptr couvreur99_check_shy::check() { + { + auto acc = ecs_->aut->acc(); + if (acc.get_acceptance().is_false()) + return nullptr; + if (acc.uses_fin_acceptance()) + throw std::runtime_error + ("Fin acceptance is not supported by couvreur99()"); + } // Position in the loop seeking known successors. pos = todo.back().q.begin(); diff --git a/src/tgbaalgos/product.cc b/src/tgbaalgos/product.cc index 83291ac1c..46c01990c 100644 --- a/src/tgbaalgos/product.cc +++ b/src/tgbaalgos/product.cc @@ -76,7 +76,11 @@ namespace spot return p.first->second; }; - new_state(left_state, right_state); + res->set_init_state(new_state(left_state, right_state)); + if (right_acc.is_false()) + // Do not bother doing any work if the resulting acceptance is + // false. + return res; while (!todo.empty()) { auto top = todo.front(); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index d1a916752..546c395f3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -109,6 +109,7 @@ TESTS = \ ltlcross4.test \ ltl2dstar.test \ ltl2dstar2.test \ + ltl2dstar3.test \ ltl2ta.test \ ltl2ta2.test \ randaut.test \ @@ -121,6 +122,7 @@ TESTS = \ emptchke.test \ dfs.test \ ltlcrossce.test \ + ltlcrossce2.test \ emptchkr.test \ ltlcounter.test \ basimul.test \ diff --git a/src/tgbatest/ltl2dstar3.test b/src/tgbatest/ltl2dstar3.test new file mode 100755 index 000000000..2c828a4a1 --- /dev/null +++ b/src/tgbatest/ltl2dstar3.test @@ -0,0 +1,48 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 . + +# Test ltl2dstar's HOA output with ltlcross. + +. ./defs +set -e + +# Skip this test if ltl2dstar is not installed. +(ltl2dstar --version) || exit 77 + +ltlfilt=../../bin/ltlfilt +ltl2tgba=../../bin/ltl2tgba +ltlcross=../../bin/ltlcross +randltl=../../bin/randltl +ltlfilt=../../bin/ltlfilt +dstar2tgba=../../bin/dstar2tgba + +RAB='--automata=rabin --output-format=hoa' +STR='--automata=streett --output-format=hoa' + +# Run ltlcross without product, because this requires too much memory. +$randltl -n 25 a b | $ltlfilt --remove-wm | +$ltlcross -F- -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ +--timeout=30 --verbose --csv=out.csv --products=0 \ +"$ltl2tgba -s %f >%N" \ +"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %H" \ +"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %H" + +grep '"in_type"' out.csv && exit 1 +exit 0 diff --git a/src/tgbatest/ltlcrossce2.test b/src/tgbatest/ltlcrossce2.test new file mode 100755 index 000000000..decabbd12 --- /dev/null +++ b/src/tgbatest/ltlcrossce2.test @@ -0,0 +1,72 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 . + +. ./defs +set -e + +ltl2tgba=../../bin/ltl2tgba + +cat >fake <<\EOF +#!/bin/sh +case $1 in +"U G e p0 F p1 p2") + +# echo 'U G e p0 F p1 p2' | ltl2dstar --output-format=hoa - - | fmt +cat <<\END +HOA: v1 States: 14 properties: implicit-labels trans-labels +no-univ-branch deterministic complete acc-name: Rabin 3 Acceptance: 6 +(Fin(0)&Inf(1))|(Fin(2)&Inf(3))|(Fin(4)&Inf(5)) Start: 10 AP: 3 "p0" +"p1" "p2" --BODY-- State: 0 {5} 0 3 5 5 0 3 5 5 State: 1 {3 4} 0 12 5 +1 0 12 5 1 State: 2 {3 4} 2 13 5 5 2 13 5 5 State: 3 {3 4} 13 13 5 5 13 +13 5 5 State: 4 {1 2 4} 4 4 4 4 4 4 4 4 State: 5 {0 2 4} 5 5 5 5 5 5 5 +5 State: 6 {2 4} 8 6 5 1 8 6 5 1 State: 7 {2 4} 7 8 5 5 2 8 5 5 State: +8 {2 4} 8 8 5 5 8 8 5 5 State: 9 {2 4} 7 11 5 9 2 6 5 1 State: 10 {2 4} +7 11 5 9 4 4 4 4 State: 11 {2 4} 8 11 5 9 8 6 5 1 State: 12 {4} 13 12 +5 1 13 12 5 1 State: 13 {4} 13 13 5 5 13 13 5 5 --END-- +END +;; +"! U G e p0 F p1 p2") +# echo '! U G e p0 F p1 p2' | ltl2dstar --output-format=hoa - - | fmt | +# sed '$s:8 13:13 8 /*<-bug*/:'; +cat <<\END +HOA: v1 States: 14 properties: implicit-labels trans-labels +no-univ-branch deterministic complete acc-name: Rabin 3 Acceptance: 6 +(Fin(0)&Inf(1))|(Fin(2)&Inf(3))|(Fin(4)&Inf(5)) Start: 11 AP: 3 "p0" "p1" +"p2" --BODY-- State: 0 {5} 4 0 8 8 4 0 8 8 State: 1 {3 4} 1 1 8 8 1 1 8 +8 State: 2 {3 4} 1 2 8 13 1 2 8 13 State: 3 {3 4} 5 3 8 8 4 0 8 8 State: +4 {1 2 4} 1 1 8 8 1 1 8 8 State: 5 {1 2 4} 5 3 8 8 1 1 8 8 State: 6 {1 +2 4} 6 3 8 8 12 1 8 8 State: 7 {1 2 4} 5 7 8 9 1 2 8 13 State: 8 {1 2 4} +8 8 8 8 8 8 8 8 State: 9 {1 2 4} 6 7 8 9 12 2 8 13 State: 10 {0 2 4} 10 +10 10 10 10 10 10 10 State: 11 {2 4} 6 7 8 9 10 10 10 10 State: 12 {2 4} +12 1 8 8 12 1 8 8 State: 13 {2 4} 12 2 13 8 /*<-bug*/ 12 2 8 13 --END-- +END +;; +esac +EOF +chmod +x fake + +run 1 ../../bin/ltlcross -f 'G(a <-> Fb) U c' \ + "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors +cat errors +grep 'error: P0\*N1 is nonempty' errors +grep 'error: P1\*N1 is nonempty' errors +grep 'error: Comp..1.\*Comp..1. is nonempty' errors +test `grep cycle errors | wc -l` = 3 +test `grep '^error:' errors | wc -l` = 4