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

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

Revision: 260
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=260&view=rev
Author:   pcmehlitz
Date:     2007-02-23 00:58:59 -0800 (Fri, 23 Feb 2007)

Log Message:
-----------
* added a first version of the inverse state space spec for state machines: PathConstraints
this thing defines sequences of events that - if not matched - cause the current choice to
be ignored. This uses a choiceGeneratorAdvanced() notification, during which we might
skip the choice

* the UGLY thing is that SCEventFromAlphabet generators have this nasty behavior of being
expanded on demand (which might be deferred in the presence of completion triggers), in which
case they have to be explicitly advanced in the StateMachine native peer (i.e. after its out
of SystemState's hands). Hence we have to refactor the notification in SystemState, but that's not
yet satisfactory. However, the current 'skip choice' mechanism is very questionable in
the context of trace replay, so this has to be changed anyways

Modified Paths:
--------------
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
    trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/util/script/ESParser.java
    trunk/src/gov/nasa/jpf/util/script/ScriptElementContainer.java

Added Paths:
-----------
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/PathConstraint.java


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