In the current Spin implementation the branch Issue374, the generated Promela
is not as efficient as it could be. Currently, it is tracking every event.
However, it is possible to eliminate most of the tracking statements as the
only events that should be tracked are those that have to do with the invariant
being checked.
https://docs.google.com/spreadsheets/d/1dsUA3j4kNt3dBwzxSPQksmFKpl-DoJL-zzSXjfuH
tu8
The data here shows that it is possible to achieve up to a 60% reduction in
memory usage and up to a 72% decrease in execution time.
Original issue reported on code.google.com by Kenneth....@gmail.com on 4 Jul 2014 at 3:30
Original issue reported on code.google.com by
Kenneth....@gmail.com
on 4 Jul 2014 at 3:30