Issue492

Title M&S refactoring: store transitions for locally equivalent labels only once
Priority wish Status resolved
Superseder Nosy List malte, silvan
Assigned To silvan Keywords
Optional summary

Created on 2014-10-17.16:28:58 by silvan, last changed by silvan.

Messages
msg4010 (view) Author: silvan Date: 2015-02-04.11:11:01
This is a very small change, which I just implemented.

Calling this one resolved finally :-)
msg4009 (view) Author: malte Date: 2015-02-03.19:57:49
> Getting rid of the notion of "irrelevant labels" is not possible for
> computation of label ranks (and hence for MergeDFP) without drastic
> performance losses; hence I had to leave this part in.

If it's only needed for one merge strategy, I'd rather have it encapsulated
within this merge strategy, so I'd rather have all relevant code moved there.
This could be a separate issue so that we can merge this one.
msg4008 (view) Author: silvan Date: 2015-02-03.15:55:28
Final results for this issue:

http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-02-issue492-v20-bisim2-rest-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-02-issue492-v20-bisim2-rest-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-02-issue492-v20-bisim2-rest-rl-base-comp.html

I'd be happy to merge this.
msg4007 (view) Author: silvan Date: 2015-02-03.15:53:17
Getting rid of the notion of "irrelevant labels" is not possible for computation
of label ranks (and hence for MergeDFP) without drastic performance losses;
hence I had to leave this part in.

Don't use rank of -1 for irrelevant labels:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-03-issue492-v20-dfp1-dfp-v20-bisim2-comp.html
Additionally don't consider self-loop transitions:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-03-issue492-v20-dfp2-v20-bisim2-comp.html

Final
msg4006 (view) Author: silvan Date: 2015-02-03.09:14:59
No big performance loss:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-02-issue492-v20-bisim2-comp-v20-bisim1-comp.html
msg4005 (view) Author: silvan Date: 2015-02-02.22:35:15
Next I'll get rid of the notion of "irrelevant labels" for bisimulation - this
should slow things down a little bit and maybe slightly change the behaviour,
but hopefully not too much.
msg4004 (view) Author: silvan Date: 2015-02-02.22:34:27
Updated results (links below); results as expected.

I changed a tiny little bit in the computation of bisimulation: it computes the
signatures only for the label group number rather than for all lables - the
reduction in memory seems huge.

