alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

scc_map: fix computation of ap_set_of, and (indirectly) aprec_set_of

Browse source 
Reported by Étienne Renault.

* src/tgbaalgos/scc.cc (build_map): Update root_.frond().supp for all
transitions leaving the top state, not only those causing a merge.
* src/tgbaalgos/scc.hh (ap_set_of): Clarify documentation.
* src/tgbatest/kv.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-12 09:39:29 +02:00
parent 561b852106
commit 08175025c9
3 changed files with 28 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tgbaalgos/scc.cc
View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
// Developpement de l'Epita.
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -212,6 +213,7 @@ namespace spot
++self_loops_;
bdd acc = succ->current_acceptance_conditions();
bdd cond = succ->current_condition();
root_.front().supp &= bdd_support(cond);
// ... and point the iterator to the next successor, for
// the next iteration.
succ->next();
@ -268,7 +270,7 @@ namespace spot
succ_type succs;
cond_set conds;
conds.insert(cond);
bdd supp = bdd_support(cond);
bdd supp = bddtrue;
bdd all = aut_->all_acceptance_conditions();
bdd useful = conv.as_full_product(acc);
while (threshold > root_.front().index)

13
src/tgbaalgos/scc.hh
View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Developpement de l'Epita.
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -122,10 +123,14 @@ namespace spot
/// \pre This should only be called once build_map() has run.
const cond_set& cond_set_of(unsigned n) const;
/// \brief Return the set of atomic properties occurring in an SCC.
/// \brief Return the set of atomic properties occurring on the
/// transitions leaving states from SCC \a n.
///
/// The transitions considered are all transitions inside SCC
/// \a n, as well as the transitions leaving SCC \a n.
///
/// \return a BDD that is a conjuction of all atomic properties
/// occurring on the transitions in the SCC n.
/// occurring on the transitions leaving the states of SCC \a n.
///
/// \pre This should only be called once build_map() has run.
bdd ap_set_of(unsigned n) const;

16
src/tgbatest/kv.test
View file

@ -1,6 +1,7 @@
#!/bin/sh
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
# Development de l'EPITA.
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@ -40,3 +41,14 @@ check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
# Make sure escaped variables print OK.
check '"G1"U"GG" && "FF"'
# Make sure we count 4 atomic propositions in
# G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"
# even after iterated simulation
# Report from Etienne Renault.
../ltl2tgba -KV -R3 -RIS >out \
'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'
x=`sed -n '/APre/{s/.*APrec=\[\([^]]*\)\].*/\1/p;q}' out | tr ' ' '\n' | wc -l`
test "$x" = 4