From 19aae6f9cf880d3503c6b7a80334915fab3349bc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 May 2017 20:21:50 +0200 Subject: [PATCH] introduce spot::split_edges() Fixes #255. * spot/twaalgos/split.cc, spot/twaalgos/split.hh, tests/core/split.test: New files. * spot/twaalgos/Makefile.am, tests/Makefile.am: Add them. * bin/autfilt.cc (--split-edges): New option. * python/spot/impl.i: Process split.hh. * tests/python/alternating.py: Test split_edges() on an alternating automaton. --- NEWS | 11 ++++++++ bin/autfilt.cc | 46 +++++++++++++++++++----------- python/spot/impl.i | 2 ++ spot/twaalgos/Makefile.am | 12 ++++---- spot/twaalgos/split.cc | 56 +++++++++++++++++++++++++++++++++++++ spot/twaalgos/split.hh | 33 ++++++++++++++++++++++ tests/Makefile.am | 1 + tests/core/split.test | 29 +++++++++++++++++++ tests/python/alternating.py | 32 +++++++++++++++++++++ 9 files changed, 200 insertions(+), 22 deletions(-) create mode 100644 spot/twaalgos/split.cc create mode 100644 spot/twaalgos/split.hh create mode 100755 tests/core/split.test diff --git a/NEWS b/NEWS index 233e4d8ca..ca0f9904c 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,10 @@ New in spot 2.3.3.dev (not yet released) - genaut is a binary to produce families of automata defined in the literature (in the same way as we have genltl for LTL formulas). + - autfilt learned --split-edges to convert labels that are Boolean + formulas into labels that are min-terms. (See spot::split_edges() + below.) + Library: - A new library, libspotgen, gathers all functions used to generate @@ -62,6 +66,13 @@ New in spot 2.3.3.dev (not yet released) level. A similar trick was already used in sbacc(), and saves a few states in some cases. + - There is a new spot::split_edges() function that transforms edges + (labeled by Boolean formulas over atomic propositions) into + transitions (labeled by conjunctions where each atomic proposition + appear either positive or negative). This can be used to + preprocess automata before feeding them to algorithms or tools + that expect transitions labeled by letters. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5ecbf8a87..b36445d08 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -40,34 +40,35 @@ #include "common_conv.hh" #include "common_hoaread.hh" -#include -#include -#include -#include -#include #include -#include #include +#include #include #include -#include -#include #include #include -#include -#include -#include -#include #include #include #include -#include -#include -#include -#include #include -#include +#include +#include +#include +#include #include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include static const char argp_program_doc[] ="\ Convert, transform, and filter omega-automata.\v\ @@ -137,6 +138,7 @@ enum { OPT_SEED, OPT_SEP_SETS, OPT_SIMPLIFY_EXCLUSIVE_AP, + OPT_SPLIT_EDGES, OPT_STATES, OPT_STRIPACC, OPT_SUM_OR, @@ -323,6 +325,9 @@ static const argp_option options[] = { "remove-dead-states", OPT_REM_DEAD, nullptr, 0, "remove states that are unreachable, or that cannot belong to an " "infinite path", 0 }, + { "split-edges", OPT_SPLIT_EDGES, nullptr, 0, + "split edges into transitions labeled by conjunctions of all atomic " + "propositions, so they can be read as letters", 0 }, { "sum", OPT_SUM_OR, "FILENAME", 0, "build the sum with the automaton in FILENAME " "to sum languages", 0 }, @@ -497,6 +502,7 @@ static bool opt_rem_dead = false; static bool opt_rem_unreach = false; static bool opt_rem_unused_ap = false; static bool opt_sep_sets = false; +static bool opt_split_edges = false; static const char* opt_sat_minimize = nullptr; static int opt_highlight_nondet_states = -1; static int opt_highlight_nondet_edges = -1; @@ -865,6 +871,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_simplify_exclusive_ap = true; opt_merge = true; break; + case OPT_SPLIT_EDGES: + opt_split_edges = true; + break; case OPT_STATES: opt_states = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -1277,6 +1286,9 @@ namespace else if (opt_rem_unused_ap) // constrain(aut, true) already does that aut->remove_unused_ap(); + if (opt_split_edges) + aut = spot::split_edges(aut); + if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); diff --git a/python/spot/impl.i b/python/spot/impl.i index 7848babf6..493dd9f40 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -145,6 +145,7 @@ #include #include #include +#include #include #include #include @@ -563,6 +564,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index e7e435e50..38cc4136b 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -1,9 +1,9 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire -## de Recherche et Développement de l'Epita (LRDE). -## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris -## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -## Université Pierre et Marie Curie. +## Copyright (C) 2008-2017 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). +## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 +## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +## Pierre et Marie Curie. ## ## This file is part of Spot, a model checking library. ## @@ -69,6 +69,7 @@ twaalgos_HEADERS = \ relabel.hh \ remfin.hh \ remprop.hh \ + split.hh \ strength.hh \ sbacc.hh \ sccfilter.hh \ @@ -129,6 +130,7 @@ libtwaalgos_la_SOURCES = \ remfin.cc \ remprop.cc \ relabel.cc \ + split.cc \ strength.cc \ sbacc.cc \ sccinfo.cc \ diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc new file mode 100644 index 000000000..70d63f405 --- /dev/null +++ b/spot/twaalgos/split.cc @@ -0,0 +1,56 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement +// de l'Epita. +// +// 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 3 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 this program. If not, see . + +#include + +namespace spot +{ + twa_graph_ptr split_edges(const const_twa_graph_ptr& aut) + { + twa_graph_ptr out = make_twa_graph(aut->get_dict()); + out->copy_acceptance_of(aut); + out->copy_ap_of(aut); + out->prop_copy(aut, twa::prop_set::all()); + out->new_states(aut->num_states()); + out->set_init_state(aut->get_init_state_number()); + + internal::univ_dest_mapper uniq(out->get_graph()); + + bdd all = aut->ap_vars(); + for (auto& e: aut->edges()) + { + bdd cond = e.cond; + if (cond == bddfalse) + continue; + unsigned dst = e.dst; + if (aut->is_univ_dest(dst)) + { + auto d = aut->univ_dests(dst); + dst = uniq.new_univ_dests(d.begin(), d.end()); + } + while (cond != bddfalse) + { + bdd cube = bdd_satoneset(cond, all, bddfalse); + cond -= cube; + out->new_edge(e.src, dst, cube, e.acc); + } + } + return out; + } +} diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh new file mode 100644 index 000000000..8f9fae443 --- /dev/null +++ b/spot/twaalgos/split.hh @@ -0,0 +1,33 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement +// de l'Epita. +// +// 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 3 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 this program. If not, see . + +#pragma once + +#include + +namespace spot +{ + /// \brief transform edges into transitions + /// + /// Create a new version of the automaton where all edges are split + /// so that they are all labeled by a conjunction of all atomic + /// propositions. After this we can consider that each edge of the + /// automate is a transition labeled by one letter. + SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index a60920109..a4b6b7b39 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -247,6 +247,7 @@ TESTS_twa = \ core/sccdot.test \ core/sccsimpl.test \ core/sepsets.test \ + core/split.test \ core/dbacomp.test \ core/obligation.test \ core/wdba.test \ diff --git a/tests/core/split.test b/tests/core/split.test new file mode 100755 index 000000000..97b2c7075 --- /dev/null +++ b/tests/core/split.test @@ -0,0 +1,29 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 3 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 this program. If not, see . + +. ./defs + +set -e + +test 3,7 = `ltl2tgba 'a U b' --stats=%e,%t` +test 7,7 = `ltl2tgba 'a U b' | autfilt --split --stats=%e,%t` +test 12,12 = `ltl2tgba 'a U b' | autfilt -C --split --stats=%e,%t` +test 0,0 = `ltl2tgba 0 | autfilt --split --stats=%e,%t` +test 1,1 = `ltl2tgba 0 | autfilt -C --split --stats=%e,%t` diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 1ed9d1567..b883d0c4c 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -137,3 +137,35 @@ State: 4 State: 5 [0&1] 0&1&2 --END--""" + +h = spot.split_edges(aut).to_str('hoa') +print(h) +assert h == """HOA: v1 +States: 6 +Start: 0 +AP: 2 "p1" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: univ-branch trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0&!1] 1&2 {0} +[0&1] 1&2 {0} +[!0&1] 0&1 +[0&1] 0&1 +State: 1 +[0&1] 0&1&2 +State: 2 +[!0&1] 2 +[0&!1] 2 +[0&1] 2 +State: 3 +[0&!1] 1&2 +[0&1] 1&2 +[!0&1] 0&1&2 +[0&1] 0&1&2 +State: 4 +[0&1] 0&1&2 +State: 5 +[0&1] 0&1&2 +--END--"""