Issue441

Title M&S: Integrate unsat shrinking strategies
Priority wish Status resolved
Superseder Nosy List atorralba, malte, silvan
Assigned To atorralba Keywords
Optional summary

Created on 2014-07-17.16:14:09 by atorralba, last changed by silvan.

Messages
msg10191 (view) Author: silvan Date: 2021-03-18.14:25:05
In today's meeting, we were looking for issues where nothing happened in a long time and which we would therefore like to triage. In this case, we are not opposed in general to integrate more shrink strategies (I actually would find this interesting), but since we don't see anyone working on this in the near future, we decided to close this issue for now. Feel free to re-open or re-create the issue if you have plans to open a pull request for the actual integration.
msg3229 (view) Author: atorralba Date: 2014-07-24.11:37:35
Great, I will use the same approach for the moment, applying normalize and 
compute_distances between shrinking strategies in shrink_composite.

On the other hand, we have observed that apply_abstraction is always called even 
when no shrinking is applied at all. We added a line at the beginning of Abstraction::apply_abstraction to avoid unnecessary computation:
if(size() == collapsed_groups.size()) return;
msg3217 (view) Author: silvan Date: 2014-07-23.11:37:57
Sorry for the late reply. 

I have issued the same difficulties with the current project I work on, and I
found the "solution" of calling normalize from outside whenever I required
normalized abstractions (same for computation of distances). This is, as Malte
said, of course something we want to avoid, and it is indeed on the refactoring
list.

As for "when will we implement" this, the clear answer is: at earliest after the
AAAI deadline in September, so quite some time to go... 

I don't know how we should handle this, because it might indeed take some time
and experimentation to verify that this presumably simple patch does not affect
performance.
msg3212 (view) Author: malte Date: 2014-07-21.18:25:36
The current strategy of when to normalize is somewhat unclear. The original
behaviour was to call as rarely as possible to save time, but at that time
shrink strategies didn't require normalization, which has of course changed now.

> Do you think is best to always call normalize after applying an
> abstraction or whenever we require the abstraction to be
> normalized (before bisimulation shrinking or label reduction, for
> example)?

I think it would be best to have normalization as an implementation detail of
the abstraction class, so that it could be a private method and from an outside
point of view, the abstraction always looks normalized when any of its public
methods are accessed. But we have to make sure there is no serious speed penalty
for this because we generally don't like performance regression.

So maybe it's best to do this integration after addressing this point from our
M&S refactoring list, but I cannot say at which point we will get to this.
Silvan, do you have any thoughts on this?
msg3211 (view) Author: atorralba Date: 2014-07-21.18:16:49
Hi, 
I implemented shrink_composite as you said, thanks for the advice. 

However, I found a problem with the overall organization of M&S abstractions. I 
run own-label shrinking and then bisimulation, but I get a suboptimal heuristic. 
I think that the problem is in that shrink_bisimulation requires the abstraction 
to be normalized and it is not normalized after performing own-label shrinking.

Why abstraction->normalize() is called from merge_and_shrink_heuristic? 

I think this is related to one of the items in Silvan M&S refactoring: to keep 
the transition systems in a valid state.
Do you think is best to always call normalize after applying an abstraction or 
whenever we require the abstraction to be normalized (before bisimulation 
shrinking or label reduction, for example)?
msg3209 (view) Author: malte Date: 2014-07-17.16:23:23
> One important point that may affect the overall M&S organization is that
> own-label shrinking is used with bisimulation so M&S should take a list of
> shrink strategies instead of only one.

In general, we try to use the composite pattern for things like this to keep the
basic interface simple and general. Conceptually, a sequence of shrinks can be
seen as one shrink.

For example, if you do stuff like

--shrink_strategy s1=foo()
--shrink_strategy s2=bar()
--shrink_strategy s=shrink_composite([foo, bar])

then the basic M&S heuristic would not need to be changed; we just use "s" as
the shrink_strategy. (We would need to add a --shrink_strategy option if we
don't have it yet, but in general we should have this kind of option for every
kind of object anyway.)

Advantages of doing things this way:
- heuristic doesn't need to be changed and keeps simple interface
- allows all other kinds of "decorations", too (e.g. wrapping extra debugging
around a shrink strategy)

Disadvantages:
- more verbose command-line syntax
msg3208 (view) Author: atorralba Date: 2014-07-17.16:14:09
Issue created to merge new shrinking strategies: own-label shrinking and label-
inheritance.

One important point that may affect the overall M&S organization is that own-
label shrinking is used with bisimulation so M&S should take a list of  shrink 
strategies instead of only one.
History
Date User Action Args
2021-03-18 14:25:05silvansetstatus: chatting -> resolved
messages: + msg10191
2014-07-24 11:37:35atorralbasetmessages: + msg3229
2014-07-23 11:37:57silvansetmessages: + msg3217
2014-07-21 18:25:36maltesetmessages: + msg3212
2014-07-21 18:16:50atorralbasetmessages: + msg3211
2014-07-17 17:39:49silvansetnosy: + silvan
2014-07-17 16:23:23maltesetnosy: + malte
messages: + msg3209
2014-07-17 16:14:09atorralbacreate