Commit 27ab631c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

alternation: add a states_and algorithm

This should will come handy to implement the convertion from LTL to
alternating automata, and to handle automata with multiple initial
states.

* spot/twaalgos/alternation.hh, spot/twaalgos/alternation.cc: New files.
* spot/twaalgos/Makefile.am: Add them.
* python/spot/impl.i: Add bindings.
* tests/python/alternating.py: Test states_and.
parent 48c812a5
......@@ -113,6 +113,7 @@
#include <spot/twa/taatgba.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/dot.hh>
......@@ -507,6 +508,7 @@ def state_is_accepting(self, src) -> "bool":
// Should come after the definition of twa_graph
%include <spot/twaalgos/alternation.hh>
%include <spot/twaalgos/cleanacc.hh>
%include <spot/twaalgos/degen.hh>
%include <spot/twaalgos/dot.hh>
......@@ -932,6 +934,13 @@ unblock_signal(int signum)
return sigprocmask(SIG_UNBLOCK, &set, 0);
}
// for alternation.hh
unsigned states_and(const spot::twa_graph_ptr& aut,
const std::vector<unsigned>& il)
{
return states_and(aut, il.begin(), il.end());
}
%}
%extend spot::parse_error_list {
......
......@@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
twaalgosdir = $(pkgincludedir)/twaalgos
twaalgos_HEADERS = \
alternation.hh \
are_isomorphic.hh \
bfssteps.hh \
canonicalize.hh \
......@@ -84,6 +85,7 @@ twaalgos_HEADERS = \
noinst_LTLIBRARIES = libtwaalgos.la
libtwaalgos_la_SOURCES = \
alternation.cc \
are_isomorphic.cc \
bfssteps.cc \
canonicalize.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 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 <http://www.gnu.org/licenses/>.
#include <spot/twaalgos/alternation.hh>
#include <algorithm>
#include <spot/misc/minato.hh>
namespace spot
{
outedge_combiner::outedge_combiner(const twa_graph_ptr& aut)
: aut_(aut), vars_(bddtrue)
{
}
outedge_combiner::~outedge_combiner()
{
aut_->get_dict()->unregister_all_my_variables(this);
}
bdd outedge_combiner::operator()(unsigned st)
{
const auto& dict = aut_->get_dict();
bdd res = bddtrue;
for (unsigned d1: aut_->univ_dests(st))
{
bdd res2 = bddfalse;
for (auto& e: aut_->out(d1))
{
bdd out = bddtrue;
for (unsigned d: aut_->univ_dests(e.dst))
{
auto p = state_to_var.emplace(d, 0);
if (p.second)
{
int v = dict->register_anonymous_variables(1, this);
p.first->second = v;
var_to_state.emplace(v, d);
vars_ &= bdd_ithvar(v);
}
out &= bdd_ithvar(p.first->second);
}
res2 |= e.cond & out;
}
res &= res2;
}
return res;
}
void outedge_combiner::new_dests(unsigned st, bdd out) const
{
minato_isop isop(out);
bdd cube;
std::vector<unsigned> univ_dest;
while ((cube = isop.next()) != bddfalse)
{
bdd cond = bdd_exist(cube, vars_);
bdd dest = bdd_existcomp(cube, vars_);
while (dest != bddtrue)
{
assert(bdd_low(dest) == bddfalse);
auto it = var_to_state.find(bdd_var(dest));
assert(it != var_to_state.end());
univ_dest.push_back(it->second);
dest = bdd_high(dest);
}
std::sort(univ_dest.begin(), univ_dest.end());
aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond);
univ_dest.clear();
}
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/twa/twagraph.hh>
#include <utility>
namespace spot
{
/// \brief Helper class combine outgoing edges in alternating
/// automata
///
/// The idea is that you can the operator() on some state to get an
/// BDD representation of its outgoing edges (labels and
/// destinations, but not acceptance marks). The BDD representation
/// of different states can combined using & or | to build a new
/// representation of some outgoing edges that can be attached to
/// some state with new_dests. The use of BDDs helps removing
/// superfluous edges.
///
/// Beware that new_dests() just *appends* the transitions to the
/// supplied state, it does not remove existing ones.
///
/// operator() can be called on states with universal branching
/// (that's actually the point), and can be called on state number
/// that designate groupes of destination states (in that case the
/// conjunction of all those states are taken).
class SPOT_API outedge_combiner
{
private:
const twa_graph_ptr& aut_;
std::map<unsigned, int> state_to_var;
std::map<int, unsigned> var_to_state;
bdd vars_;
public:
outedge_combiner(const twa_graph_ptr& aut);
~outedge_combiner();
bdd operator()(unsigned st);
void new_dests(unsigned st, bdd out) const;
};
/// @{
/// \brief Combine two states in a conjunction.
///
/// This creates a new state whose outgoing transitions are the
/// conjunctions of the compatible transitions of s1 and s2.
///
/// Acceptance marks are dropped.
///
/// The results is very likely to be alternating.
template<class I>
SPOT_API
unsigned states_and(const twa_graph_ptr& aut, I begin, I end)
{
if (begin == end)
throw std::runtime_error
("state_and() expects an non-empty list of states");
outedge_combiner combiner(aut);
bdd combination = bddtrue;
while (begin != end)
combination &= combiner(*begin++);
unsigned new_s = aut->new_state();
combiner.new_dests(new_s, combination);
return new_s;
}
template<class T>
SPOT_API
unsigned states_and(const twa_graph_ptr& aut,
const std::initializer_list<T>& il)
{
return states_and(aut, il.begin(), il.end());
}
/// @}
}
......@@ -94,3 +94,41 @@ State: 1
State: 2
[0 | 1] 2
--END--"""
st = spot.states_and(aut, [0, 2])
st2 = spot.states_and(aut, [1, st])
st3 = spot.states_and(aut, [0, 1, 2])
assert (st, st2, st3) == (3, 4, 5)
received = False
try:
st4 = spot.states_and(aut, [])
except RuntimeError:
received = True
assert received
h = 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&2 {0}
[1] 0&1
State: 1
[0&1] 0&2&1
State: 2
[0 | 1] 2
State: 3
[0] 1&2
[1] 0&1&2
State: 4
[0&1] 0&1&2
State: 5
[0&1] 0&1&2
--END--"""
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