Thanks for the comments. I'd like to consolidate the default branch and the paper 
CEGAR branch before making more structural changes, but then we should definitely 
discuss a better code structure.

The issue branch at hand has been merged and pushed.

I looked into the code and have added some minor comments. However, we also had
a discussion on the general structure of the code and agreed that some classes
should be restructured. In particular, we should aim for a structure with:

1. A datastructure class, e.g. CartesianAbstractionSystem, that serves as the
sole interface to the rest of the cegar code
2. A class that implements CEGAR, especially the refinment loop
3. A class that implements the additive CEGAR stuff, especially everything
regarding the SCP computation

Jendrik, we can further talk this through if you are interested and open a new
issue for what we agree on. From my point of view, this issue can be closed then.

Here are some relative scatter plots comparing the total_time for the landmarks and goals abstractions:

base vs v2: http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-base-vs-v2.png
v2 vs v3: http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-v3-issue657-v2-issue657-v3-total_time-cegar-landmarks-goals-max_transitions=1000000.png
v3 vs v4: http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-v4-issue657-v3-issue657-v4-total_time-cegar-landmarks-goals-max_transitions=1000000.png

Only the second comparison has a significant trend in any direction. It shows that caching the pre- and postconditions speeds up the abstraction 
computation.

The experiment comparing v3 to v4 shows no significant changes:

http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-v4-issue657-v3-issue657-v4-compare.html

I meant to say "comparing v2 to v3" in the last message.

The experiment comparing v3 to v4 shows that we use a bit more memory (as expected for 
storing the pre- and postconditions), but reduce the time for building abstractions in many 
domains (higher score_total_time):

http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-v3-issue657-v2-issue657-v3-compare.html

I have merged the current default branch into the issue branch and ran some 
experiments. There seem to be no changes regarding runtime and coverage:

http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-v2.html

The difference between v2 and v2-base (on default) is that the new 
TransitionUpdater class rewires the transitions, instead of the AbstractStates 
themselves.

I also implemented v3 and v4. 

v3 caches the operator pre- and postconditions in TransitionUpdater to avoid 
accessing the task interface too often. This speeds up the abstraction 
construction by a factor of 3 on a locally tested example task.

v4 stores *sorted* pre- and postconditions to allow aborting the search for pre- 
and postconditions early.

Experiments comparing v2 to v3 and v3 to v4 are running.

Thomas, could you have a look at the code, please?

https://bitbucket.org/jendrikseipp/downward/pull-requests/51

I don't mind waiting. It would be great if you could have a look.

If you don't mind waiting, I can have a look at this (however, if my
one-day-a-week stays as busy as today, it'll probably take a while until I
manage to find the time for a review).

OK, I'll run experiments and will probably merge the code without review if the 
results look good.

Anybody else up for a review?

That's more than I can review. You'll have to find someone else. :-)

OK, good thing I asked before implementing it :-) Malte, could you have a look at 
the pull request, please?

https://bitbucket.org/jendrikseipp/downward/pull-requests/51

Doesn't sound good to me. Replacing an attribute access by a hash lookup is too
expensive for something that is potentially needed frequently.

I'm done implementing the TransitionSystem class as we discussed. It doesn't 
hold the transitions; they are still stored in AbstractState. This makes for a 
cumbersome interface though, I think. Now both TransitionSystem and 
AbstractState have methods for adding and removing transitions and the ones of 
AbstractState should only be called by TransitionSystem. Therefore, it probably 
makes sense to move the transitions into TransitionSystem after all. They could 
be stored in a unordered_maps mapping from states to vectors of incoming and 
outgoing transitions. What do you think about this solution?

re 1): For the option name, I think "transitions" is fine as long as it's
clearly documented. For the code, perhaps "non_looping_transitions" works. Long,
but explicit. It shouldn't show up in a thousand places.

1) We couldn't come up with a good name for non-self-loop transitions. Malte, 
do you have an idea?

2) Notes from our offline discussion: We agreed to add a TransitionSystem class 
that operates on the existing data structures and stores the number of 
transitions.

