Commit 1541eee7 authored by Etienne Renault's avatar Etienne Renault

twacube_algos: add support for are_equivalent

* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/twacube.cc: Here.
parent 2ddb742c
......@@ -19,6 +19,7 @@
#include "config.h"
#include <spot/twacube_algos/convert.hh>
#include <spot/twaalgos/contains.hh>
#include <assert.h>
namespace spot
......@@ -187,4 +188,76 @@ namespace spot
return res;
}
// FIXME this code is very close to twacube_to_twa, can we merge both?
bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa)
{
// Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps_twa = extract_aps(twa, ap_binder);
std::vector<std::string> aps_twacube = twacube->ap();
// Comparator to compare two strings in case insensitive manner
std::function< bool (const std::string&, const std::string&) >
comparator = [](const std::string& lhs, const std::string& rhs){
return lhs.compare(rhs) == 0;
};
// Error. Not working on the same set of aps.
if (aps_twa->size() != aps_twacube.size() ||
!std::equal(aps_twa->begin(), aps_twa->end(),
aps_twacube.begin(), comparator))
throw std::runtime_error("are_equivalent: not working on the same "
"atomic propositions");
// Grab necessary variables
auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset();
auto d = twa->get_dict();
auto res = make_twa_graph(d);
// Fix the acceptance of the resulting automaton
res->acc() = twacube->acc();
// Grep bdd id for each atomic propositions
std::vector<int> bdds_ref;
for (unsigned i = 0; i < aps_twacube.size(); ++i)
{
bdds_ref.push_back(ap_binder[i]);
}
// Build all resulting states
for (unsigned int i = 0; i < theg.num_states(); ++i)
{
unsigned st = res->new_state();
(void) st;
assert(st == i);
}
// Build all resulting conditions.
for (unsigned int i = 1; i <= theg.num_edges(); ++i)
{
bdd cond = bddtrue;
for (unsigned j = 0; j < cs.size(); ++j)
{
if (cs.is_true_var(theg.edge_data(i).cube_, j))
cond &= bdd_ithvar(bdds_ref[j]);
else if (cs.is_false_var(theg.edge_data(i).cube_, j))
cond &= bdd_nithvar(bdds_ref[j]);
// otherwise it 's a free variable do nothing
}
res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
cond, theg.edge_data(i).acc_);
}
// Fix the initial state
res->set_init_state(twacube->get_initial());
bool result = are_equivalent(res, twa);
delete aps_twa;
return result;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement de
// Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -53,4 +53,8 @@ namespace spot
/// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube);
/// \brief Check wether a twacube and a twa are equivalent
SPOT_API bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa);
}
......@@ -49,6 +49,8 @@ int main()
// Test translation
auto aut = twa_to_twacube(tg);
assert(spot::are_equivalent(aut, tg));
spot::print_dot(std::cout, tg, "A");
std::cout << "-----------\n" << *aut << "-----------\n";
......
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