informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
790 stars 31 forks source link

High memory usage after #1365 #1456

Closed bugarela closed 2 months ago

bugarela commented 3 months ago

My change on https://github.com/informalsystems/quint/pull/1365 made it so memory usage increases a lot during simulation, as we are now storing many traces to select the few best ones latter.

The solution is probably to only store the N best traces, according to how many were requested. Previously, we only stored the single best trace and compared it every time. We can now compare it to the Nth trace, and then only sort the N-best ones when we find a new best one.

(Found by @cason)