alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twaalgos: add LTL to AA translation

Browse source
This commit is contained in:
Antoine Martin 2022-06-21 13:54:32 +02:00
parent 6ebbb93024
commit e4bfebf36f
4 changed files with 356 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
python/spot/impl.i
View file

@ -163,6 +163,7 @@
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/translate_aa.hh>
#include <spot/twaalgos/toweak.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/dtwasat.hh>
@ -790,6 +791,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/stutter.hh>
%include <spot/twaalgos/synthesis.hh>
%include <spot/twaalgos/translate.hh>
%include <spot/twaalgos/translate_aa.hh>
%include <spot/twaalgos/toweak.hh>
%include <spot/twaalgos/hoa.hh>
%include <spot/twaalgos/dtwasat.hh>

2
spot/twaalgos/Makefile.am
View file

@ -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

320
spot/twaalgos/translate_aa.cc Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/translate_aa.hh>
#include <spot/tl/nenoform.hh>
#include <iostream>
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<twa_graph::graph_t> 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<unsigned> 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<unsigned> 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<unsigned> 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<unsigned> 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;
}
}

32
spot/twaalgos/translate_aa.hh Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
namespace spot
{
SPOT_API twa_graph_ptr
ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states = false);
}