Commit 02b5460b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

dot, hoa: default to "k" for kripke structure

* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc: If a Kripke
structure is passed, automatically enable the "k" option.
* tests/core/parse_print_test.cc, tests/ltsmin/modelcheck.cc,
tests/python/ltsmin.ipynb: Remove the explicit use of "k".
* NEWS: Mention the change.
parent a9b4560f
......@@ -6,7 +6,7 @@ New in spot 1.99.7a (not yet released)
exception instead of using an assertion that could be disabled.
* The load_ltsmin() function has been split in two. Now you should
first call ltsmin_model::load(filename) to create an ltlmin_model,
first call ltsmin_model::load(filename) to create an ltsmin_model,
and then call the ltsmin_model::kripke(...) method to create an
automaton that can be iterated on the fly. The intermediate
object can be queried about the supported variables and their
......@@ -23,6 +23,9 @@ New in spot 1.99.7a (not yet released)
possible. This is similar to the "k" option already supported
by print_hoa(), and is useful when printing Kripke structures.
* Option "k" is automatically passed used by print_dot() and
print_hoa() when printing Kripke structures.
Python:
* The ltsmin interface has been binded in Python. See
......
......@@ -31,6 +31,7 @@
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/kripke/kripke.hh>
#include <cstdlib>
#include <cstring>
#include <algorithm>
......@@ -663,6 +664,9 @@ namespace spot
const char* options)
{
dotty_output d(os, options);
// Enable automatic state labels for Kripke structure.
if (std::dynamic_pointer_cast<const kripke>(g))
d.parse_opts("k");
auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states()))
aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1);
......
......@@ -33,6 +33,7 @@
#include <spot/misc/minato.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/tl/formula.hh>
#include <spot/kripke/kripke.hh>
namespace spot
{
......@@ -575,15 +576,28 @@ namespace spot
std::ostream&
print_hoa(std::ostream& os,
const const_twa_ptr& aut,
const char* opt)
const const_twa_ptr& aut,
const char* opt)
{
auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
if (!a)
a = make_twa_graph(aut, twa::prop_set::all());
return print_hoa(os, a, opt);
// for Kripke structures, automatically append "k" to the options.
char* tmpopt = nullptr;
if (std::dynamic_pointer_cast<const kripke>(aut))
{
unsigned n = opt ? strlen(opt) : 0;
tmpopt = new char[n + 2];
if (opt)
strcpy(tmpopt, opt);
tmpopt[n] = 'k';
tmpopt[n + 1] = 0;
}
print_hoa(os, a, tmpopt ? tmpopt : opt);
delete[] tmpopt;
return os;
}
}
......@@ -44,7 +44,7 @@ int main(int argc, char** argv)
}
if (!paut->ks)
break;
print_hoa(std::cout, paut->ks, "k");
print_hoa(std::cout, paut->ks);
}
return return_value;
}
......@@ -243,7 +243,7 @@ checked_main(int argc, char **argv)
if (output == Kripke)
{
tm.start("kripke output");
spot::print_hoa(std::cout, model, "k");
spot::print_hoa(std::cout, model);
tm.stop("kripke output");
goto safe_exit;
}
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment