diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc index 3be50e8e6..7a1ab2a2f 100644 --- a/src/bin/spot-x.cc +++ b/src/bin/spot-x.cc @@ -1,6 +1,5 @@ - // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -70,10 +69,20 @@ a non-accepting SCC.") }, { DOC("degen-lcache", "If non-zero (the default), whenever the \ degeneralization algorithm enters an SCC on a state that has already \ been associated to a level elsewhere, it should reuse that level. \ -The \"lcache\" stands for \"level cache\".") }, +Different values can be used to select which level to reuse: 1 always \ +uses the first level seen, 2 uses the minimum level seen so far, and \ +3 uses the maximum level seen so far. The \"lcache\" stands for \ +\"level cache\".") }, { DOC("degen-order", "If non-zero, the degeneralization algorithm \ will compute one degeneralization order for each SCC it processes. \ This is currently disabled by default.") }, + { DOC("degen-lskip", "If non-zero (the default), the degeneralization \ +algorithm will skip as much levels as possible for each transition. This \ +is enabled by default as it very often reduce the number of resulting \ +states. A consequence of skipping levels is that the degeneralized \ +automaton tends to have smaller cycles around the accepting states. \ +Disabling skipping will produce automata with large cycles, and often \ +with more states.") }, { DOC("simul", "Set to 0 to disable simulation-based reductions. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index a7e3e4760..0da2f5190 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -24,6 +25,7 @@ #include "ltlast/constant.hh" #include #include +#include #include "tgbaalgos/scc.hh" #include "tgba/bddprint.hh" @@ -217,7 +219,7 @@ namespace spot public: unsigned - next_level(bdd all, int slevel, bdd acc) + next_level(bdd all, int slevel, bdd acc, bool skip_levels) { bdd temp = acc; if (all != found_) @@ -243,7 +245,11 @@ namespace spot acc = temp; unsigned next = slevel; while (next < order_.size() && bdd_implies(order_[next], acc)) - ++next; + { + ++next; + if (!skip_levels) + break; + } return next; } @@ -266,16 +272,18 @@ namespace spot { bdd all_; std::map orders_; + bool skip_levels_; public: - scc_orders(bdd all): all_(all) + scc_orders(bdd all, bool skip_levels): + all_(all), skip_levels_(skip_levels) { } unsigned next_level(int scc, int slevel, bdd acc) { - return orders_[scc].next_level(all_, slevel, acc); + return orders_[scc].next_level(all_, slevel, acc, skip_levels_); } void @@ -290,7 +298,7 @@ namespace spot sba* degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, - bool use_lvl_cache) + int use_lvl_cache, bool skip_levels) { bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; @@ -333,7 +341,7 @@ namespace spot } // Initialize scc_orders - scc_orders orders(a->all_acceptance_conditions()); + scc_orders orders(a->all_acceptance_conditions(), skip_levels); // Make sure we always use the same pointer for identical states // from the input automaton. @@ -355,7 +363,7 @@ namespace spot tr_cache_t tr_cache; // State level cache - typedef std::map lvl_cache_t; + typedef std::map lvl_cache_t; lvl_cache_t lvl_cache; // Compute SCCs in order to use any optimization. @@ -385,7 +393,11 @@ namespace spot s.second = orders.next_level(m.initial(), s.second, acc); else while (s.second < order.size() && bdd_implies(order[s.second], acc)) - ++s.second; + { + ++s.second; + if (!skip_levels) + break; + } } #ifdef DEGEN_DEBUG @@ -523,7 +535,8 @@ namespace spot // } if (is_scc_acc) { - // If lvl_cache is used and switching SCCs, use level from cache + // If lvl_cache is used and switching SCCs, use level + // from cache if (use_lvl_cache && s_scc != scc && lvl_cache.find(d.first) != lvl_cache.end()) { @@ -564,10 +577,17 @@ namespace spot // Consider both the current acceptance // sets, and the acceptance sets common to // the outgoing transitions of the - // destination state. - while (next < order.size() - && bdd_implies(order[next], acc)) - ++next; + // destination state. But don't do + // that if the state is accepting and we + // are not skipping levels. + if (skip_levels || !is_acc) + while (next < order.size() + && bdd_implies(order[next], acc)) + { + ++next; + if (!skip_levels) + break; + } d.second = next; } } @@ -591,8 +611,23 @@ namespace spot ds2num[d] = dest; todo.push_back(d); // Insert new state to cache - if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end()) - lvl_cache[d.first] = d.second; + + if (use_lvl_cache) + { + std::pair res = + lvl_cache.insert(lvl_cache_t::value_type(d.first, + d.second)); + + if (!res.second) + { + if (use_lvl_cache == 3) + res.first->second = + std::max(res.first->second, d.second); + else if (use_lvl_cache == 2) + res.first->second = + std::min(res.first->second, d.second); + } + } } state_explicit_number::transition*& t = diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index f3354cac2..c67528bed 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -44,7 +44,9 @@ namespace spot /// default because our benchmarks show that it usually does more /// harm than good). If \a use_lvl_cache is set, everytime an SCC /// is entered on a state that as already been associated to some - /// level elsewhere, reuse that level). + /// level elsewhere, reuse that level (set it to 2 to keep the + /// smallest number, 3 to keep the largest level, and 1 to keep the + /// first level found). /// /// Any of these three options will cause the SCCs of the automaton /// \a a to be computed prior to its actual degeneralization. @@ -53,7 +55,8 @@ namespace spot SPOT_API sba* degeneralize(const tgba* a, bool use_z_lvl = true, bool use_cust_acc_orders = false, - bool use_lvl_cache = true); + int use_lvl_cache = 1, + bool skip_levels = true); } diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 0c2be1410..e7d6e6d3c 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -39,15 +39,16 @@ namespace spot postprocessor::postprocessor(const option_map* opt) : type_(TGBA), pref_(Small), level_(High), degen_reset_(true), degen_order_(false), degen_cache_(true), - simul_(-1), scc_filter_(-1), ba_simul_(-1), tba_determinisation_(false), - sat_minimize_(0), sat_acc_(0), sat_states_(0), state_based_(false), - wdba_minimize_(true) + degen_lskip_(true), simul_(-1), scc_filter_(-1), ba_simul_(-1), + tba_determinisation_(false), sat_minimize_(0), sat_acc_(0), + sat_states_(0), state_based_(false), wdba_minimize_(true) { if (opt) { degen_order_ = opt->get("degen-order", 0); degen_reset_ = opt->get("degen-reset", 1); degen_cache_ = opt->get("degen-lcache", 1); + degen_lskip_ = opt->get("degen-lskip", 1); simul_ = opt->get("simul", -1); simul_limit_ = opt->get("simul-limit", -1); scc_filter_ = opt->get("scc-filter", -1); @@ -116,7 +117,8 @@ namespace spot const tgba* d = degeneralize(a, degen_reset_, degen_order_, - degen_cache_); + degen_cache_, + degen_lskip_); delete a; if (ba_simul_ <= 0) return d; diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 693089b42..52b812ec0 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -110,7 +110,8 @@ namespace spot // Fine-tuning options fetched from the option_map. bool degen_reset_; bool degen_order_; - bool degen_cache_; + int degen_cache_; + bool degen_lskip_; int simul_; int simul_limit_; int scc_filter_; diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 7866d0060..7e2e674d9 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,8 +1,9 @@ -## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## -*- coding: utf-8 -*- +## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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), -## Université Pierre et Marie Curie. +## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +## Université Pierre et Marie Curie. ## ## This file is part of Spot, a model checking library. ## @@ -106,6 +107,7 @@ TESTS = \ dupexp.test \ degendet.test \ degenid.test \ + degenlskip.test \ kv.test \ lbttparse.test \ scc.test \ diff --git a/src/tgbatest/degenlskip.test b/src/tgbatest/degenlskip.test new file mode 100755 index 000000000..3836d2cb5 --- /dev/null +++ b/src/tgbatest/degenlskip.test @@ -0,0 +1,70 @@ +#!/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 . + +. ./defs + +set -e + +# Make sure degen-skip=0 and degen-skip=1 produce the expected +# automata for 'GFa & GFb' + +../../bin/ltl2tgba -B 'GFa & GFb' > out1 +../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' > out2 +../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' > out3 + +diff out1 out2 +cmp out2 out3 && exit 1 + +cat <expected2 +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 1 [label="a & b\n{Acc[1]}"] + 1 -> 2 [label="!a & b\n{Acc[1]}"] + 1 -> 3 [label="!b\n{Acc[1]}"] + 2 [label="1"] + 2 -> 1 [label="a\n"] + 2 -> 2 [label="!a\n"] + 3 [label="2"] + 3 -> 1 [label="a & b\n"] + 3 -> 2 [label="!a & b\n"] + 3 -> 3 [label="!b\n"] +} +EOF + + +cat <expected3 +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 2 [label="1\n{Acc[1]}"] + 2 [label="1"] + 2 -> 3 [label="b\n"] + 2 -> 2 [label="!b\n"] + 3 [label="2"] + 3 -> 1 [label="a\n"] + 3 -> 3 [label="!a\n"] +} +EOF + +diff out2 expected2 +diff out3 expected3 diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test index b21e589d0..6150ac722 100755 --- a/src/tgbatest/ltlcross2.test +++ b/src/tgbatest/ltlcross2.test @@ -38,6 +38,7 @@ ltl2tgba=../../bin/ltl2tgba "$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \ +"$ltl2tgba --lbtt --ba -x degen-skip=0 --lbtt %f >%T" \ "$ltl2tgba --lbtt --ba --high %f > %T" \ "$ltl2tgba --lbtt -BDC %f > %T" \ "$ltl2tgba --lbtt -BC %f > %T" \