Comparison against previous version (not even to baseline):
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-02-02-issue492-v20-bisim1-bisim-v20-comp.html
msg4003 (view) Author: silvan Date: 2015-02-02.14:30:06
Stop, I need to correct myself. I ran the wrong revision :-( Probably nothing
bad happened at all.
msg4002 (view) Author: silvan Date: 2015-02-02.14:28:25
Those are the links posted in the previous comments.
msg4001 (view) Author: malte Date: 2015-02-02.14:02:02
I checked the diff for issue269 and see no problematic changes. There is no
reason why it should affect merge-and-shrink performance either negatively or
positively; if it does, it should just be bad/good luck.

> However, after merging from default (issue269 with using g_rng has been
> integrated), the baseline for all bisimulation configurations (and sometimes
> also for shrink_fh) raised in coverage

How large is this change? Do we have an experimental report on this somewhere?

I'm fine with merging this if you are.
msg4000 (view) Author: silvan Date: 2015-02-02.12:48:24
After running many more different versions, I now wanted to settle onto a
version which has not the best runtime behaviour compared to v8, but is still
good compared to the baseline and with much cleaner code.

(More details: 
- We do not use the EquivalenceRelation class for storing locally equivalent
labels, but do this directly in TransitionSystem, which increases runtime for no
obvious reason (I re-confirmed this in trying out every specific change for its
own compared to the baseline-v8 version), but it saves memory.
- We do not use the "smallest" label of every label block as a representative,
but an arbitrary index into vector<vector<Transition>>. In particular, when a
new label is introduced and it is equivalent to an existing one, we do not move
any Transitions around. Strangely, this also slightly increases runtime, but
makes the code much simpler.)

However, after merging from default (issue269 with using g_rng has been
integrated), the baseline for all bisimulation configurations (and sometimes
also for shrink_fh) raised in coverage, but so did not the version of this
issue. In issue269, nothing changed for the bisimulation, but only for
shrink_bucket_based, so this behaviour seems odd to me. Maybe due to the change
of the order in which the label reduction considers transition systems and hence
reduces labels, this affects the bisimulation computation. Anyway, the
experiments in issue269 do not report results for the configurations we use
here, so it's hard to see what happens.

Here are the results:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-01-31-issue492-v20-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-01-31-issue492-v20-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-01-31-issue492-v20-rl-base-comp.html

Do you think it's worth to investigate the diff that issue269 introduced? Or
should we live with the results we have?
msg3946 (view) Author: malte Date: 2014-12-16.00:17:48
Looks good to me.
msg3945 (view) Author: silvan Date: 2014-12-15.22:22:18
In v8, apply_abstraction() does not compute all transitions anymore, but only
for every block equivalent labels. Equivalent labels cannot become non-locally
equivalent through shrinking and hence the equivalence relation needs only to be
updated if more blocks of labels are equivalent after shrinking.

Results are less accentuated than I would have expected, but still rather positive:
comparison against previous version (v7):
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-cggl-v7-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-dfp-v7-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-rl-v7-comp.html

against baseline:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v8-rl-base-comp.html
msg3933 (view) Author: silvan Date: 2014-12-15.09:26:22
Now that issue500 has been merged, everything is better. We cannot easily
compare to previous versions (vx for x < 7), but only to the new default
versions baseline issue432-v7.

This issue's v7 does not differ from v6 with the exception of issue500 being
merged in. Results now look promising even compared to baseline for the first time:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v7-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v7-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v7-rl-base-comp.html

While I think that this could already be good enough to be closed soon, I still
would like to change the "apply abstraction" method to not recompute all
equivalent labels but to only take into account the changes.
msg3932 (view) Author: silvan Date: 2014-12-15.09:23:18
In v6, we changed the constructor of composite transition systems to compute the
new transitions and locally equivalent labels based on the equivalence relation
of the components:

http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v6-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v6-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-14-issue492-v6-rl-base-comp.html
msg3899 (view) Author: malte Date: 2014-12-04.00:37:05
> I don't think I can continue alone from here on, so as you said in your
> previous comment, it would be nice to discuss further possibilities and maybe
> also to have a look at the code next week.

Sounds good.

The result look better than I feared -- I hope this is something we can work with.
msg3898 (view) Author: silvan Date: 2014-12-03.22:48:31
For version 4, I removed all notion of relevant labels. Unfortunately, this
wasn't as easy as expected, because of several reasons:
- the old version does not recognize "new irrelevant" labels that may arise
after shrinking
- the computation of bisimulation behaves differently if the transitions of
irrelevant labels are present
- the computation of label ranks (for MergeDFP) greatly differs if the
transitions of irrelevant labels are present

For a first version, I hence adapted bisimulation and MergeDFP such that they
compute if a label has the transitions of an irrelevant label according to the
old notion whenever they use transitions of that label. Still, the comparison
cannot expected to be exactly the same in terms of the resulting heuristics
because of the aforementioned possibility of labels becoming irrelevant after
shrinking in the old versions.

Anyway, the results are not at all favoring the inclusion of the transitions of
irrelevant labels (for large transition systems, these are just so many).

Comparison against baseline:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-cggl-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-dfp-base-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-rl-base-comp.html

Comparison against version 3:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-cggl-v3-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-dfp-v3-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-rl-v3-comp.html

And, for completeness:
- bisimulation does not check whether a label would have been irrelevant or not
according to older versions (compared against version 4):
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-bisim-v4-comp.html

- dfp does not check... (same as for bisim):
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-dfp-v4-comp.html

- both bisimulation and dfp do not check...:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-03-issue492-v4-bisim-dfp-v4-comp.html

I think the important results are those comparing v4 against base/v3, and the
memory consumption increases drastically, although for some configurations, the
resulting heuristics, if computed, become better. 

I don't think I can continue alone from here on, so as you said in your previous
comment, it would be nice to discuss further possibilities and maybe also to
have a look at the code next week.
msg3897 (view) Author: silvan Date: 2014-12-03.15:49:57
For the record: results of version 3.
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v3-cggl-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v3-dfp-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v3-rl-comp.html
msg3896 (view) Author: malte Date: 2014-12-01.20:33:16
Thanks! Unfortunately I don't have time to look at the code at the moment (excep
during the upcoming Fast Downward sprint if we want to prioritize this), so I
can only give high-level comments. Let's perhaps discuss this live when we have
the opportunity.

