Leaking Gaz Burner: ASPIC Result




Initialising Polka
 ---- Configuration of Aspic 
   * name of file : gb.fst 
   * inputfile of type Fast 
   * ANALYSIS 
   * with acceleration 
   * delay of widening = 1 
The Fast file has been sucessfully parsed 
 
 ---- Beginning of translation to the internal language 
   * Name = gb 
   * 3 variable(s) 
   * Searching objective in fast strategy 
       -> we suppose that we want to compute post*(init) with init a convex set
       or post*(init) and bad if the state bad exists and bad is convex
       -> Dealing with the bad state(s).  done. 
       -> Finding initial polyhedron. done. 
   * 2 state(s) and 4 (possibly non convex) transitions 
       -> vertices/transitions for the automaton itself, done
       -> now dealing with the bad locations, we have 1 bad region
          ## we have no bad node, just a formula 
       -> vertices/transitions for the safety property (bad locations), done
   * The initial state has label ell and the associated polyhedron is {
l=0,t=0,x=0,1>0,$>=0} 
   * There is/are 1 bad node(s)
  ---- End of translation to the internal language

The module is done
The encoded graph has 3 vertex and 6 edges 
After splitting simpleloops, the graph has 5 vertex and 6 edges 
Initial graph=[
               { v = hen, attrvertex = { reach=empty(3); first=empty(3);
                                         bottom=true }  }
               { v = ell, attrvertex = { reach={l=0,t=0,x=0,1>0,$>=0};
                                         first={l=0,t=0,x=0,1>0,$>=0};
                                         bottom=false }  }
               { v = __bad_0, attrvertex = { reach=empty(3); first=empty(3);
                                             bottom=true }  }
               { v = hen__split, attrvertex = { reach=empty(3);
                                                first=empty(3); bottom=true }  }
               { v = ell__split, attrvertex = { reach=empty(3);
                                                first=empty(3); bottom=true }  }
               info = { itime=0.000000; iiterations=0; idescendings=0;
                        iinit=[ell]; iworkvertex=[ell__split];
                        iworkhedge=[t1] }
               ]
Result  graph=[
               { v = hen, attrvertex = { reach={x=0,$>=0,1>0,l>=0,t+50>=6l,
                                                t>=l}; first=empty(3);
                                         bottom=false }  }
               { v = ell, attrvertex = { reach={x=0,t>=6l,1>0,$>=0,l>=0};
                                         first={l=0,t=0,x=0,$>=0,1>0};
                                         bottom=false }  }
               { v = __bad_0, attrvertex = { reach=empty(3); first=empty(3);
                                             bottom=true }  }
               { v = hen__split, attrvertex = { reach={x+6l<=t+50,x+l<=t,
                                                       $>=0,1>0,l>=0,x>=0};
                                                first=empty(3); bottom=false }  }
               { v = ell__split, attrvertex = { reach={x<=10,x<=l,$>=0,1>0,
                                                       x>=0,5x+t>=6l};
                                                first=empty(3); bottom=false }  }
               info = { itime=0.000000; iiterations=4; idescendings=0;
                        iinit=[ell]; iworkvertex=[]; iworkhedge=[] }
               ]
 ---- Result : All the bad locations are unreachable