Part 1. of Álvaro's suggestions is currently being implemented as issue561.
(Sorry for messing up the issue numbers! This kind of happened accidentally...)

Part 2. is more speculative at the moment, and I don't think we should worry
about it until our current round of M&S refactoring is done. I'm therefore
marking this one as resolved, but feel free to bring this up at a later time
when the code has stabilized again.

I thought a bit more about this, and another problem came to my mind with the
suggested separation: as we currently keep the lts/abstraction in a valid state
after every external operation, the new abstraction class would need to
synchronize on the distances computation, i.e. compute distances whenever
required (which can happen after shrinking but also after discarding
unreachable/irrelevant states, triggered through distances computation).
Otherwise, the merge-and-shrink construction process would need to manually
decide when to compute distances, as it was done earlier, and we really want to
avoid this, because the lts/abstraction relies on computed distances for several
purposes such as computing DFP label ranks and computing bisimulations.

I'll take this one off my list -- if anyone else has a good idea how to
implement the changes suggested by Álvaro (and they definitely make sense),
please feel free to tackle this issue.

Thank your for this precise description! I understand that using a
more generic labeled transisition system class would be nice, but on
the other hand, I think that the current implementation still is
somewhat more specific to merge-and-shrink than one might think: we
don't have transitions_by_label anymore, but we store transitions
according to their "label group", which is a set of labels. The
reason is to only represent transitions of equivalent labels only
once. Additionally, we also require operations like applying an
abstraction and constructing an LTS from two given LTS, which I find
rather "ungeneral", and hence which I think is something which
should not necessarily be part of a generic LTS class.

This means that the first step you suggested would probably only
result in having two different classes in the merge-and-shrink
framework (which is already a small improvement, considering the
size of the current single class), but not a generic LTS class which
would also be used by other parts of the code. The second step,
introducing an abstract LTS class from which an MS-LTS class would
inherit, seems to be the cleaner approach, but also a large
refactoring step, which I am not sure that I want to undertake right
now.

I actually considered to make the MS-LTS even less LTS-like by
refactoring it further, introducing a class (or a struct)
"LabelGroupTransitions" that contains a set of labels, its
transitions (or a pointer to its transitions which are stored
somewhere else compactly) and its cost (and possibly more
information if useful). The notion of a graph would then hardly
exist anymore. This does not contradict refactoring according to
step 1, of course.

Hi, 

The main reason to separate M&S abstractions and labeled transition systems is 
to be more generic with respect to the representation of the LTS. Thus, the 
purpose of the class LTS should be only to represent a graph. Thus, the 
distances should still be stored in the M&S abstraction (though the algorithms 
implementing compute_distances should receive as input an LTS). 

The advantages of the separation are: 
(1) Graphs representation/algorithms are a good tool for the FD toolbox. For 
example, in different contexts strongly connected components have to be 
computed on the causal graph or on M&S abstractions. Using a generic graph/LTS 
class is good for reusing the same algorithms.  

(2) The most important part is to be flexible in the representation of LTSs. 
Right now, they're represented with the transitions_by_label list. This is a 
good representation for the merge and apply_abstraction operations, which are 
arguably central to the M&S algorithm. However, other algorithms may benefit 
from other representations. For compute_distances, the transitions are 
organized by source state in order to implement Dijkstra search. Bisimulation 
shrinking could also benefit from a similar data-structure so it might be worth 
it to reuse it from compute_distances to bisimulation.
As another example, in order to optimize time in some algorithms, I replicate 
transitions_by_label into transitions_by_src and transitions_by_target, or even 
transitions_by_src_and_label. 

I argue that, as more algorithms are introduced in M&S, it will become less and 
less clear which representation is best. Moreover, the best representation 
might vary depending on the characteristics of the domain or even the 
particular abstractions (e.g., using a different representation for small or 
large abstractions). Thus, a desing with different implementations of the LTS 
will help to use the better representation for each case.

Of course, there is also some risk of trying to do something too generic, at 
cost of performance or clarity in the code. Therefore, I summarize my 
suggestion in two steps. The first one should be very simple and it could be 
implemented right now:
 - Separate transitions_by_label into an LTS class. The M&S abstraction will 
have the lookup table, the distances and a (shared) pointer to its LTS.

The second one involves more tradeoffs and we might want to think whether we 
really want to do it:
 - Consider an interface for LTS that is valid for compute_distances, 
bisimulation, strongly connected components, etc. Make LTS an abstract class.
Of course, the extra level of indirection of an abstract class can damage 
performance, especially if one call is performed for every transition.

One solution could be to use iterators over the transitions, in a similar way 
to boost::graph. 

In my code I considered methods like applySrcLabel(int label, int src, 
std::function<bool(const LTSTransition & tr)> && f), which apply a given 
function to each transition from src labeled with l. This solution worked well 
for my algorithms, though the use of lambda functions decreased clarity of the 
code.

This is part of meta issue432.

We want to separate the code from TransitionSystem into two classes representing
abstractions and transition systems. It should then be possible to throw away
merge-and-shrink transition systems after the corresponding abstraction has been
merged. Transition systems could also be used for any other purpose than
merge-and-shrink.