6 Dec
2016
6 Dec
'16
3:35 p.m.
Hi Marvin,
Hello dear spot devs,
I have a question concerning stepping through an automaton based on the boolean formula
assigned to the edge between two states, using c++.
What I want to achieve is the following:
I'm translating an LTL formula into a deterministic monitor automaton, so I have a
spot::const_twa_graph_ptr.
Now I simply want to "run" the DFA, i.e., I have a trace and want to perform a
state change based on the transition matching the current letter in my trace.
I don't get that step just from the examples or the doxygen documentation.
maybe something like
unsigned step(const const_twa_graph_ptr& aut, unsigned src, bdd label)
{
for (auto& edge: aut->out(src))
if (bdd_implies(label, edge.cond))
return edge.dst;
throw std::runtime_error("unmatched label");
}
Furthermore it would also be great, if you could tell
me how to output the bdd on the edge in an human readable way (boolean formula), as it is
done in the online tool of yours (https://spot.lrde.epita.fr/trans.html).
I believe this is shown in https://spot.lrde.epita.fr/tut21.html
--
Alexandre Duret-Lutz