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

hoa: simplify the interface of hoa_reachable()

Browse source 
* src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh: Only
keep one function public, and do not pass the formula.
* src/tgbatest/ltl2tgba.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-04 18:00:32 +01:00
parent cbf1e15b01
commit 490c97d797
3 changed files with 25 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/tgbaalgos/hoa.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et
// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -30,7 +30,6 @@
#include "misc/bddlt.hh"
#include "misc/minato.hh"
#include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh"
#include "ltlast/atomic_prop.hh"
namespace spot
@ -230,11 +229,20 @@ namespace spot
}
enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
enum hoa_acceptance
{
Hoa_Acceptance_States, /// state-based acceptance if
/// (globally) possible
/// transition-based acceptance
/// otherwise.
Hoa_Acceptance_Transitions, /// transition-based acceptance globally
Hoa_Acceptance_Mixed /// mix state-based and transition-based
};
std::ostream&
hoa_reachable(std::ostream& os,
const const_tgba_ptr& aut,
const ltl::formula* f,
hoa_acceptance acceptance,
hoa_alias alias,
bool newline)
@ -253,8 +261,6 @@ namespace spot
auto n = aut->get_named_prop<std::string>("automaton-name");
if (n)
escape_str(os << "name: \"", *n) << '"' << nl;
else if (f)
escape_str(os << "name: \"", to_string(f)) << '"' << nl;
os << "States: " << num_states << nl
<< "Start: 0" << nl
<< "AP: " << md.vap.size();
@ -331,8 +337,7 @@ namespace spot
std::ostream&
hoa_reachable(std::ostream& os,
const const_tgba_ptr& aut,
const char* opt,
const ltl::formula* f)
const char* opt)
{
bool newline = true;
hoa_acceptance acceptance = Hoa_Acceptance_States;
@ -357,7 +362,7 @@ namespace spot
break;
}
}
return hoa_reachable(os, aut, f, acceptance, alias, newline);
return hoa_reachable(os, aut, acceptance, alias, newline);
}
}

37
src/tgbaalgos/hoa.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -21,46 +21,23 @@
# define SPOT_TGBAALGOS_HOA_HH
#include <iosfwd>
#include "ltlast/formula.hh"
#include "misc/common.hh"
#include "tgba/fwd.hh"
namespace spot
{
enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
enum hoa_acceptance
{
Hoa_Acceptance_States, /// state-based acceptance if
/// (globally) possible
/// transition-based acceptance
/// otherwise.
Hoa_Acceptance_Transitions, /// transition-based acceptance globally
Hoa_Acceptance_Mixed /// mix state-based and transition-based
};
/// \ingroup tgba_io
/// \brief Print reachable states in Hanoi Omega Automata format.
///
/// \param os The output stream to print on.
/// \param g The automaton to output.
/// \param f The (optional) formula associated to the automaton. If given
/// it will be output as a comment.
/// \param acceptance Force the type of acceptance mode used
/// in output.
/// \param alias Whether aliases should be used in output.
/// \param newlines Whether to use newlines in output.
/// \param opt a set of characters each corresponding to a possible
/// option: (s) state-based acceptance, (t) transition-based
/// acceptance, (m) mixed acceptance, (l) single-line output.
SPOT_API std::ostream&
hoa_reachable(std::ostream& os,
const const_tgba_ptr& g,
const ltl::formula* f = 0,
hoa_acceptance acceptance = Hoa_Acceptance_States,
hoa_alias alias = Hoa_Alias_None,
bool newlines = true);
SPOT_API std::ostream&
hoa_reachable(std::ostream& os,
const const_tgba_ptr& g,
const char* opt,
const ltl::formula* f = 0);
const char* opt);
}
#endif // SPOT_TGBAALGOS_HOA_HH

7
src/tgbatest/ltl2tgba.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
@ -1572,6 +1572,9 @@ checked_main(int argc, char** argv)
}
}
if (f)
a->set_named_prop("automaton-name", new std::string(to_string(f)));
if (output != -1)
{
tm.start("producing output");
@ -1701,7 +1704,7 @@ checked_main(int argc, char** argv)
}
case 17:
{
hoa_reachable(std::cout, a, hoa_opt, f) << '\n';
hoa_reachable(std::cout, a, hoa_opt) << '\n';
break;
}
default: