...
 
Commits (3)
......@@ -134,14 +134,15 @@ namespace spot
}
spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube)
twacube_to_twa(spot::twacube_ptr twacube, spot::bdd_dict_ptr d)
{
// Grab necessary variables
auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset();
// Build the resulting graph
auto d = spot::make_bdd_dict();
if (d == nullptr)
d = spot::make_bdd_dict();
auto res = make_twa_graph(d);
// Fix the acceptance of the resulting automaton
......@@ -183,7 +184,6 @@ 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)
{
......@@ -205,50 +205,7 @@ namespace spot
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());
auto res = twacube_to_twa(twacube, twa->get_dict());
bool result = are_equivalent(res, twa);
delete aps_twa;
......
......@@ -50,9 +50,12 @@ namespace spot
SPOT_API twacube_ptr
twa_to_twacube(spot::const_twa_graph_ptr aut);
/// \brief Convert a twacube into a twa
/// \brief Convert a twacube into a twa.
/// When \d is specified, the BDD_dict in parameter is used rather than
/// creating a new one.
SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube);
twacube_to_twa(spot::twacube_ptr twacube,
spot::bdd_dict_ptr d = nullptr);
/// \brief Check wether a twacube and a twa are equivalent
SPOT_API bool are_equivalent(const spot::twacube_ptr twacube,
......
......@@ -20,6 +20,10 @@
#include "config.h"
#include <bddx.h>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/contains.hh>
#include <iostream>
#include <spot/twacube/twacube.hh>
#include <spot/twacube_algos/convert.hh>
......@@ -28,6 +32,24 @@
#include <spot/twaalgos/dot.hh>
#include <spot/tl/defaultenv.hh>
static void checkit(std::string f_str)
{
spot::default_environment& env = spot::default_environment::instance();
auto pf = spot::parse_infix_psl(f_str, env, false);
spot::formula f = pf.f;
auto dict = spot::make_bdd_dict();
spot::translator trans(dict);
auto prop = trans.run(&f);
auto propcube = spot::twa_to_twacube(prop);
assert(spot::are_equivalent(propcube, prop));
auto propcubeback = spot::twacube_to_twa(propcube, dict);
assert(spot::are_equivalent(propcube, propcubeback));
assert(spot::are_equivalent(prop, propcubeback));
}
int main()
{
// Build some TWA
......@@ -66,4 +88,11 @@ int main()
<< std::endl;
}
spot::print_dot(std::cout, spot::twacube_to_twa(aut), "A");
// Now check the equivalence of multiple translations
checkit("F!p8 U (((!p11 & p17 & Gp4) | (!p17 & (p11 | F!p4))) R (p4 U p2))");
checkit("F(((p9 & F!p12) | (!p9 & Gp12)) R (G!p7 & ((p16 R p5) M p4)))");
checkit("Gp14 U ((Fp11 W (p13 R p6)) M ((Fp16 & Fp10) | G(!p10 & !p16)))");
checkit("F(((p9 & F!p12) | (!p9 & Gp12)) R (G!p7 & ((p16 R p5) M p4)))");
checkit("Gp14 U ((Fp11 W (p13 R p6)) M ((Fp16 & Fp10) | G(!p10 & !p16)))");
}