9 Mar
2017
9 Mar
'17
4:17 p.m.
hi,
Is there a way to get more than one accepting run of the product automaton?
Ideally would be to have all simple accepting runs,
but some cheap heuristics would also do.
I wanted to implement some heuristics [1], but got stuck with the following:
how to map edges of the accepting run to the edges of the original product?
(or: states of the accepting run to states of the product?)
thanks!:)
ayrat
[1]
An heuristics:
- get an accepting run,
- forbid one edge of that run in the original product (for example, by
setting its label to bddfalse),
- ask for another accepting run on the thus modified product,
- restore that edge and change another edge,
and so on.
9 Mar
9 Mar
6:58 p.m.
Hi Ayrat,
On Thu, Mar 9, 2017 at 4:17 PM, Ayrat Khalimov <ayrat.khalimov(a)gmail.com> wrote:
Is there a way to get more than one accepting run of
the product automaton?
Ideally would be to have all simple accepting runs,
but some cheap heuristics would also do.
Some of the NDFS-based emptiness checks (like SE05) support having their
check() method called several times and they will restart from where
they stopped, possibly returning more accepting runs. But I'm not sure we
even have a test for this.
I'll try to see if I can demonstrate this in Python and get back to you.
how to map edges of the accepting run to the edges of
the original product?
Do you mean this:
prod = spot.product(left, right)
run = prod.accepting_run(prod)
left_run = run.project(left)
or equivalently:
left_run = left.intersecting_run(right)
?
Reading you again, I'm not sure if the question is about a product or
any automaton. Anyway to map a edge from a run to its automaton,
you'd have to enumerate all the edges that leave the source of the said
edge, and locate one that have the same label, acceptance mark, and
destination (you might have to check label implication instead of equality
if the run has been projected as above).
PS: also I think currently none of the emptiness checks look at the label
of edges they assume that all labels are different from bddfalse. This might
be a flaw. Or we should at least document it. If you are altering
left or right
in a product, this is OK, because product() will not create bddfalse
transitions,
but if you are running the emptiness check directly on an automaton with
bddfalse-labeled transition, that will fail (I think).
--
Alexandre Duret-Lutz
10 Mar
10 Mar
10:45 a.m.
On Thu, Mar 9, 2017 at 6:58 PM, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
Some of the NDFS-based emptiness checks (like SE05)
support having their
check() method called several times and they will restart from where
they stopped, possibly returning more accepting runs. But I'm not sure we
even have a test for this.
I'll try to see if I can demonstrate this in Python and get back to you.
The following seems to report only non-overlapping cycles:
import spot
aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA')
# Note: SE05 should only be used with Büchi acceptance.
ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut)
while True:
res = ec.check()
if not res:
break
print(res.accepting_run())
--
Alexandre Duret-Lutz
12 Mar
12 Mar
2:59 p.m.
thanks!
I used the enumeration of accepting runs that you suggested. (my tool
didn't perform as better as i hoped, but that is my task:)
> Do you mean this:
> prod = spot.product(left, right)
> run = prod.accepting_run(prod)
> left_run = run.project(left)
> Anyway to map a edge from a run to its automaton,
> you'd have to enumerate all the edges that leave the source of the said
> edge, and locate one that have the same label, acceptance mark, and
> destination (you might have to check label implication instead
you nailed it! I enumerated the edges of the original automaton and
compared the edges
as you suggested. That worked!
thanks for your help,
Ayrat
On Fri, Mar 10, 2017 at 10:45 AM, Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
On Thu, Mar 9, 2017 at 6:58 PM, Alexandre Duret-Lutz
<adl(a)lrde.epita.fr>
wrote:
Some of the NDFS-based emptiness checks (like
SE05) support having their
check() method called several times and they will restart from where
they stopped, possibly returning more accepting runs. But I'm not sure
we
even have a test for this.
I'll try to see if I can demonstrate this in Python and get back to you.
The following seems to report only non-overlapping cycles:
import spot
aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA')
# Note: SE05 should only be used with Büchi acceptance.
ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut)
while True:
res = ec.check()
if not res:
break
print(res.accepting_run())
--
Alexandre Duret-Lutz
2887
days inactive
2890
days old
3 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Ayrat Khalimov