[Javapathfinder-svn] SF.net SVN: javapathfinder:[1890] branches/mango/Mango/ javapathfinder-mango-bridge/mango/rewriter/MangoState.java

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

Revision: 1890
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1890&view=rev
Author:   frankrimlinger
Date:     2009-09-04 04:20:48 +0000 (Fri, 04 Sep 2009)

Log Message:
-----------
Splicing total state is easy.  The thing to keep in mind is that each branch point gets its own choice generator.  So the choice generator is the logical place to store the accumulated total state s_0.  The first instruction of a transition, say with formal state s, sets

totalState=(o s s_0)
partialState=s

For i>0, the i'th instruction sets 
totalState=(o s totalState_i-1)
partialState=(o s partialState_i-1)

Having said this, since we will be composing with loop invocations, which may or may not represent state transitions (because the loop could hang), the sound thing to do is to work in the dual category of predicate transformers, which always exist.  Most people just check out when you talk about the dual category, but oh well, it is necessary.  For the record, predicate transformers in a nutshell:  
S= set of states
s is a state transformer s:S->S
b is a predicate, b:S->{t,f}
P the set of predicates
A predicate transformer is just a map P->P.  These can be bad, but it turns out that every predicate transformer arising from deterministic control flow factors as s*^b*, where duality (*) is defined like so, for any predicate p,

s*(p)=pS
b*(p)=b

For any control flow diagram with vertices which are state transformers s and edges which are predicates b, the dual diagram just replaces s with s* and b with b*^id*, where id is the identity state transformer.  Composing backwards along a path gives a potential state transition, but you have an ugly computation involving the branch conditions to get the constraint.  The situation is much nicer in the dual graph, composing forwards just give the accumulated predicate transformer, which takes a predicate at the end of a path to its weakest precondition at the beginning.  None of this would make any difference, except that a loop can be modelled in full generality as a deterministic predicate transformer, a simple exercise for the reader.  (Hint: b(s)=false for all states which hang the loop).

So, MangoState is refactored like so:

class MangoState{
	Hitem totalDual;
	Hitem partialDual;
}

The choice generator stores the accumulated totalDual, x_0. 
First transition= x*^b*, you assume b, and:
totalDual=(o x_0  x)
partialDual= x

i'th transition= x*^b*, you assume b, and:
totalDual=(o totalDual_i-1 x)
partialDual=(o partialDual_i-1 x)

This is all fine and well, but still need to write the code for Step update.

Modified Paths:
--------------
    branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoState.java


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