Getting rid of the "relevant labels" optimization would be a very attractive
simplification, and I think this issue could be a good place to try it out -- if
we can afford it at all, then we can afford it when implementing this issue. I'd
be interested in trying it out now, but of course the risk is that we'll have to
undo the change later. You're doing the work, so your choice.
msg3895 (view) Author: silvan Date: 2014-12-01.19:44:10
I conducted several experiments, the latest being a tagged version v2.

The features are the following:
- transitions of locally equivalent labels are only stored once
- we keep a mapping from labels to their representatives
- when applying label reduction, we manually update the equivalence relation and
the mapping
- after shrinking and computing the composite transition system (i.e. the only
places where all transitions have been computed from scratch), we compute the
equivalence relation from scratch.

Results:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v2-cggl-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v2-dfp-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-12-01-issue492-v2-rl-comp.html

I think in order to gain more performance, we would need to get rid of the label
to representative mapping or generally have a tighter coupling of the
transitions to the equivalence relation so we don't need to update and keep them
synchronized. I am not sure how to do this however.

For version 3, I also changed the interface to MergeDFP and ShrinkBisimulation,
both using the equivalence relation to retrieve information about labels rather
than iterating over all labels, possibly looking at the same (equivalent)
transitions several times.

I also think that computing the equivalence relation when constructing the
composite transition system could maybe be done by intersecting the equivalence
relations of both component transition systems. I haven't tried it out yet however.

Last, we wanted to get rid of the relevant and irrelevant labels distinction,
but I wasn't sure if we wanted to test the influence already now or only later.
The code would very probably be "easier" with that change.

I'll create a pull-request on bitbucket so you have a look at code, if you like.
msg3846 (view) Author: silvan Date: 2014-10-17.16:28:57
This is part of meta issue432.

We want to compute the equivalence relation for locally equivalent labels in
every transition system and store transitions only for every equivalence group.
We could possibly even get rid of relevant and irrelevant labels, making
self-loops of irrelevant labels explicit and only storing them once.
History
Date User Action Args
2015-02-04 11:11:01silvansetstatus: chatting -> resolved
messages: + msg4010
2015-02-03 19:57:49maltesetmessages: + msg4009
2015-02-03 15:55:29silvansetmessages: + msg4008
2015-02-03 15:53:17silvansetmessages: + msg4007
2015-02-03 09:14:59silvansetmessages: + msg4006
2015-02-02 22:35:15silvansetmessages: + msg4005
2015-02-02 22:34:27silvansetmessages: + msg4004
2015-02-02 14:30:06silvansetmessages: + msg4003
2015-02-02 14:28:25silvansetmessages: + msg4002
2015-02-02 14:02:02maltesetmessages: + msg4001
2015-02-02 12:48:24silvansetmessages: + msg4000
2014-12-16 00:17:48maltesetmessages: + msg3946
2014-12-15 22:22:18silvansetmessages: + msg3945
2014-12-15 09:26:22silvansetmessages: + msg3933
2014-12-15 09:23:18silvansetmessages: + msg3932
2014-12-04 00:37:05maltesetmessages: + msg3899
2014-12-03 22:48:31silvansetmessages: + msg3898
2014-12-03 15:49:57silvansetmessages: + msg3897
2014-12-01 20:33:16maltesetmessages: + msg3896
2014-12-01 19:44:10silvansetmessages: + msg3895
2014-10-17 16:28:58silvancreate