Leaking Gaz Burner: ASPIC Log




Analyzing : gb 
** Initialisation ** 
end_of_make_inigraph 
 ... edge = t4 from hen to ell : {x>=50} --> x |-> 0 ;
 ... edge = t3 from hen to hen : {} --> t |-> t + 1 ;x |-> x + 1 ;
 ... edge = t2 from ell to hen : {} --> x |-> 0 ;
 ... edge = t1 from ell to ell : {x<=9} --> l |-> l + 1 ;x |-> x + 1 ;t |-> t + 1 ;
 ... edge = __trans_hen_to___bad_0 from hen to __bad_0 : {t+50<6l} --> 
 ... edge = __trans_ell_to___bad_0 from ell to __bad_0 : {t+50<6l} --> 
end_of_make_transfotab 

 The transfo types : [SimpleReset;Simple;SimpleReset;Simple;Simple;Simple;] 
 

 The graph loops structure = [[1; 4; 0; 3]; 2]

** Creation of the FP module ** 

 strategy=[[(ell,[t4],true); (ell__split,[t1],false); (hen,[t2],false);
            (hen__split,[t3],false)];
           (__bad_0,[__trans_ell_to___bad_0,__trans_hen_to___bad_0],false)]
*** Analysis...  Processing strategy [[(ell,[t4],true); (ell__split,[t1],false);
                        (hen,[t2],false); (hen__split,[t3],false)];
                       (__bad_0,[__trans_ell_to___bad_0,__trans_hen_to___bad_0],false)]
  Processing strategy [(ell,[t4],true); (ell__split,[t1],false);
                       (hen,[t2],false); (hen__split,[t3],false)]
  processing vertex ell__split :
    the old polyhedron is  empty(3) 
meta_trans of type Simple    contrib of hedge t1 = {x=l,x=t,$>=0,1>0,x>=0,
                                                    x<=10}
    nreach={x=l,x=t,$>=0,1>0,x>=0,x<=10}
  processing vertex hen :
    the old polyhedron is  empty(3) 
    contrib of hedge t2 = {x=0,t=l,l>=0,$>=0,l<=10,1>0}
    the contributions from the preceeding nodes is  {x=0,t=l,l>=0,$>=0,l<=10,
                                                     1>0} 
    apply many loops :
        step 1 : Single contrib of all loops each alone : 
        step 2 : contrib of all loops alltogether : 
   --- contrib 123 = {
x=0,t=l,l>=0,$>=0,l<=10,1>0} 
        step 3 : re-apply all loops each alone : 
    contrib of loop -edges  = {
x=0,t=l,l>=0,$>=0,l<=10,1>0}
    nreach={x=0,t=l,l>=0,$>=0,l<=10,1>0}
  processing vertex hen__split :
    the old polyhedron is  empty(3) 
meta_trans of type Simple    contrib of hedge t3 = {x+l=t,x+10>=t,$>=0,1>0,
                                                    x<=t,x>=0}
    nreach={x+l=t,x+10>=t,$>=0,1>0,x<=t,x>=0}
  processing vertex ell with widening:
    the old polyhedron is  {l=0,t=0,x=0,$>=0,1>0} 
    contrib of hedge t4 = {x=0,t>=l+50,$>=0,l>=0,1>0,l<=10}
    the contributions from the preceeding nodes is  {x=0,l>=0,1>0,t>=6l,$>=0,
                                                     l<=10} 
    apply many loops :
        step 1 : Single contrib of all loops each alone : 
        step 2 : contrib of all loops alltogether : 
   --- contrib 123 = {
x=0,l>=0,1>0,t>=6l,$>=0,l<=10} 
        step 3 : re-apply all loops each alone : 
    contrib of loop -edges  = {
x=0,l>=0,1>0,t>=6l,$>=0,l<=10}
    nreach={x=0,l>=0,1>0,t>=6l,$>=0,l<=10}
    widening {l=0,t=0,x=0,$>=0,1>0} by {x=0,l>=0,1>0,t>=6l,$>=0,l<=10} 
    widening = {x=0,$>=0,1>0,t>=6l,l>=0}
  processing vertex ell__split :
    the old polyhedron is  {x=l,x=t,x<=10,$>=0,1>0,x>=0} 
meta_trans of type Simple    contrib of hedge t1 = {x<=l,$>=0,1>0,x>=0,
                                                    5x+t>=6l,x<=10}
    nreach={x<=l,$>=0,1>0,x>=0,5x+t>=6l,x<=10}
  processing vertex hen :
    the old polyhedron is  {t=l,x=0,l<=10,$>=0,1>0,l>=0} 
    contrib of hedge t2 = {x=0,$>=0,1>0,t>=l,l>=0,t+50>=6l}
    the contributions from the preceeding nodes is  {x=0,$>=0,1>0,t>=l,l>=0,
                                                     t+50>=6l} 
    apply many loops :
        step 1 : Single contrib of all loops each alone : 
        step 2 : contrib of all loops alltogether : 
   --- contrib 123 = {
x=0,$>=0,1>0,t>=l,l>=0,t+50>=6l} 
        step 3 : re-apply all loops each alone : 
    contrib of loop -edges  = {
x=0,$>=0,1>0,t>=l,l>=0,t+50>=6l}
    nreach={x=0,$>=0,1>0,t>=l,l>=0,t+50>=6l}
  processing vertex hen__split :
    the old polyhedron is  {x+l=t,x<=t,$>=0,1>0,x+10>=t,x>=0} 