1) I agree, renaming these things makes sense.

2) Discussing this in person is a good idea.

Two comments:

1) "transition" and "arc" are the same thing, so please don't use the
distinction between these two words to distinguish general transitions and
transitions that are not self-loops. "Arc" is the usual word for the directed
edges of directed graphs, which can be self-loops. I suggest we use "transition"
everywhere, since this is consistent with other parts of the code.

2) I'm not sure I follow the discussion, but if it's about replacing an O(1)
incremental way of counting transitions with an O(n) non-incremental way, please
let us first check if this is really necessary. If the operation is not
runtime-critical, it just shows that we have other parts of the code that need
optimizing, but that doesn't mean we should introduce a new future bottleneck.
If you want, we can briefly discuss this live on Monday.

I agree with setting max_time=infinity by default and already pushed the change.

Incrementally computing the number of arcs is not so straightforward, I think. Obviously, it 
would be possible to count the number of removed and added arcs during the refinement. This, 
however, happens in AbstractState and we need the number of arcs in Abstraction. If we can 
only query the split state v and the resulting two new states v1 and v2 for the number of 
incoming arcs, outgoing arcs and self-loops, dynamically computing the number of arcs is not 
possible, I believe. If we were to use the formula (total_arcs_out = total_arcs_in is the 
number we want to limit with max_arcs, i.e. we want to limit the "real" number of arcs and 
ignore that each "real" arc is stored twice in the implementation) 

new_total_arcs_out = old_total_arcs_out + in(v1) + in(v2) - in(v) + out(v1) + out(v2) - 
out(v)

we would count the arcs produced by splitting v's self-loops twice.

Experimentally, I found that indeed computing the number of arcs from scratch doesn't hurt 
the runtime.

Before I look too deep into the code, there is one major code design that I
think might be worth changing: currently, the number of arcs is counted over and
over, instead of storing it in a member variable that is set to 0 for the
trivial abstraction and which is increased accordingly with every split. I am
aware that this is most likely non-critical (at least as long as the
abstractions do not become too big), but it should be fairly simple to update
the value online.

I would set max_time=infinity to ensure deterministic behavior.

I'll take a look at your changes.

The main goal of this issue is to find a replacement parameter for
max_time, that is more deterministic and achieves similar results.
First, I tried limiting the number of transitions (self-loops + real
transitions), but experiments showed that the number of transitions
doesn't correlate with the runtime. This is probably due to the fact
that especially for small abstractions, almost all transitions are
self-loops. They are responsible for the magnitude of the transtions,
but can be ignored during the searches for the next shortest solution.

In the current code version, I'm therefore limiting the number of
"arcs", i.e. real transitions without self-loops. The number of arcs
correlates nicely with the CEGAR preprocessing time, so it seems to be
the parameter that I was looking for.

To evaluate the max_arcs parameter, I have run some experiments. They
show that setting max_arcs to 2 million solves 3 more tasks in total
than even the best configuration that sets the max_time parameter
(max_time=900, the default, has the highest coverage). Comparing
max_arcs=2M to max_time=900 for other attributes shows that max_arcs=2M
needs much less time for the abstraction computation (obviously
reducing max_time would also achieve this, but with a reduction in
coverage), and also much less memory:

http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-max_arcs=2M-init-time-relative.png
http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-max_arcs=2M-total_time-relative.png
http://ai.cs.unibas.ch/_tmp_files/seipp/issue657-max_arcs=2M-init_memory-relative.png

Therefore, I propose to use "cegar(max_time=900, max_arcs=2000000)" as
the new default CEGAR configuration. Leaving max_time=900 in would only
serve as a safeguard for tasks we have not yet seen. We could also set
max_time=infinity (as I'd do for experiments). What do you think?

I have created a pull request at
https://bitbucket.org/jendrikseipp/downward/pull-requests/51. Thomas,
could you have a look, please?

The number of transitions should predict the amount of memory (and maybe time) 
much better than the number of states.