Title M&S refactoring part 2:TransitionSystem: one-shot constructor, refactoring of TSConstIterator, less coupling with LabelEquivalenceRelation
Priority wish Status resolved
Superseder Nosy List malte, silvan
Assigned To silvan Keywords
Optional summary

Created on 2015-12-07.14:30:13 by silvan, last changed by silvan.

msg4985 (view) Author: silvan Date: 2015-12-19.11:33:01
After discovering a bug (thanks windows buildbot!) in the application of label
reduction to label equivalence relation that would try to remove a label from a
group it wasn't part of, I ran another experiment comparing to the version
before this issues. Fortunately, nothing changed:

I guess that gcc willingly removes an element from a doubly linked list even
from the "wrong" group, because the removing operation actually does not have to
look at the group and only has to update the pointers of the neighbouring
elements. The Visual Studio compiler failed however.
msg4979 (view) Author: silvan Date: 2015-12-14.10:21:11
That change was already included. Merged and pushed.
msg4974 (view) Author: malte Date: 2015-12-12.19:59:16
If the change to use caches within the heuristics (done by Salomé a while back)
is already integrated in your branch, then I don't think it's necessary.
Everything else shouldn't change where and how many times heuristic values are
computed. But of course feel free to run experiments if you prefer.
msg4972 (view) Author: silvan Date: 2015-12-12.19:02:02
Summarizing comparison (baseline vs v7):

Performance increases for f-preserving shrinking configurations, and decreases
for bisimulation shrinking configurations. Considering that the code got much
cleaner (thanks for the feedback!), I think this can be merged.

However, there have been *lots* of changes in the default branch; should I
re-run experiments after merging the latest version?
msg4971 (view) Author: silvan Date: 2015-12-12.18:56:25

All together, this doesn't look that bad. (Although I still don't understand why
there is so much change at all.)
msg4965 (view) Author: silvan Date: 2015-12-11.16:38:01
In version 7, I changed the recomputation of label group costs in
LabelEquivalenceRelation to only recompute the cost of affected groups. To do
so, the method takes an unordered_set<int> pointer from TransitionSystem, which
computes this information anyway. Surprisingly for me, this does not have a
purely positive impact on performance. However, it is unclear to say that memory
or time increases or decreases, because it is different for different

I'll also run the remaining configurations of the regular ones.
msg4955 (view) Author: malte Date: 2015-12-11.11:32:00
Very nice.
msg4954 (view) Author: silvan Date: 2015-12-11.10:36:26
And especially after seeing the results in version 6, where I basically changed
one line, namely to reserve memory for the new transitions when applying an
abstraction to a transition system
(new_transitions.reserve(old_transition.size())). Even if this is usually too
much, it apparently is a lot better than risking several resizes.
msg4947 (view) Author: malte Date: 2015-12-10.17:09:16
I think we can live with it, especially as coverage still looks good.
msg4946 (view) Author: silvan Date: 2015-12-10.16:27:27
In version 5, as discussed, we store a vector<Transitions> for later moving
instead of a set. This attenuates the increase of memory consumption compared to
the last version, but in comparison with version 3, there is still a notable
difference. For some configurations, the average memory score goes down by up to
0.75. Should we live with that?
msg4931 (view) Author: silvan Date: 2015-12-10.09:45:22
Version 4 changed the order of the method
TransitionSystem::apply_label_reduction as we discussed, but unfortunately, the
memory consumption increases a lot.

I think that precomputing the transitions and keeping them around (and we still
need to the keep the old group ids in parallel) for *all* label reductions,
before assigning them to their new position, is too expensive.
(The changeset is here:
msg4929 (view) Author: silvan Date: 2015-12-09.21:52:59
Results for version 3, which fixes the slow version 2, are fine (comparison
against v1):
msg4920 (view) Author: silvan Date: 2015-12-09.14:49:07
Following our discussion from the train this morning, I separated the single
loop into several pieces: unfortunately, it now requires 4 iterations over the
label mapping or its derived information to incorporate the label mapping:
1) collect the group ids which are affected for every "single" label reduction
2) update label equivalence relation: remove all labels from their group(s), add
a new group for the new label
3) compute the transitions for all new labels (more precisely, all new label
groups), and remember all label groups that became empty -- we cannot remove
their transitions yet however, as we still may need them for other label reductions
4) remove all transitions of label groups that became empty

The method in TransitionSystem did not become shorter, but at least the
interface of LabelEquivalenceRelation became smaller. I am still not sure
whether this change is really an improvement. It is small and has a nice
side-by-side diff. Maybe you could have a look at it?
msg4915 (view) Author: silvan Date: 2015-12-09.12:16:36
Version 2 includes some refactoring and documentation of TransitionSystem. Most
importantly, the class TSConstIterator now has a more typical iterator class
interface, with a *-operator that returns a simple class that wraps the label
group and its transitions. To avoid also having a non-const iterator,
TransitionSystems internally directly iterates over the group ids (only in once
place, namely computation of locally equivalent labels). In the second version,
this was done without skipping empty label groups, and hence caused a huge overhead.

Version 3 fixes this, but results aren't ready yet.
msg4892 (view) Author: silvan Date: 2015-12-08.10:48:16
In version 1, the three constructors of TransitionSystem have been replaced by a
single one-shot constructor, that moves in all necessary data, either provided
by the FTSFactory (atomic transition systems) or a new static merge method in

There seems to be slight a increase in memory consumption, which I cannot
explain. The diff is somewhat small, maybe it is worth to have a look at it.
msg4885 (view) Author: silvan Date: 2015-12-07.14:30:13
This is part of meta issue567. 

We want to tackle item O.):
  - We currently have a two-stage initialization for the atomic
    transition systems. First, they are created in an incomplete state,
    and then the factory takes over the rest of the initialization. We
    should have a constructor that generates them in one shot.

More precisely, atomic transition systems are currently partly created by
FTSFactory, and party in an "atomic transition system" constructor. The goal is
to get rid of the three different constructors in TransitionSystem, and to have
only one constructor which moves in *all* data which make up a transition
system. This also requires the merge constructor to be moved to a separate
function, which will probably be used from FactoredTransitionSystem.
Date User Action Args
2015-12-19 11:33:01silvansetmessages: + msg4985
2015-12-14 10:21:15silvansetstatus: chatting -> resolved
2015-12-14 10:21:11silvansetmessages: + msg4979
2015-12-12 19:59:16maltesetmessages: + msg4974
2015-12-12 19:02:02silvansetmessages: + msg4972
2015-12-12 18:56:25silvansetmessages: + msg4971
2015-12-11 16:38:01silvansetmessages: + msg4965
2015-12-11 11:32:00maltesetmessages: + msg4955
2015-12-11 10:36:26silvansetmessages: + msg4954
2015-12-10 17:09:16maltesetmessages: + msg4947
2015-12-10 16:27:27silvansetmessages: + msg4946
2015-12-10 09:45:22silvansetmessages: + msg4931
2015-12-09 21:52:59silvansetmessages: + msg4929
2015-12-09 16:26:06silvansetnosy: - jendrik
2015-12-09 16:24:25silvansetnosy: + jendrik
2015-12-09 14:49:07silvansetmessages: + msg4920
2015-12-09 12:16:36silvansetmessages: + msg4915
2015-12-08 15:10:14silvansettitle: M&S refactoring part 2:TransitionSystem should have only one constructor -> M&S refactoring part 2:TransitionSystem: one-shot constructor, refactoring of TSConstIterator, less coupling with LabelEquivalenceRelation
2015-12-08 10:48:16silvansetmessages: + msg4892
2015-12-07 14:30:13silvancreate