[Javapathfinder-user] How to store variables related with previous scenarios

[zuo j. <zu...@pk...>]

Hello, I encounter a problem with using jpf and have to request for help.

  My program has a test driver class User that models a user who generates
mails in different scenarios. This is achieved by non-deterministically
setting the receiver field.

 

  class User {

         ...

         public void writeMail() {

                   Message msg = Message.create();

                   ...

                   receiver = pickAddress();

                   msg.setReceiver(receiver);

                   agent.messageGenerated(msg);

         }

} 

  

  As the scenarios are too many, I need to make reductions before processing
the newly generated message by analyzing if it is equivalent with some
message that has been generated and processed before. If the newly generated
message has equivalent peers it will be omitted. 

  To do so, the previously generated messages need to be stored. But I
noticed that when jpf backtracks and generates a new message, the fields of
all objects will be restored to their original states. Thus, all the
previously generated messages cannot be stored.

  I wanted to use SearchListener and VMListener. After I looking at their
source files I found that they do not provide the values of the variables of
complex types. How can I store and access the variables that are related
with the previous scenario?

  Thanks in advance!

 

J. H. Zuo