[Javapathfinder-svn] SF.net SVN: javapathfinder:[1244] branches/mango/extensions/mango

[<fra...@us...>]

Revision: 1244
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1244&view=rev
Author:   frankrimlinger
Date:     2009-03-02 19:50:38 +0000 (Mon, 02 Mar 2009)

Log Message:
-----------
Fixed some E-Z bugs, and invariant rules fired correctly for itsAWrap.clear().  Finished the icon binding chore.  Next bug: rewriter fails to acknowledge termination conjecture for itsAWrap.clear().  

Have started thinking about jpf integration.  Since jpf likes to boot off a preferences file, the obvious thing is to generate such a file and use it to wake up jpf in a new thread.  As jpf wakes up it will generate the java model.  Mango must then observe this model and use it to generate the Mango model.  Then new code must be written to convert the mango model into annotations that are usable by jpf.  Also, a control mechanism must be written to step jpf from the mango gui.  Then this apparatus must be tested against the prototype test set (which incidentally remains to be generated.)  With all this in place, the new invariant strategy based on the jpf backtracing mechanism can be layered in.  From there, other innovations to enhance automation will be introduced.  The mango gui will never entirely wither away, because certain kinds of reason really do require user input.  But the long term goal would be for it to blend into the development platform so that programmers could use the tool without actually knowing it was there.

Modified Paths:
--------------
    branches/mango/extensions/mango/Mango/src/mango/deprecatedPackage/factory/TreeModelFactory.java
    branches/mango/extensions/mango/Mango/src/mango/worker/engine/events/RewriteEvent.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/graphic/CallEdgeSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/graphic/InvocationEdgeSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/graphic/SourceLineSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/graphic/VertexSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/reflection/ReflectionSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/AssertionSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/ucon/AlphaSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
    branches/mango/extensions/mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
    branches/mango/extensions/mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
    branches/mango/extensions/mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantFactorizationAgent.java
    branches/mango/extensions/mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/itsAWrap/clear([I)V/a.zip


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