lps2lts uses too much memory when generating a state space in .lts format

[wiegerw]

When generating a state space for a non probabilistic LPS, the memory consumption of lps2lts varies a lot depending on the chosen output format. For an .lts file roughly 3 times more memory is needed than for an .aut file. This causes real problems, for example in the OPZuid project.

As far as I can tell, the only reason for this difference is that probabilistic states have a much higher memory footprint than non probabilistic states. It seems unreasonable that a user of a non probabilistic LPS needs to pay for this overhead.

So I propose that the old functionality using non probabilistic states is restored.

[jgroote]

States in .lts format for non probabilistic transition systems are not stored as probabilistic transitions, although this has been the case. Also, saving the transitions does not touch anything related to probabilistic states. It is the case that the .aut format is far more efficient than the .lts format because in the .aut format transitions are written to disk immediately and not stored in memory. Also the transformation to .lts format by transforming the statespace to an aterm takes quite some memory. However, this is a substantial improvement in both speed and memory compared to the .svc format used previously. Changing the .lts format is a major undertaking. In case efficient memory use is required one should use the .aut format.

[wiegerw]

I am truly shocked by this premature closure of this ticket. Do you sincerely believe that this enormous overhead for .lts generation cannot be avoided?

[tneele]

I would suggest to reopen this ticket and label it as 'long term'. I agree with Wieger that using .lts as output format requires a lot of memory. I don't agree that this is solely due to the way probabilistic states are stored.

In the current framework where LTSs are stored as ATerms, it is not clear how to reduce the memory usage of lps2lts further when using .lts as the output format. Streaming transitions to disk (as done for .aut files) would be very nice, but the current binary aterm format does not support that. In my opinion, this can only be addressed properly if we make significant changes to the binary aterm format.

[wiegerw]

I just compared lps2lts right before the addition of probabilistic extensions with the current version. On my case study I measure an increase of 80% in memory usage for the generation of an .lts file. Anyway, the decision that it can never be significant enough to repair this has already been made by Jan Friso, so I will no longer bother people with it.

[jgroote]

I think that the last comment is reason to reopen this issue, to investigate why such a dramatic increase in memory is observed. I cannot believe that this is due to the use of probabilities as by far the most memory is used in the generation of the .lts file, and here no probabilistic information is stored. But if the reported figures of an 80% increase in memory usage are right for the generation of a .lts format, before the introduction of probabilities and the current situation this requires further investigation.

[mlaveaux]

We have made various improvements to the saving of .lts files that at this point it is difficult to compare it to the old versions.