Re: [Javapathfinder-user] JPF Extension

[Peter C. M. <pcm...@em...>]

Hi Carlos,

Willem already mentioned this - we have the same requirements with the 
UML state chart model checking, where we want to store every UML step as 
a JPF state, but still do state matching. We are still experimenting 
with this, but you can do it with ChoiceGenerators. Look at the 
extensions/statechart/env/jpf/StateMachine.run() (which is kind of a 
template method) and the getEnablingEvents() method in it's native peer 
(which is the state storage point).  This works because the only 
condition that's used to determine transition boundaries is if executing 
an instruction causes a new ChoiceGenerator to be registered in the 
SystemState. What looks a bit weird is that you might get some 
degenerated ChoiceGenerators that only exist for state storage purposes, 
i.e. don't really produce choices  (e.g. the 
gov.nasa.jpf.jvm.choice.sc.NullSCEventGenerator), but that's in general 
fine with specialized CG's where you obtain and process the choices 
explicitly in your code. Generic things like ThreadChoiceGenerators 
would be different of course.

With respect to your second question, it depends on how complex your 
state extension is, and whether it involves executing its own code or 
just consists of simple data. If it can be reduced to scalar values 
(builtin types) then it's probably best to go with Willem's suggestion - 
store it as field values into a JPF object, and get the state 
storage/matching/restoration for free. If it gets complex (e.g. graphs), 
and you don't want to create tons of JPF objects that actually might 
blow up your JPF state space (which you nowadays can also filter of 
course), then you might consider doing it like 
gov.nasa.jpf.util.script.EventGeneratorFactory, i.e. use the JPF state 
id to store/restore your extensions from a SearchListener. I'm not sure 
if the EventGeneratorFactory is such a good example when to use this, 
but it should at least show you how to use it.

-- Peter

Carlos Pita wrote:
> Hi all,
> 
> I'm writing an extension to jpf and I would like to ask you a couple of
> questions. The point of this extension is to check high-level, abstract,
> architectural properties. To achieve this a mapping from patterns of
> what I call low-level events (mainly method invocations) to high-level
> events (architectural domain events) is defined. Once a high-level event
> is emitted -in response to a complete low-level event sequence that was
> received from the underlying model checker- a number of actions (that
> is, high-level state mutators) would be executed and a number of
> assertions (that is, high-level properties that I want to check) would
> be proved of the high-level state. Pictorially:
> 
> jvm listener
>      |
>      v
> LLEvt1, LLEvt2, ... ---> Mapper---> HLEvt---> Actions (modify HLState)
>                                        |
>                                        '--> Assertions (check HLState)
> 
> (where LL stands for low-level and HL for high-level)
> 
> To catch the low-level events I'm listening to executeInstruction events
> from the jpf jvm. Upon reception of a low-level event the mapper can
> change its internal state (the state of the automata implementing the
> patterns). Also eventually a low-level pattern would reach its final
> state and a high-level event would be emitted, probably modifying the
> high-level state. Both of this state changes are scheduling relevant,
> from the point of view of the checker, so every time the mapper state or
> the high-level model state change, the current thread should be
> rescheduled:
> 
> executeInstruction(vm) {
>    if instruction is invocation {
>      create LLEvent
>      feed the mapper with the event
>      if mapper.hasChanged or hlState.hasChanged {
>         store serialized changed state into jpf system state
>         vm.currentThread.reschedule
>      }
>    }
> }
> 
> Question #1: is this the right/best way to force a transition?
> 
> Notice that I want to store my external states as byte arrays inside jpf own
> state. So as a consequence both the mapper and the high-level states
> are serializable.
> Every time these states change, not only a transition must happen but
> also the aforementioned states must be serialized and stored into jpf. I
> thought of storing them into jpf's heap area, but I'm not sure at all,
> so here goes question #2:
> 
> Question #2: is this the right/best way to make jpf aware of external
> state?
> 
> Well, I think that's all for now. Any help would be appreciated.
> 
> Thank you in advance.
> Regards,
> Carlos
> 
> -------------------------------------------------------------------------
> Take Surveys. Earn Cash. Influence the Future of IT
> Join SourceForge.net's Techsay panel and you'll get the chance to share your
> opinions on IT & business topics through brief surveys - and earn cash
> http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>