/* A Tvp program for exchanging left and right subtrees in a binary tree */ #define COMPLETE /* #define FULL #define BLUR_ENTRY #define BLUR_SUMMARY #define ANCESTOR */ // ********************************************************************** // ********************************************************************** // SETS and PREDICATE DECLARATIONS // ********************************************************************** // ********************************************************************** // ====================================================================== // ====================================================================== // Program variables and fields // ====================================================================== %s ExchangeVarAll { tree, bLeft, bRight } %s MainVarAll { tree } %s VarAll ExchangeVarAll + MainVarAll %s Fields { left, right } %s Bools { } %s FP { fp1 } %s FR { } // ====================================================================== // Standard predicates // ====================================================================== #include "predicate.tvp" foreach (m in Mode){ foreach (z in VarAllFPR){ %r z(v_1) & r_down[m,z](v_2) & v_1!=v_2 & !cyc_down[m](v_1) ==> !down[m](v_2,v_1) #ifdef ANCESTOR %r z(v_2) & a_down[m,z](v_1) & v_1!=v_2 & !cyc_down[m](v_2) ==> !down[m](v_2,v_1) #endif } %r down[m](v_1,v_2) & !cyc_down[m](v_1) ==> !down[m](v_2,v_1) %r !cyc_down[m](v) & !sm(v) ==> !down[m](v,v) } #ifdef FULL %s InstrumMode1 InstrumMode1 + { full_left, full_right } foreach (m in Mode){ %i full_left[m](v) = (E(v_1) left[m](v,v_1)) -> (E(v_1) right[m](v,v_1)) nonabs %i full_right[m](v) = (E(v_1) right[m](v,v_1)) -> (E(v_1) left[m](v,v_1)) nonabs %r (E(v_1) left[m](v,v_1)) & (A(v_2) !right[m](v,v_2)) ==> !full_left[m](v) %r (E(v_1) right[m](v,v_1)) & (A(v_2) !left[m](v,v_2)) ==> !full_right[m](v) %r (E(v_1) left[m](v,v_1)) & (E(v_1) right[m](v,v_1)) ==> full_left[m](v) %r (E(v_1) left[m](v,v_1)) & (E(v_1) right[m](v,v_1)) ==> full_right[m](v) } #endif // ====================================================================== // specialized instrumentation predicates // ====================================================================== %s CrossInstrum1 CrossInstrum1 + { exch_right_succ, exch_left_succ } foreach (m1 in Mode){ foreach (m2 in Mode - { m1 }){ %i exch_right_succ[m1,m2](v) = A(v_1) ( right[m1](v,v_1) -> left[m2](v,v_1) ) abs %i exch_left_succ[m1,m2](v) = A(v_1) ( left[m1](v,v_1) -> right[m2](v,v_1) ) abs } } foreach (m1 in Mode){ foreach (m2 in Mode - { m1 }){ %r right[m1](v_1,v_2) & left[m2](v_1,v_2) ==> exch_right_succ[m1,m2](v_1) %r left[m2](v_1,v_2) & right[m1](v_1,v_2) ==> exch_left_succ[m2,m1](v_1) %r right[m1](v_1,v_2) & !left[m2](v_1,v_2) ==> !exch_right_succ[m1,m2](v_1) %r left[m1](v_1,v_2) & !right[m2](v_1,v_2) ==> !exch_left_succ[m1,m2](v_1) %r exch_right_succ[m1,m2](v_1) & right[m1](v_1,v_2) ==> left[m2](v_1,v_2) %r exch_left_succ[m1,m2](v_1) & left[m1](v_1,v_2) ==> right[m2](v_1,v_2) } } foreach (m1 in Mode){ foreach (m2 in Mode - {m1}){ foreach (m3 in Mode - {m1,m2}){ %r id_succ[right,m1,m2](v) & exch_right_succ[m2,m3](v) ==> exch_right_succ[m1,m3](v) %r id_succ[left,m1,m2](v) & exch_left_succ[m2,m3](v) ==> exch_left_succ[m1,m3](v) %r exch_right_succ[m1,m2](v) & id_succ[left,m2,m3](v) ==> exch_right_succ[m1,m3](v) %r exch_left_succ[m1,m2](v) & id_succ[right,m2,m3](v) ==> exch_left_succ[m1,m3](v) %r exch_right_succ[m1,m2](v) & exch_left_succ[m2,m3](v) ==> id_succ[right,m1,m3](v) %r exch_left_succ[m1,m2](v) & exch_right_succ[m2,m3](v) ==> id_succ[left,m1,m3](v) } } } // Important: linking reachability in different modes foreach (m1 in Mode){ foreach (m2 in Mode-{m1}){ foreach (z in VarAllFPR){ %r r_down[m1,z](v) & (A(v_1) (r_down[m1,z](v) -> ((id_succ[right,m1,m2](v_1) & id_succ[left,m1,m2](v_1)) | (exch_right_succ[m1,m2](v_1) & exch_left_succ[m1,m2](v_1))))) ==> r_down[m2,z](v) #ifdef ANCESTOR %r a_down[m1,z](v) & (A(v_1) ((a_down[m1,z](v) & !z(v_1))-> ((id_succ[right,m1,m2](v_1) & id_succ[left,m1,m2](v_1)) | (exch_right_succ[m1,m2](v_1) & exch_left_succ[m1,m2](v_1))))) ==> a_down[m2,z](v) #endif } } } // Other important things /* Idea: foreach (m in Mode){ %r r_down[m,bLeft](v) ==> !r_down[m,bRight](v) %r r_down[m,bRight](v) ==> !r_down[m,bLeft](v) } */ // Real things: two subtrees of two "independent" variables are disjoint // We specify it only for bRight and bLeft, but it could be generalized foreach (m in Mode){ %r r_down[m,bLeft](v) & (A(v) r_down[m,bLeft](v) -> !shared_down[m](v)) & (E(v_1,v_2) bLeft(v_1) & bRight(v_2) & v_1!=v_2 & !r_down[m,bLeft](v_2) & !r_down[m,bRight](v_1)) ==> !r_down[m,bRight](v) %r r_down[m,bRight](v) & (A(v) r_down[m,bRight](v) -> !shared_down[m](v)) & (E(v_1,v_2) bLeft(v_1) & bRight(v_2) & v_1!=v_2 & !r_down[m,bLeft](v_2) & !r_down[m,bRight](v_1)) ==> !r_down[m,bLeft](v) } %% // ********************************************************************** // ********************************************************************** // FUNCTION DEFINITIONS // ********************************************************************** // ********************************************************************** #include "function.tvp" %function BlurSummary[](X) %t "BlurSummary" { begin focus(X, { r_down[out,fp1](v), cyc_down[out](v), cyc_down[ext](v) }); let Y = transform(X, halt:E(v) cyc_down[out](v) | cyc_down[ext](v), update:{ #ifdef ANCESTOR foreach (m in Mode){ foreach(zz in VarAllFPR){ a_down[m,zz](v) = (r_down[out,fp1](v) ? a_down[m,zz](v) : 1/2) } } #endif foreach (m1 in Mode){ foreach (m2 in Mode - {m1}){ exch_right_succ[m1,m2](v) = (r_down[out,fp1](v) ? exch_right_succ[m1,m2](v) : 1/2) exch_left_succ[m1,m2](v) = (r_down[out,fp1](v) ? exch_left_succ[m1,m2](v) : 1/2) } } sm(v) = (r_down[out,fp1](v) ? sm(v) : 1/2) // Cross-instrumentation foreach(m in {out,ext}){ foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,m](v) = 1/2 p[f,m,inp](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,m](v_1,v_2) = 1/2 p[f,m,inp](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,m](v) = 1/2 p[m,inp](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,m](v_1,v_2) = 1/2 p[m,inp](v_1,v_2) = 1/2 } } }) in begin blur(Y); focus(Y, { cyc_down[out](v), cyc_down[ext](v) }); let Z = transform(Y, halt:E(v) cyc_down[out](v) | cyc_down[ext](v), ) in Z end end } %function BlurEntry[](X) %t "BlurEntry" { begin focus(X, { r_down[out,tree](v) }); let Y = transform(X, update:{ #ifdef ANCESTOR foreach (m in Mode){ foreach(zz in VarAllFPR){ a_down[m,zz](v) = 1/2 } } #endif foreach (m1 in Mode){ foreach (m2 in Mode - {m1}){ exch_right_succ[m1,m2](v) = (r_down[out,tree](v) ? exch_right_succ[m1,m2](v) : 1/2) exch_left_succ[m1,m2](v) = (r_down[out,tree](v) ? exch_left_succ[m1,m2](v) : 1/2) } } sm(v) = (r_down[out,tree](v) ? sm(v) : 1/2) // Cross-instrumentation foreach(m in {inp,out}){ foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,ext,m](v) = 1/2 p[f,m,ext](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,ext,m](v_1,v_2) = 1/2 p[f,m,ext](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[ext,m](v) = 1/2 p[m,ext](v) = 1/2 } foreach(p in CrossInstrum2){ p[ext,m](v_1,v_2) = 1/2 p[m,ext](v_1,v_2) = 1/2 } } }) in begin blur(Y); coerce(Y); Y end end } %function FocusReach[](X) %t "FocusReach" { begin focus(X, { r_down[inp,bLeft](v), r_down[inp,bRight](v) }); transform(X, halt: E(v) r_down[inp,bLeft](v) & r_down[inp,bRight](v)) end } %function FocusRTree[](X) %t "FocusRTree" { begin focus(X, { tree(v), r_down[out,tree](v) }); X end } %% // ********************************************************************** // ********************************************************************** // EQUATIONS // ********************************************************************** // ********************************************************************** // ********************************************************************** // exchange */ // ********************************************************************** /* The function function exchange(tree) : is var bRight,bLeft; begin exchange_entry: y := tree; exchange0: if (tree!=null){ exchange1: bRight = tree->right; exchange2: bLeft = tree->left; exchange3: tree->right = null; exchange4: tree->left = null; exchange5: tree->right = bLeft; exchange6: tree->left = bRight; exchange7: exchange(bRight); exchange8: exchange(bLeft); exchange_end: exchange_summary: end */ exchange_entry = call_X_1[exchange, tree, tree](main_call) exchange_entry = call_X_1[exchange, bRight, tree](exchange7) exchange_entry = call_X_1[exchange, bLeft, tree](exchange8) #ifdef BLUR_ENTRY exchange_entry0 = BlurEntry[](exchange_entry) exchange0 = IsVarNotNull[tree](exchange_entry0) exchange_end = IsVarNull[tree](exchange_entry0) #else exchange0 = IsVarNotNull[tree](exchange_entry) exchange_end = IsVarNull[tree](exchange_entry) #endif exchange2 = AssignVarNext[bRight,tree,right](exchange0) exchange3 = AssignVarNext[bLeft,tree,left](exchange2) exchange3a = FocusReach[](exchange3) exchange4 = AssignNextNull[tree,right](exchange3a) exchange5 = AssignNextNull[tree,left](exchange4) exchange6 = AssignNextVar[tree,right,bLeft](exchange5) exchange7 = AssignNextVar[tree,left,bRight](exchange6) exchange8 = ret_0_1[exchange, bRight](exchange7,exchange_summary) exchange_end = ret_0_1[exchange, bLeft](exchange8,exchange_summary) #ifdef BLUR_SUMMARY exchange_summary0 = summary_1_0[exchange,tree](exchange_end) exchange_summary = BlurSummary[](exchange_summary0) #else exchange_summary = summary_1_0[exchange,tree](exchange_end) #endif // ********************************************************************** // Main // ********************************************************************** main_call0 = Setup_1[tree](main_begin) main_call = FocusRTree[](main_call0) main_end = ret_0_1[exchange,tree](main_call,exchange_summary) %% exchange_entry exchange0 exchange4 exchange7 exchange8 exchange_end exchange_summary main_begin main_call main_end /* main_begin main_call0 main_call exchange_entry exchange0 exchange2 exchange3 exchange3a exchange4 exchange5 exchange6 exchange7 exchange8 exchange_end exchange_summary main_end */