From e4bfebf36f5ce6b9d44ad1fe03d389d63ebc62de Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Tue, 21 Jun 2022 13:54:32 +0200 Subject: [PATCH] twaalgos: add LTL to AA translation --- python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/translate_aa.cc | 320 ++++++++++++++++++++++++++++++++++ spot/twaalgos/translate_aa.hh | 32 ++++ 4 files changed, 356 insertions(+) create mode 100644 spot/twaalgos/translate_aa.cc create mode 100644 spot/twaalgos/translate_aa.hh diff --git a/python/spot/impl.i b/python/spot/impl.i index 09e29f6e9..471b85cbb 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -163,6 +163,7 @@ #include #include #include +#include #include #include #include @@ -790,6 +791,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 8e5b929d0..432f1a85d 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -99,6 +99,7 @@ twaalgos_HEADERS = \ totgba.hh \ toweak.hh \ translate.hh \ + translate_aa.hh \ word.hh \ zlktree.hh @@ -177,6 +178,7 @@ libtwaalgos_la_SOURCES = \ totgba.cc \ toweak.cc \ translate.cc \ + translate_aa.cc \ word.cc \ zlktree.cc diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc new file mode 100644 index 000000000..0663651de --- /dev/null +++ b/spot/twaalgos/translate_aa.cc @@ -0,0 +1,320 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013-2018, 2020-2021 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 . + +#include "config.h" +#include +#include +#include + +#include + +namespace spot +{ + namespace + { + struct ltl_to_aa_builder + { + ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink) + : aut_(aut) + , accepting_sink_(accepting_sink) + , uniq_(aut_->get_graph(), accepting_sink) + , oe_(aut_, accepting_sink) + { + } + + twa_graph_ptr aut_; + unsigned accepting_sink_; + internal::univ_dest_mapper uniq_; + outedge_combiner oe_; + + unsigned recurse(formula f) + { + switch (f.kind()) + { + case op::ff: + return aut_->new_state(); + + case op::tt: + { + unsigned init_state = aut_->new_state(); + aut_->new_edge(init_state, accepting_sink_, bddtrue, {}); + return init_state; + } + + case op::ap: + case op::Not: + { + unsigned init_state = aut_->new_state(); + + bdd ap; + if (f.kind() == op::ap) + ap = bdd_ithvar(aut_->register_ap(f.ap_name())); + else + ap = bdd_nithvar(aut_->register_ap(f[0].ap_name())); + + aut_->new_edge(init_state, accepting_sink_, ap, {}); + return init_state; + } + + // FIXME: is this right for LTLf? + case op::strong_X: + case op::X: + { + unsigned sub_init_state = recurse(f[0]); + unsigned new_init_state = aut_->new_state(); + aut_->new_edge(new_init_state, sub_init_state, bddtrue, {}); + return new_init_state; + } + + case op::Or: + { + unsigned init_state = aut_->new_state(); + + for (const auto& sub_formula : f) + { + unsigned sub_init = recurse(sub_formula); + for (auto& e : aut_->out(sub_init)) + { + unsigned dst = e.dst; + if (aut_->is_univ_dest(e.dst)) + { + auto dests = aut_->univ_dests(e); + dst = uniq_.new_univ_dests(dests.begin(), dests.end()); + } + aut_->new_edge(init_state, dst, e.cond, {}); + } + } + + return init_state; + } + + case op::And: + { + unsigned init_state = aut_->new_state(); + + outedge_combiner oe(aut_, accepting_sink_); + bdd comb = bddtrue; + for (const auto& sub_formula : f) + { + unsigned sub_init = recurse(sub_formula); + comb &= oe_(sub_init); + } + oe_.new_dests(init_state, comb); + + return init_state; + } + + case op::U: + case op::W: + { + auto acc = f.kind() == op::U + ? acc_cond::mark_t{0} + : acc_cond::mark_t{}; + + unsigned init_state = aut_->new_state(); + + unsigned lhs_init = recurse(f[0]); + unsigned rhs_init = recurse(f[1]); + + std::vector new_dests; + for (auto& e : aut_->out(lhs_init)) + { + auto dests = aut_->univ_dests(e); + std::copy(dests.begin(), dests.end(), + std::back_inserter(new_dests)); + new_dests.push_back(init_state); + + unsigned dest = uniq_.new_univ_dests(new_dests.begin(), + new_dests.end()); + aut_->new_edge(init_state, dest, e.cond, acc); + + new_dests.clear(); + } + + for (auto& e : aut_->out(rhs_init)) + { + unsigned dst = e.dst; + if (aut_->is_univ_dest(e.dst)) + { + auto dests = aut_->univ_dests(e); + dst = uniq_.new_univ_dests(dests.begin(), dests.end()); + } + aut_->new_edge(init_state, dst, e.cond, {}); + } + + return init_state; + } + + case op::R: + case op::M: + { + auto acc = f.kind() == op::M + ? acc_cond::mark_t{0} + : acc_cond::mark_t{}; + + unsigned init_state = aut_->new_state(); + + unsigned lhs_init = recurse(f[0]); + unsigned rhs_init = recurse(f[1]); + + std::vector new_dests; + for (auto& e : aut_->out(rhs_init)) + { + auto dests = aut_->univ_dests(e); + std::copy(dests.begin(), dests.end(), + std::back_inserter(new_dests)); + new_dests.push_back(init_state); + + unsigned dst = uniq_.new_univ_dests(new_dests.begin(), + new_dests.end()); + aut_->new_edge(init_state, dst, e.cond, acc); + + new_dests.clear(); + } + + std::vector dsts; + for (const auto& lhs_e : aut_->out(lhs_init)) + { + const auto& lhs_dsts = aut_->univ_dests(lhs_e); + std::copy(lhs_dsts.begin(), lhs_dsts.end(), + std::back_inserter(dsts)); + size_t lhs_dest_num = dsts.size(); + + for (const auto& rhs_e : aut_->out(rhs_init)) + { + const auto& rhs_dsts = aut_->univ_dests(rhs_e); + std::copy(rhs_dsts.begin(), rhs_dsts.end(), + std::back_inserter(dsts)); + + bdd cond = lhs_e.cond & rhs_e.cond; + + unsigned dst = uniq_.new_univ_dests(dsts.begin(), + dsts.end()); + aut_->new_edge(init_state, dst, cond, {}); + + // reset to only lhs' current edge destinations + dsts.resize(lhs_dest_num); + } + dsts.clear(); + } + + return init_state; + } + + // F(phi) = tt U phi + case op::F: + { + auto acc = acc_cond::mark_t{0}; + + // if phi is boolean then we can reuse its initial state (otherwise + // we can't because of potential self loops) + if (f[0].is_boolean()) + { + unsigned init_state = recurse(f[0]); + aut_->new_edge(init_state, init_state, bddtrue, acc); + return init_state; + } + + unsigned init_state = aut_->new_state(); + unsigned sub_init = recurse(f[0]); + + aut_->new_edge(init_state, init_state, bddtrue, acc); + + for (auto& e : aut_->out(sub_init)) + aut_->new_edge(init_state, e.dst, e.cond, {}); + + return init_state; + } + + // G phi = ff R phi + case op::G: + { + unsigned init_state = aut_->new_state(); + + unsigned sub_init = recurse(f[0]); + + // translate like R, but only the self loop part; `ff` cancels out + // the product of edges + std::vector new_dests; + for (auto& e : aut_->out(sub_init)) + { + auto dests = aut_->univ_dests(e); + std::copy(dests.begin(), dests.end(), + std::back_inserter(new_dests)); + new_dests.push_back(init_state); + + unsigned dst = uniq_.new_univ_dests(new_dests.begin(), + new_dests.end()); + aut_->new_edge(init_state, dst, e.cond, {}); + + new_dests.clear(); + } + + return init_state; + } + + case op::eword: + case op::Xor: + case op::Implies: + case op::Equiv: + case op::Closure: + case op::NegClosure: + case op::NegClosureMarked: + case op::EConcat: + case op::EConcatMarked: + case op::UConcat: + case op::OrRat: + case op::AndRat: + case op::AndNLM: + case op::Concat: + case op::Fusion: + case op::Star: + case op::FStar: + case op::first_match: + SPOT_UNREACHABLE(); + return -1; + } + + SPOT_UNREACHABLE(); + } + }; + } + + twa_graph_ptr + ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states) + { + SPOT_ASSERT(f.is_ltl_formula()); + f = negative_normal_form(f); + + auto aut = make_twa_graph(dict); + aut->set_co_buchi(); + + unsigned accepting_sink = aut->new_state(); + aut->new_edge(accepting_sink, accepting_sink, bddtrue, {}); + auto builder = ltl_to_aa_builder(aut, accepting_sink); + + unsigned init_state = builder.recurse(f); + aut->set_init_state(init_state); + + if (purge_dead_states) + aut->purge_dead_states(); + + return aut; + } +} diff --git a/spot/twaalgos/translate_aa.hh b/spot/twaalgos/translate_aa.hh new file mode 100644 index 000000000..9a8760072 --- /dev/null +++ b/spot/twaalgos/translate_aa.hh @@ -0,0 +1,32 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2005, 2006 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. +// +// 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 + +namespace spot +{ + SPOT_API twa_graph_ptr + ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states = false); +}