Commit f26dd904 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: better support for explicit Kripke

Part of issue #376, reported by Hashim Ali.

* python/spot/impl.i: Add bindings for kripke_graph.
* python/spot/__init__.py (automaton): Add a want_kripke option.
* spot/kripke/kripkegraph.hh: Honnor the "state-names" property
when displaying states.
* spot/twaalgos/hoa.cc: Preserve names of Kripke states.
* tests/python/ltsmin-dve.ipynb: Illustrate all the above.
* NEWS: Mention those changes.
* THANKS: Add Hashim.
parent a86925e2
Pipeline #6441 passed with stages
in 226 minutes and 12 seconds
......@@ -4,7 +4,7 @@ New in spot 2.7.0.dev (not yet release)
- Work around GCC bug #89303, that causes memory leaks and std::weak_bad_ptr
exceptions when Spot is compiled with the version of g++ 8.2 currently
distributed with Debian (starting with 8.2.0-15).
distributed by Debian unstable (starting with g++ 8.2.0-15).
Python:
......@@ -17,6 +17,20 @@ New in spot 2.7.0.dev (not yet release)
- unregister_all_my_variables(for_me)
- unregister_variable(var, for_me)
- Better support for explicit Kripke structures
- the kripke_graph type now has bindings
- spot.automaton() and spot.automata() now support a want_kripke=True
to return a kripke_graph
See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html
for some examples.
Library:
- Printing Kripke structures via print_hoa() will save state names.
- kripke_graph_ptr objects now honnor any "state-names" property
when formating states.
Bugs fixed:
- The print_dot_psl() function would incorrectly number all but the
......@@ -38,7 +52,7 @@ New in spot 2.7.0.dev (not yet release)
suspendable automaton could incorrectly build transition-based
automata when multipliying two state-based automata. This caused
ltl2tgba to emit error messages such as: "automaton has
transition-based acceptance despite prop_state_acc()==true"
transition-based acceptance despite prop_state_acc()==true".
New in spot 2.7 (2018-12-11)
......
......@@ -17,6 +17,7 @@ Felix Klaedtke
Florian Perlié-Long
František Blahoudek
Gerard J. Holzmann
Hashim Ali
Heikki Tauriainen
Henrich Lauko
Jan Strejček
......
# -*- coding: utf-8 -*-
# Copyright (C) 2014-2018 Laboratoire de
# Copyright (C) 2014-2019 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -367,7 +367,8 @@ class atomic_prop_set:
def automata(*sources, timeout=None, ignore_abort=True,
trust_hoa=True, no_sid=False, debug=False):
trust_hoa=True, no_sid=False, debug=False,
want_kripke=False):
"""Read automata from a list of sources.
Parameters
......@@ -386,6 +387,10 @@ def automata(*sources, timeout=None, ignore_abort=True,
trust_hoa : bool, optional
If True (the default), supported HOA properies that
cannot be easily verified are trusted.
want_kripke : bool, optional
If True, the input is expected to discribe Kripke
structures, in the HOA format, and the returned type
will be of type kripke_graph_ptr.
no_sid : bool, optional
When an automaton is obtained from a subprocess, this
subprocess is started from a shell with its own session
......@@ -445,6 +450,8 @@ def automata(*sources, timeout=None, ignore_abort=True,
o.ignore_abort = ignore_abort
o.trust_hoa = trust_hoa
o.raise_errors = True
o.want_kripke = want_kripke
for filename in sources:
try:
p = None
......@@ -496,8 +503,9 @@ def automata(*sources, timeout=None, ignore_abort=True,
mgr = proc if proc else _supress()
with mgr:
while a:
# This returns None when we reach the end of the file.
a = p.parse(_bdd_dict).aut
# the automaton is None when we reach the end of the file.
res = p.parse(_bdd_dict)
a = res.ks if want_kripke else res.aut
if a:
yield a
finally:
......
......@@ -47,7 +47,6 @@
%shared_ptr(spot::fair_kripke)
%shared_ptr(spot::kripke)
%shared_ptr(spot::kripke_graph)
%shared_ptr(spot::kripke)
%shared_ptr(spot::ta)
%shared_ptr(spot::ta_explicit)
%shared_ptr(spot::ta_product)
......@@ -172,8 +171,9 @@
#include <spot/parseaut/public.hh>
#include <spot/kripke/kripke.hh>
#include <spot/kripke/fairkripke.hh>
#include <spot/kripke/kripke.hh>
#include <spot/kripke/kripkegraph.hh>
#include <spot/ta/ta.hh>
#include <spot/ta/tgta.hh>
......@@ -678,10 +678,11 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/complement.hh>
%include <spot/parseaut/public.hh>
%include <spot/kripke/fairkripke.hh>
%include <spot/kripke/kripke.hh>
%include <spot/kripke/kripkegraph.hh>
%include <spot/parseaut/public.hh>
%include <spot/ta/ta.hh>
%include <spot/ta/tgta.hh>
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011-2018 Laboratoire de Recherche et Développement de
// Copyright (C) 2011-2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -239,9 +239,11 @@ namespace spot
std::string format_state(unsigned n) const
{
std::stringstream ss;
ss << n;
return ss.str();
auto named = get_named_prop<std::vector<std::string>>("state-names");
if (named && n < named->size())
return (*named)[n];
return std::to_string(n);
}
virtual std::string format_state(const state* st) const override
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et
// Copyright (C) 2014-2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -304,6 +304,9 @@ namespace spot
case 'k':
state_labels = true;
break;
case 'K':
state_labels = false;
break;
case 'l':
newline = false;
break;
......@@ -732,14 +735,12 @@ namespace spot
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());
bool preserve_names = false;
// for Kripke structures, automatically append "k" to the options.
// (Unless "K" was given.)
char* tmpopt = nullptr;
if (std::dynamic_pointer_cast<const fair_kripke>(aut))
if (std::dynamic_pointer_cast<const fair_kripke>(aut) &&
(!opt || (strchr(opt, 'K') == nullptr)))
{
unsigned n = opt ? strlen(opt) : 0;
tmpopt = new char[n + 2];
......@@ -747,7 +748,13 @@ namespace spot
strcpy(tmpopt, opt);
tmpopt[n] = 'k';
tmpopt[n + 1] = 0;
preserve_names = true;
}
auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
if (!a)
a = make_twa_graph(aut, twa::prop_set::all(), preserve_names);
print_hoa(os, a, tmpopt ? tmpopt : opt);
delete[] tmpopt;
return os;
......
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