meta_trans of type Simple    contrib of hedge t3 = {x+6l<=t+50,x+l<=t,$>=0,
                                                    1>0,l>=0,x>=0}
    nreach={x+6l<=t+50,x+l<=t,$>=0,1>0,l>=0,x>=0}
  processing vertex ell with widening:
    the old polyhedron is  {x=0,$>=0,1>0,t>=6l,l>=0} 
    contrib of hedge t4 = {x=0,t>=l+50,$>=0,l>=0,1>0,t>=6l}
    the contributions from the preceeding nodes is  {x=0,t>=6l,1>0,$>=0,l>=0} 
    apply many loops :
        step 1 : Single contrib of all loops each alone : 
        step 2 : contrib of all loops alltogether : 
   --- contrib 123 = {
x=0,t>=6l,1>0,$>=0,l>=0} 
        step 3 : re-apply all loops each alone : 
    contrib of loop -edges  = {
x=0,t>=6l,1>0,$>=0,l>=0}
    no change
  End Processing strategy [(ell,[t4],true); (ell__split,[t1],false);
                           (hen,[t2],false); (hen__split,[t3],false)]
  Sum up of the looping step (3 iterations)
    acc(ell)={x=0,t>=6l,1>0,$>=0,l>=0}
    acc(ell__split)={x<=10,x<=l,$>=0,1>0,x>=0,5x+t>=6l}
    acc(hen)={x=0,$>=0,1>0,l>=0,t+50>=6l,t>=l}
    acc(hen__split)={x+6l<=t+50,x+l<=t,$>=0,1>0,l>=0,x>=0}
  processing vertex __bad_0 :
    the old polyhedron is  empty(3) 
    the contributions from the preceeding nodes is  empty(3) 
    apply many loops :
    no change
  End Processing strategy [[(ell,[t4],true); (ell__split,[t1],false);
                            (hen,[t2],false); (hen__split,[t3],false)];
                           (__bad_0,[__trans_ell_to___bad_0,__trans_hen_to___bad_0],false)]
  Sum up of the looping step (1 iterations)
    acc(ell)={x=0,t>=6l,1>0,$>=0,l>=0}
    acc(ell__split)={x<=10,x<=l,$>=0,1>0,x>=0,5x+t>=6l}
    acc(hen)={x=0,$>=0,1>0,l>=0,t+50>=6l,t>=l}
    acc(hen__split)={x+6l<=t+50,x+l<=t,$>=0,1>0,l>=0,x>=0}
    acc(__bad_0)=empty(3)

** End of FP iteration, printing output in gb.dot ** 

 output=[
         { v = hen, attrvertex = {x=0,$>=0,1>0,l>=0,t+50>=6l,t>=l},
                    succ-edge = [t3],
                    pred-edge = [t2] }
         { v = ell, attrvertex = {x=0,t>=6l,1>0,$>=0,l>=0},
                    succ-edge = [t1],
                    pred-edge = [t4] }
         { v = __bad_0, attrvertex = empty(3),
                        succ-edge = [],
                        pred-edge = [__trans_hen_to___bad_0
                                     __trans_ell_to___bad_0] }
         { v = hen__split, attrvertex = {x+6l<=t+50,x+l<=t,$>=0,1>0,l>=0,x>=0},
                           succ-edge = [t4 __trans_hen_to___bad_0],
                           pred-edge = [t3] }
         { v = ell__split, attrvertex = {x<=10,x<=l,$>=0,1>0,x>=0,5x+t>=6l},
                           succ-edge = [t2 __trans_ell_to___bad_0],
                           pred-edge = [t1] }
         { n = t4, attrhedge = (),
                   succ-vertex = [|ell|],
                   pred-vertex = [|hen__split|] }
         { n = t3, attrhedge = (),
                   succ-vertex = [|hen__split|],
                   pred-vertex = [|hen|] }
         { n = t2, attrhedge = (),
                   succ-vertex = [|hen|],
                   pred-vertex = [|ell__split|] }
         { n = t1, attrhedge = (),
                   succ-vertex = [|ell__split|],
                   pred-vertex = [|ell|] }
         { n = __trans_hen_to___bad_0, attrhedge = (),
                                       succ-vertex = [|__bad_0|],
                                       pred-vertex = [|hen__split|] }
         { n = __trans_ell_to___bad_0, attrhedge = (),
                                       succ-vertex = [|__bad_0|],
                                       pred-vertex = [|ell__split|] }
         info = { time=0.010000; iterations=4; descendings=0; }
         ]