diff --git a/spot/twacube/Makefile.am b/spot/twacube/Makefile.am index 6fecda6f15f8bf122a9334b3633d1e52f00d04ec..ff4c4ac4340a822cf920c098eba1417c27c75a69 100644 --- a/spot/twacube/Makefile.am +++ b/spot/twacube/Makefile.am @@ -25,8 +25,9 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) twacubedir = $(pkgincludedir)/twacube -twacube_HEADERS = cube.hh +twacube_HEADERS = cube.hh twacube.hh noinst_LTLIBRARIES = libtwacube.la libtwacube_la_SOURCES = \ - cube.cc + cube.cc \ + twacube.cc diff --git a/spot/twacube/twacube.cc b/spot/twacube/twacube.cc new file mode 100644 index 0000000000000000000000000000000000000000..63abc22e2e4707b02c4f9852a28fac96183edf20 --- /dev/null +++ b/spot/twacube/twacube.cc @@ -0,0 +1,159 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Developpement 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 . + +#include "twacube.hh" +#include + +namespace spot +{ + cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_)) + { + } + cstate::cstate(unsigned int id): id_(id) + { + } + + cstate::~cstate() + { } + + unsigned int cstate::label() + { + return id_; + } + + transition::transition(transition&& t) noexcept: + cube_(std::move(t.cube_)), acc_(std::move(t.acc_)) + { } + + transition::transition(const cube& cube, + acc_cond::mark_t acc): + cube_(cube), acc_(acc) + { } + + transition::~transition() + { } + + transition::transition() + { } + + twacube::twacube(const std::vector& aps): + init_(0U), aps_(aps), cubeset_(aps.size()) + { + } + + twacube::~twacube() + { + spot::cubeset cs = get_cubeset(); + for (unsigned int i = 1; i <= theg_.num_edges(); ++i) + cs.release(theg_.edge_data(i).cube_); + } + + const acc_cond& twacube::acc() const + { + return acc_; + } + + acc_cond& twacube::acc() + { + return acc_; + } + + const std::vector& twacube::get_ap() + { + return aps_; + } + + unsigned int twacube::new_state() + { + return theg_.new_state(); + } + + void twacube::set_initial(unsigned int init) + { + init_ = init; + } + + unsigned int twacube::get_initial() + { + if (theg_.num_states() == 0) + new_state(); + + return init_; + } + + cstate* twacube::state_from_int(unsigned int i) + { + return &theg_.state_data(i); + } + + void + twacube::create_transition(unsigned int src, const cube& cube, + const acc_cond::mark_t& mark, unsigned int dst) + { + theg_.new_edge(src, dst, cube, mark); + } + + const cubeset& + twacube::get_cubeset() const + { + return cubeset_; + } + + bool + twacube::succ_contiguous() const + { + unsigned int i = 1; + while (i <= theg_.num_edges()) + { + unsigned int j = i; + + // Walk first bucket of successors + while (j <= theg_.num_edges() && + theg_.edge_storage(i).src == theg_.edge_storage(j).src) + ++j; + + // Remove the next bucket + unsigned int itmp = j; + + // Look if there are some transitions missing in this bucket. + while (j <= theg_.num_edges()) + { + if (theg_.edge_storage(i).src == theg_.edge_storage(j).src) + return false; + ++j; + } + i = itmp; + } + return true; + } + + std::ostream& + operator<<(std::ostream& os, const twacube& twa) + { + spot::cubeset cs = twa.get_cubeset(); + os << "init : " << twa.init_ << '\n'; + for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i) + os << twa.theg_.edge_storage(i).src << "->" + << twa.theg_.edge_storage(i).dst << " : " + << cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_) + << ' ' << twa.theg_.edge_data(i).acc_ + << '\n'; + return os; + } +} diff --git a/spot/twacube/twacube.hh b/spot/twacube/twacube.hh new file mode 100644 index 0000000000000000000000000000000000000000..21513ca9cd837e640a71c3da157bc7e70b30c859 --- /dev/null +++ b/spot/twacube/twacube.hh @@ -0,0 +1,153 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016 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 . + +#pragma once + +#include +#include +#include +#include +#include + +namespace spot +{ + class SPOT_API cstate + { + public: + cstate() {} + cstate(const cstate& s) = delete; + cstate(cstate&& s) noexcept; + cstate(unsigned int id); + virtual ~cstate(); + unsigned int label(); + private: + unsigned int id_; + }; + + class SPOT_API transition + { + public: + cube cube_; + acc_cond::mark_t acc_; + transition(); + transition(const transition& t) = delete; + transition(transition&& t) noexcept; + transition(const cube& cube, acc_cond::mark_t acc); + virtual ~transition(); + }; + + class SPOT_API trans_index final + { + public: + typedef digraph graph_t; + typedef graph_t::edge_storage_t edge_storage_t; + + trans_index(trans_index& ci) = delete; + trans_index(unsigned int state, graph_t& g): + st_(g.state_storage(state)) + { + reset(); + } + + trans_index(trans_index&& ci): + idx_(ci.idx_), + st_(ci.st_) + { + } + + inline void reset() + { + idx_ = st_.succ; + } + + inline void next() + { + ++idx_; + } + + inline bool done() const + { + return !idx_ || idx_ > st_.succ_tail; + } + + inline unsigned int current(unsigned int seed = 0) const + { + // no-swarming : since twacube are dedicated for parallelism, i.e. + // swarming, we expect swarming is activated. + if (SPOT_UNLIKELY(!seed)) + return idx_; + // swarming. + return (((idx_-st_.succ+1)*seed) % (st_.succ_tail-st_.succ+1)) + st_.succ; + } + + private: + unsigned int idx_; + const graph_t::state_storage_t& st_; + }; + + class SPOT_API twacube final + { + public: + twacube() = delete; + twacube(const std::vector& aps); + virtual ~twacube(); + const acc_cond& acc() const; + acc_cond& acc(); + const std::vector& get_ap(); + unsigned int new_state(); + void set_initial(unsigned int init); + unsigned int get_initial(); + cstate* state_from_int(unsigned int i); + void create_transition(unsigned int src, const cube& cube, + const acc_cond::mark_t& mark, unsigned int dst); + const cubeset& get_cubeset() const; + bool succ_contiguous() const; + typedef digraph graph_t; + const graph_t& get_graph() + { + return theg_; + } + typedef graph_t::edge_storage_t edge_storage_t; + const graph_t::edge_storage_t& + trans_storage(std::shared_ptr ci, + unsigned int seed = 0) const + { + return theg_.edge_storage(ci->current(seed)); + } + const transition& trans_data(std::shared_ptr ci, + unsigned int seed = 0) const + { + return theg_.edge_data(ci->current(seed)); + } + + std::shared_ptr succ(unsigned int i) + { + return std::make_shared(i, theg_); + } + + friend SPOT_API std::ostream& operator<<(std::ostream& os, + const twacube& twa); + private: + unsigned int init_; + acc_cond acc_; + const std::vector& aps_; + graph_t theg_; + cubeset cubeset_; + }; +} diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc index 3a434b1f1a916c2329d26da014852d00af0a53b1..53daca648f4b615aa125cb206df872f60b1463ba 100644 --- a/spot/twacube_algos/convert.cc +++ b/spot/twacube_algos/convert.cc @@ -58,4 +58,76 @@ namespace spot } return result; } + + spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut, + std::unordered_map& ap_binder, + std::vector& aps) + { + // Declare the twa cube + spot::twacube* tg = new spot::twacube(aps); + + // Fix acceptance + tg->acc() = aut->acc(); + + // This binder maps twagraph indexes to twacube ones. + std::unordered_map st_binder; + + // Fill binder and create corresponding states into twacube + for (unsigned n = 0; n < aut->num_states(); ++n) + st_binder.insert({n, tg->new_state()}); + + // Fix the initial state + tg->set_initial(st_binder[aut->get_init_state_number()]); + + // Get the cubeset + auto cs = tg->get_cubeset(); + + // Now just build all transitions of this automaton + // spot::cube cube(aps); + for (unsigned n = 0; n < aut->num_states(); ++n) + for (auto& t: aut->out(n)) + { + bdd cond = t.cond; + + // Special case for bddfalse + if (cond == bddfalse) + { + spot::cube cube = tg->get_cubeset().alloc(); + for (unsigned int i = 0; i < cs.size(); ++i) + cs.set_false_var(cube, i); // FIXME ! use fill! + tg->create_transition(st_binder[n], cube, + t.acc, st_binder[t.dst]); + } + else + // Split the bdd into multiple transitions + while (cond != bddfalse) + { + bdd one = bdd_satone(cond); + cond -= one; + spot::cube cube =spot::satone_to_cube(one, cs, ap_binder); + tg->create_transition(st_binder[n], cube, t.acc, + st_binder[t.dst]); + } + } + // Must be contiguous to support swarming. + assert(tg->succ_contiguous()); + return tg; + } + + std::vector* + extract_aps(spot::twa_graph_ptr& aut, + std::unordered_map& ap_binder) + { + std::vector* aps = new std::vector(); + for (auto f: aut->ap()) + { + int size = aps->size(); + if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end()) + { + aps->push_back(f.ap_name()); + ap_binder.insert({aut->get_dict()->var_map[f], size}); + } + } + return aps; + } } diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh index 313b114e146094d5d68e02ebefce59f2836eb8b0..7f3d8c55a52a8815777bdbe861cc47070d861eee 100644 --- a/spot/twacube_algos/convert.hh +++ b/spot/twacube_algos/convert.hh @@ -24,6 +24,8 @@ #include #include #include +#include +#include namespace spot { @@ -37,4 +39,15 @@ namespace spot /// that bind cube indexes to bdd indexes. SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset, std::unordered_map& reverse_binder); + + /// \brief Extract the atomic propositions from the automaton + SPOT_API std::vector* + extract_aps(spot::twa_graph_ptr& aut, + std::unordered_map& ap_binder); + + /// \brief Convert a twa into a twacube + SPOT_API spot::twacube* + twa_to_twacube(spot::twa_graph_ptr& aut, + std::unordered_map& ap_binder, + std::vector& aps); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 1c8617cb78ae13f6cf51f553b94df02af9f722e6..8a07b91fc3b979ac8120235057200d2d1be684c7 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -99,7 +99,8 @@ check_PROGRAMS = \ core/tgbagraph \ core/tostring \ core/tunabbrev \ - core/tunenoform + core/tunenoform \ + core/twacube # Keep this sorted alphabetically. core_acc_SOURCES = core/acc.cc @@ -150,6 +151,7 @@ core_tunabbrev_SOURCES = core/equalsf.cc core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' core_tunenoform_SOURCES = core/equalsf.cc core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"' +core_twacube_SOURCES = core/twacube.cc TESTS_tl = \ @@ -328,7 +330,8 @@ TESTS_twa = \ core/parity.test \ core/parity2.test \ core/ltlsynt.test \ - core/rabin2parity.test + core/rabin2parity.test \ + core/twacube.test ############################## PYTHON ############################## diff --git a/tests/core/.gitignore b/tests/core/.gitignore index 4e87ead2b7c61d87c94bfbc450f2f74e5081e4d4..6c7c4a1dcad9f85ce1a8101ad0da1b0ad9ff9a90 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -74,5 +74,6 @@ tripprod trival tunabbrev tunenoform +twacube unabbrevwm safra diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc new file mode 100644 index 0000000000000000000000000000000000000000..08ab2532325bf32f79959b1afb33d4d5b6e53dc6 --- /dev/null +++ b/tests/core/twacube.cc @@ -0,0 +1,73 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016 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 + +#include +#include +#include +#include +#include +#include +#include + +int main() +{ + // Build some TWA + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + bdd p1 = bdd_ithvar(tg->register_ap("p1")); + bdd p2 = bdd_ithvar(tg->register_ap("p2")); + tg->acc().add_sets(2); + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + tg->new_edge(s1, s1, bddfalse, 0U); + tg->new_edge(s1, s2, p1, 0U); + tg->new_edge(s1, s3, p2, tg->acc().mark(1)); + tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); + tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1})); + tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1})); + + // Map Bdd indexes to cube indexes + std::unordered_map ap_binder; + + // Get the set of propositions used by this automaton + std::vector* aps = extract_aps(tg, ap_binder); + + // Test translation + auto* aut = twa_to_twacube(tg, ap_binder, *aps); + spot::print_dot(std::cout, tg); + std::cout << "-----------\n" << *aut << "-----------\n"; + + unsigned int seed = 17; + for (auto it = aut->succ(2); !it->done(); it->next()) + { + auto& t = aut->trans_storage(it, seed); + auto& d = aut->trans_data(it, seed); + std::cout << t.src << ' ' << t.dst << ' ' + << ' ' << aut->get_cubeset().dump(d.cube_, *aps) + << ' ' << d.acc_ + << std::endl; + } + + delete aps; + delete aut; +} diff --git a/tests/core/twacube.test b/tests/core/twacube.test new file mode 100755 index 0000000000000000000000000000000000000000..125e178297c10fbe612bb32ee5ab2376691706d2 --- /dev/null +++ b/tests/core/twacube.test @@ -0,0 +1,71 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014, 2015 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 . + +# While running some benchmark, Tomáš Babiak found that Spot took too +# much time (i.e. >1h) to translate those six formulae. It turns out +# that the WDBA minimization was performed after the degeneralization +# algorithm, while this is not necessary (WDBA will produce a BA, so +# we may as well skip degeneralization). Translating these formulae +# in the test-suite ensure that they don't take too much time (the +# buildfarm will timeout if it does). + +. ./defs + +set -e + +run 0 ../twacube > stdout + +cat >expected < 0 + 0 [label="0"] + 0 -> 0 [label="0"] + 0 -> 1 [label="p1"] + 0 -> 2 [label="p2\n{1}"] + 1 [label="1"] + 1 -> 2 [label="p1 & p2\n{0}"] + 2 [label="2"] + 2 -> 0 [label="p1 | p2\n{0,1}"] + 2 -> 1 [label="!p1 | p2"] + 2 -> 2 [label="1\n{0,1}"] +} +----------- +init : 0 +0->0 : !p1&!p2 {} +0->1 : p1 {} +0->2 : p2 {1} +1->2 : p1&p2 {0} +2->0 : !p1&p2 {0,1} +2->0 : p1 {0,1} +2->1 : !p1 {} +2->1 : p1&p2 {} +2->2 : 1 {0,1} +----------- +2 1 !p1 {} +2 2 1 {0,1} +2 0 p1 {0,1} +2 1 p1&p2 {} +2 0 !p1&p2 {0,1} +EOF + +diff stdout expected