State compression in Spot

From LRDE

Revision as of 17:07, 29 January 2019 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

To represent a system by an automaton, we have to save the values of all variables of this system in each state. This can take a lot of memory when there is a lot of variables and/or a lot of states, and also can grow the execution time due to cache misses. To avoid this problem in Spot, we compress the array of variables of each state, which already reduces the memory consumption and the execution time. In this report, we present a datastructure for a better compression of variables in states, using the redundancy of the values in each states of the automatonand the different constraints encounter to add it in Spot.