K
kvnsmnsn
I'm currently working on a Model Checking application that is extend-
ing the capability of Kansas State University's Bogor model checking
tool. I'm using Eclipse as a software development tool. Eclipse lets
me click on a variable or class name and see where that variable or
class is declared. Bogor is capable of taking a BIR file as an input
and then gives me a <currentState> variable that tells me which state
the program is currently in (starting with the program's initial
state) and a <doTransition()> method that changes <currentState> from
its current value to one of its successor states. So using Bogor on a
given program I can build the state graph that is equivalent to that
program.
My program stores information for a set of FIFO queues each of which
includes a state (of class <IState>), an <int> state id, a <boolean>
accepting value telling me whether this state is an accepting state or
not, and an <int> that identifies the set of accepting predecessors
this state has.
The problem that I have is that these queues have grown so large that
my program has run out of memory. So it has become necessary to write
the contents of a queue to disk when that queue becomes too large. So
naturally I wanted to look at the <IState> class definition to find
out what I would need to do to store my queues' base type (that I call
<QueueEntry>) on disk. Accordingly I clicked on <IState> to see where
it was declared. Unfortunately that resulted in not the specific de-
claration of <IState> coming up but an interface for <IState>, which
gave me absolutely no information at all about the actual representa-
tion of the <IState> values my program is going to be working with.
However, the interface mentioned that <IState> extends <Serializable>.
I read the information on interface <Serializable> in the Java API,
and it looks like the fact that <IState> extends that interface means
that I can write it to disk and read it back from disk. In particu-
lar, from what I've read it seems like there's no reason why I
couldn't make class <QueueEntry> itself extend <Serializable>, which
would go a long way to solving my problem.
But having read the API and having discovered (I think) that I can
write <QueueEntry> objects to disk and read them from disk, I still
don't see precisely _how_ to write them and read them. At least the
exact procedure didn't _seem_ to be documented in the API. Is there
anyone out there that can tell me how that's done? Or who can point
me to where it's actually documented? Thanks in advance for any in-
formation you can give me.
---Kevin Simonson
"You'll never get to heaven, or even to LA,
if you don't believe there's a way."
from _Why Not_
ing the capability of Kansas State University's Bogor model checking
tool. I'm using Eclipse as a software development tool. Eclipse lets
me click on a variable or class name and see where that variable or
class is declared. Bogor is capable of taking a BIR file as an input
and then gives me a <currentState> variable that tells me which state
the program is currently in (starting with the program's initial
state) and a <doTransition()> method that changes <currentState> from
its current value to one of its successor states. So using Bogor on a
given program I can build the state graph that is equivalent to that
program.
My program stores information for a set of FIFO queues each of which
includes a state (of class <IState>), an <int> state id, a <boolean>
accepting value telling me whether this state is an accepting state or
not, and an <int> that identifies the set of accepting predecessors
this state has.
The problem that I have is that these queues have grown so large that
my program has run out of memory. So it has become necessary to write
the contents of a queue to disk when that queue becomes too large. So
naturally I wanted to look at the <IState> class definition to find
out what I would need to do to store my queues' base type (that I call
<QueueEntry>) on disk. Accordingly I clicked on <IState> to see where
it was declared. Unfortunately that resulted in not the specific de-
claration of <IState> coming up but an interface for <IState>, which
gave me absolutely no information at all about the actual representa-
tion of the <IState> values my program is going to be working with.
However, the interface mentioned that <IState> extends <Serializable>.
I read the information on interface <Serializable> in the Java API,
and it looks like the fact that <IState> extends that interface means
that I can write it to disk and read it back from disk. In particu-
lar, from what I've read it seems like there's no reason why I
couldn't make class <QueueEntry> itself extend <Serializable>, which
would go a long way to solving my problem.
But having read the API and having discovered (I think) that I can
write <QueueEntry> objects to disk and read them from disk, I still
don't see precisely _how_ to write them and read them. At least the
exact procedure didn't _seem_ to be documented in the API. Is there
anyone out there that can tell me how that's done? Or who can point
me to where it's actually documented? Thanks in advance for any in-
formation you can give me.
---Kevin Simonson
"You'll never get to heaven, or even to LA,
if you don't believe there's a way."
from _Why Not_