Michael Jones, PhD

"The philosophy behind the collapsing scheme is that although many states can be visited by a program the underlying components of many of these states will be the same." (page 4, second column). An example is given for collapsing the rest of a state except the stack frame for a method invocation due to a local variable update.

In our context, the problem is where to draw the boundaries for the "components" in our memory structure.





So I've got just the data segment, code segment and stack collapsed in my little drawing above. The JPF apparently uses components of the program itself. So we'd get into the call stack, variable locations etc and collapse to a finer level of detail. I doesn't make sense to store the ROM, since its, well, read only. I doesn't make sense to collapse the register set or the program counter or the stack pointer. Since they change so often. But it might make sense to collapse the register set. I think empty memory can be collapsed too. Our components are going to be defined at the OS level. So that means we'll know where the data and code segments are, but we won't see into the structure of either of those segments.

See also "State Compression in Spin" by G. Holzmann in SPIN 1997