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

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

Revision: 634
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=634&view=rev
Author:   pcmehlitz
Date:     2007-10-18 13:43:48 -0700 (Thu, 18 Oct 2007)

Log Message:
-----------
* added optional event receiver constraints. For scripts, this is specified as

   [<receiver-pattern> {'|' <receiver-pattern> } ':'] <event-name> ['(' <args> ')']
   
where receiver pattern is using or StringSetMatcher notation, NOT general regexes, which means the only
meta char is the wildcard '*' (like a Unix wildcard char).

Explicitly sent events don't need receiver constraints, because they get them automatically. If we send an event to
an explicitly specified state, this implies it's only processed by itself or its children. Sounds sound, but the
implementation hurts (we pull it out of the PendingEvents queue of the receiver, just to encode the receiver again
in the SCEvent id). Nothing is perfect. At least, the receiver filter is consistent (all in NativeStateMachine and
SCEvent)

The SimStateMachine still needs to be updated accordingly

* added a little ReceiverConstraints example for this

* added a multiple-instances filter to NativeStateMachine.createCGFromPendingEvents(), since the hierarchical
lookup can lead to multiple inclusions of the same event, which just makes life harder for the model checker

Modified Paths:
--------------
    trunk/examples/jpfESAS/launch/CEV-ascent-guards.launch
    trunk/examples/jpfESAS/launch/CEV-safehold.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-bt.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless.launch
    trunk/examples/jpfESAS/launch/CEV-tli.launch
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
    trunk/src/gov/nasa/jpf/util/StringSetMatcher.java

Added Paths:
-----------
    trunk/extensions/statechart/examples/ReceiverConstraints.es
    trunk/extensions/statechart/examples/ReceiverConstraints.java


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