From bc416fdb2f38888e7622062e9ef82d234697a543 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Aug 2011 18:42:00 +0200 Subject: [PATCH] Make sure the degeneralization is idempotent (up to renaming of states). * src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the acceptance conditions that are common to all outgoing transitions of this state. This helps to make the degeneralization idempotent. * src/tgbatest/degenid.test: New test case. * src/tgbatest/Makefile.am: Add it. --- ChangeLog | 12 ++++++++++++ src/tgba/tgbatba.cc | 38 +++++++++++++++++++++++++++++-------- src/tgbatest/Makefile.am | 1 + src/tgbatest/degenid.test | 40 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 83 insertions(+), 8 deletions(-) create mode 100755 src/tgbatest/degenid.test diff --git a/ChangeLog b/ChangeLog index 853809abe..532ee587b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2011-08-25 Alexandre Duret-Lutz + + Make sure the degeneralization is idempotent (up to renaming of + states). + + * src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the + acceptance conditions that are common to all outgoing transitions + of this state. This helps to make the degeneralization + idempotent. + * src/tgbatest/degenid.test: New test case. + * src/tgbatest/Makefile.am: Add it. + 2011-08-25 Alexandre Duret-Lutz Fix escaping of state name in save_reachable()'s output. diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 0293e942e..50ed88dc3 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -143,7 +143,8 @@ namespace spot typedef tgba_tba_proxy::cycle_list list; typedef tgba_tba_proxy::cycle_list::const_iterator iterator; public: - tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, + tgba_tba_proxy_succ_iterator(const state* rs, + tgba_succ_iterator* it, iterator expected, const list& cycle, bdd the_acceptance_cond, @@ -156,10 +157,11 @@ namespace spot bdd acc = it->current_acceptance_conditions(); // As an extra optimization step, gather the acceptance // conditions common to all outgoing transitions of the - // destination state, and pretend they are already present - // on this transition. + // destination state. We will later add these to "acc" to + // pretend they are already present on this transition. state* odest = it->current_state(); - acc |= aut->common_acceptance_conditions_of_original_state(odest); + bdd otheracc = + aut->common_acceptance_conditions_of_original_state(odest); iterator next; // bddtrue is a special condition used for tgba_sba_proxy @@ -169,7 +171,22 @@ namespace spot // bddtrue is also used by tgba_tba_proxy if the automaton // does not use acceptance conditions. In that case, all // states are accepting. - if (*expected != bddtrue) + if (*expected == bddtrue) + { + // When degeneralizing to SBA, remove the acceptance + // conditions that are common to all outgoing + // transitions of this state. Since they are common, + // we need not fear removing them: we will see them + // eventually if we make a cycle. This helps to make + // the degeneralization idempotent. + acc -= aut->common_acceptance_conditions_of_original_state(rs); + // Use the acceptance sets common to all outgoing + // transition of the destination state. In case of a + // self-loop, we will be adding back the acceptance + // sets we removed. This is what we want. + acc |= otheracc; + } + else { // A transition in the *EXPECTED acceptance set should // be directed to the next acceptance set. If the @@ -189,6 +206,10 @@ namespace spot // month = {December} // } next = expected; + // Consider both the current acceptance sets, and the + // acceptance sets common to the outgoing transition of + // the destination state. + acc |= otheracc; while (next != cycle.end() && (acc & *next) == *next) ++next; if (next != cycle.end()) @@ -367,10 +388,11 @@ namespace spot down_cast(local_state); assert(s); - tgba_succ_iterator* it = a_->succ_iter(s->real_state(), - global_state, global_automaton); + const state* rs = s->real_state(); + tgba_succ_iterator* it = a_->succ_iter(rs, global_state, global_automaton); - return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(), + return new tgba_tba_proxy_succ_iterator(rs, it, + s->acceptance_iterator(), acc_cycle_, the_acceptance_cond_, this); } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 276873f1a..646eade63 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -92,6 +92,7 @@ TESTS = \ mixprod.test \ dupexp.test \ degendet.test \ + degenid.test \ kv.test \ reduccmp.test \ reductgba.test \ diff --git a/src/tgbatest/degenid.test b/src/tgbatest/degenid.test new file mode 100755 index 000000000..6ae6f90eb --- /dev/null +++ b/src/tgbatest/degenid.test @@ -0,0 +1,40 @@ +#!/bin/sh +# Copyright (C) 2011 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 2 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 Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs + +set -e + +# Make sure degeneralization is idempotent + +for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do + for opt in -DS -D; do + ../ltl2tgba $opt -b "$f" > autX.spot + ../ltl2tgba -X -kt autX.spot > base.size + cat base.size + for x in X XX XXX; do + ../ltl2tgba -X $opt -b aut$x.spot > autX$x.spot + ../ltl2tgba -X -kt autX$x.spot > new.size + cat new.size + cmp base.size new.size + done + done +done