[Javapathfinder-devel] SF.net SVN: javapathfinder: [478] trunk

[<pcm...@us...>]

Revision: 478
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=478&view=rev
Author:   pcmehlitz
Date:     2007-08-06 12:22:48 -0700 (Mon, 06 Aug 2007)

Log Message:
-----------
* need to "internalize" state/sent-event pairs, to enable state matching if we send
the same event over again, and that's the only change in the JPF state space. If we just
create new PendingEvent instances, this would never match. We need to check for
multiple occurrences of the same PendingEvent anyways

the trick we do is that we keep the PendingEvent instances in the target state, and
just mark them as processed / re-enable them on subsequent sends. That way, we save
a static HashMap (which would need to be reset on every JPF run)

this isn't yet symmetrical with respect to event order yet

* moved the send event logging into native - no need to have StringBuffers and all that
on the model side

* added a little reminder assertion if we transition into a State instance that wasn't declared
'final'. Still need to explore if I might silently re-initialize in this case
(we still need to check for multiple substate adds anyways)

Modified Paths:
--------------
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEvent.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.