Commit fba4bdeb authored by Etienne Renault's avatar Etienne Renault

convert: twacube to twa translation

* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/core/twacube.test: here.
parent 5497f23a
......@@ -130,4 +130,54 @@ namespace spot
}
return aps;
}
spot::twa_graph_ptr
twacube_to_twa(spot::twacube* twacube)
{
// Grab necessary variables
auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset();
// Build the resulting graph
auto d = spot::make_bdd_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 (auto& ap : twacube->get_ap())
bdds_ref.push_back(res->register_ap(ap));
// 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());
return res;
}
}
......@@ -50,4 +50,8 @@ namespace spot
twa_to_twacube(spot::twa_graph_ptr& aut,
std::unordered_map<int, int>& ap_binder,
std::vector<std::string>& aps);
/// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube* twacube);
}
......@@ -68,6 +68,7 @@ int main()
<< std::endl;
}
spot::print_dot(std::cout, spot::twacube_to_twa(aut));
delete aps;
delete aut;
}
......@@ -66,6 +66,24 @@ init : 0
2 0 p1 {0,1}
2 1 p1&p2 {}
2 0 !p1&p2 {0,1}
digraph G {
rankdir=LR
node [shape="circle"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="!p1 & !p2"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="!p1 & p2\n{0,1}"]
2 -> 0 [label="p1\n{0,1}"]
2 -> 1 [label="!p1"]
2 -> 1 [label="p1 & p2"]
2 -> 2 [label="1\n{0,1}"]
}
EOF
diff stdout expected
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