Re: [Javapathfinder-devel] GSoC

[Peter C. M. <Pet...@na...>]

Hi Carl,

if you look into extensions/statechart, and esp. the examples/jpfESAS  
directory, you see that JPF models UML statecharts as a hierarchy of  
nested classes, where each class represents a state in the diagram.  
Triggers are just normal instance methods of these classes, and  
transitions correspond to setNextState(<tgt-state>) calls. The only  
overhead is that states need to be instantiated, i.e. the whole  
structure corresponds almost 1:1 to the diagram.

Since there is this close correspondence, it's possible to (re-) 
create the diagram out of the JPF classes, display it in it's own  
window, and use that display to animate traces found by the model  
checker (i.e. step through a sequence of events that cause a property  
violation). This consists of two steps:

(1) create a diagram out of the JPF internal state model (stored as a  
hierarchy of States, and accessible from within StateMachine). This  
is mostly a layout problem

(2) use SimStateMachine and Listeners to animate the execution of a  
sequence of events within this diagram/view (please look at the JPF  
website docu under "Search and VMListeners" for more details about  
listeners). It actually might be more easy just to write a derived  
SimStateMachine (say "VisualStateMachine") and use that for driving  
your animation w/o using a listener

-- Peter  



On Apr 5, 2008, at 1:27 PM, <ca...@um...> <ca...@um...> wrote:
> Hi this is Carl Albach.  I wrote previously asking a few  
> questions.  I've already
> submitted my application for the visualization of JPF's statechart  
> model checking
> extension idea.  I'm very interested in the idea.  I just wanted to  
> maybe refine the
> description on the application and find out a little more about the  
> project.  If there
> is anything more you could tell me about it, that would be great.   
> Also, the project
> idea page mentions that it would rely on the JPF Listener API.  If  
> you could point
> me in the direction of that API that would also be helpful.  Thanks  
> a lot.
>
> Carl Albach
>
> ---------------------------------------------------------------------- 
> ---
> This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
> Register now and save $200. Hurry, offer ends at 11:59 p.m.,
> Monday, April 7! Use priority code J8TLD2.
> http://ad.doubleclick.net/clk;198757673;13503038;p?http:// 
> java.sun.com/javaone
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel