*** Aspic by Laure Gonnord, version 3.4 Binary compiled on vendredi 1 janvier 2016 Input file = main.fst *** Configuration of Aspic * (version 3.4) * name of file : main.fst * inputfile of type (real) Fast format * PRINTING all stuff for compsys ranking method * DEBUG : Only prints analysis steps in a separate .log file * PRINTING STUFF : Infile+Invars * ANALYSIS * with acceleration * delay of widening = 1 * steps of descending sequence = 0 * newpath heuristic = disabled * Name of model = main, Name of file = main.fst * 30 variable(s) and 22 locs(s) and 67 transitions(s) in the .fst * 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 -> Initial region "init" found -> Finding initial polyhedron. OK. -> No bad region INFO : 30 vars, 22 locations, 67 transitions * The initial state has label f0 and the associated polyhedron is { $>=0,1>0} * There is/are 0 bad node(s) * Precomputing special stuff for ranking option 60 vars, 68(68==68) transitions and 23 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * LRA with acceleration with delay = 1 mainjust one = empty(60)just one = {L=Y__o,F=X__o,A=0,B=1,C=1,D=4,O=O__o, P=P__o,G=0,H=0,I=0,J=0,K=0,Q=Q__o,M=2, N=0,R=R__o,S=S__o,T=T__o,U=U__o,V=V__o, E=W__o,$>=0,1>0,E>1}just one = { F=X__o,E=W__o,A=0,B=1,C=1,D=4,O=O__o,P=P__o,G=0,H=0,I=0,J=0,K=0,Q=Q__o, L=Y__o,N=0,R=R__o,S=S__o,T=T__o,U=U__o,V=V__o,$>=0,1>0,M>=2,E+1>M}just one = { F=X__o,E=W__o,A=0,B=1,C=1,D=4,O=O__o,P=P__o,G=0,H=0,I=0,J=0,K=0,Q=Q__o, L=Y__o,N=0,R=R__o,S=S__o,T=T__o,U=U__o,V=V__o,$>=0,1>0,M>=2,E+1>M}just one = empty(60)just one = { Q=Q__o,L=Y__o,S=S__o,B=0,C=1,D=4,R=R__o,T=T__o,G=0,H=0,I=0,J=0,K=0,U=U__o, M=0,V=V__o,O=3,P=0,E=W__o,F=X__o,$>=0,1>0,E>2,A<=1}just one = {L=Y__o, F=X__o, S=S__o,B=0, C=1,D=4, R=R__o, T=T__o,G=0, H=0,I=0,J=0, K=0,U=U__o, E=W__o, V=V__o, Q=Q__o,P=0, A<=1,M+2<=O, E+1>O,M>=0, 1>0,M<5,$>=0}just one = { F=X__o,E=W__o,S=S__o,B=0,C=1,D=4,Q=Q__o,T=T__o,G=0,H=0,I=0,J=0,K=0,U=U__o, L=Y__o,V=V__o,R=R__o,P=0,$>=0,1>0,M>=0,E>M,E+1>O,A<=1}just one = {F=X__o, E=W__o, S=S__o, B=0,C=1, D=4, Q=Q__o, T=T__o, G=0,H=0, I=0,J=0, K=0, U=U__o, L=Y__o, V=V__o, R=R__o, P=0,$>=0, 1>0,M>=0, E>M,E+1>O, A<=1} *Hum* A problem occured when accelerating the loops, now trying with -noaccel option * Name of model = main, Name of file = main.fst * 30 variable(s) and 22 locs(s) and 67 transitions(s) in the .fst * 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 -> Initial region "init" found -> Finding initial polyhedron. OK. -> No bad region INFO : 30 vars, 22 locations, 67 transitions * The initial state has label f0 and the associated polyhedron is { $>=0,1>0} * There is/are 0 bad node(s) * Precomputing special stuff for ranking option 60 vars, 68(68==68) transitions and 23 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * classical LRA (CH79) with delay = 4 main *** Results : * Invariants = f129 -----> {A>=0, C>=0, M>=4, O>=4, Q>=0, Q+1>R, R>=0, V>=0, V<=1, R<=1, Q<=1, O<5, M<5, C<=1, B<=1, A<=1, D=4, E=W__o, F=X__o, L=Y__o, U=U__o, G=V} f130 -----> {A>0, C>=0, G>=0, M>=4, O>=4, Q>=0, Q+1>R, R>=0, R<=1, Q<=1, O<5, M<5, G<=1, C<=1, B<=1, A<=1, D=4, U=U__o, L=Y__o, G=V, F=X__o, E=W__o} f131 -----> {A>0, C>=0, G>=0, M>=4, O>=4, Q>=0, Q+1>R, R>=0, R<=1, Q<=1, O<5, M<5, G<=1, C<=1, B<=1, A<=1, D=4, U=U__o, L=Y__o, G=V, F=X__o, E=W__o} f132 -----> {A>0, C>0, G>=0, M>=4, O>=4, Q>=0, Q+1>R, R>=0, R<=1, Q<=1, O<5, M<5, G<=1, C<=1, B<=1, A<=1, D=4, U=U__o, L=Y__o, G=V, F=X__o, E=W__o} f0 -----> {B1=B1__o, A1=A1__o, Z=Z__o, Y=Y__o, X=X__o, W=W__o, V=V__o, U=U__o, T=T__o, S=S__o, R=R__o, Q=Q__o, P=P__o, O=O__o, N=N__o, M=M__o, L=L__o, K=K__o, J=J__o, I=I__o, H=H__o, G=G__o, F=F__o, E=E__o, D=D__o, C=C__o, B=B__o, A=A__o, C1=C1__o, D1=D1__o} f25 -----> {M>=0, A=1, B=1, C=1, D=4, G=0, H=0, I=0, J=0, K=0, N=N__o, O=O__o, P=P__o, Q=Q__o, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f31 -----> {A<=1, A>=0, A+M>=1, B=1, C=1, D=4, G=0, H=0, I=0, J=0, K=0, O=O__o, P=P__o, Q=Q__o, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f34 -----> {A+M>=1, A>0, E>M, A<=1, B=1, C=1, D=4, G=0, H=0, I=0, J=0, K=0, V=V__o, U=U__o, T=T__o, S=S__o, R=R__o, Q=Q__o, P=P__o, O=O__o, L=Y__o, F=X__o, E=W__o} f44 -----> {B<=1, A>=0, A<=1, C=1, D=4, G=0, H=0, I=0, J=0, K=0, Q=Q__o, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f47 -----> {A>=0, A<=1, B<=1, M+1<=O, E+1>O, C=1, D=4, G=0, H=0, I=0, J=0, K=0, Q=Q__o, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f50 -----> {A>=0, E>O, M+1<=O, B<=1, A<=1, C=1, D=4, G=0, H=0, I=0, J=0, K=0, V=V__o, U=U__o, T=T__o, S=S__o, R=R__o, Q=Q__o, L=Y__o, F=X__o, E=W__o} f60 -----> {A>=0, A<=1, B<=1, M>=0, M<5, C=1, D=4, G=0, I=0, J=0, K=0, Q=Q__o, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f66 -----> {A>=0, M>=4, M<5, B<=1, A<=1, C=1, D=4, G=0, I=0, J=0, K=0, V=V__o, U=U__o, T=T__o, S=S__o, R=R__o, Q=Q__o, L=Y__o, F=X__o, E=W__o} f72 -----> {B<=1, C>=0, M>=0, M<5, A>=0, C<=1, A<=1, D=4, G=0, J=0, K=0, C=Q, R=R__o, S=S__o, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f78 -----> {A>=0, C>0, M>=4, M<5, C<=1, B<=1, A<=1, D=4, G=0, J=0, K=0, V=V__o, U=U__o, T=T__o, S=S__o, R=R__o, L=Y__o, F=X__o, E=W__o, C=Q} f84 -----> {Q<=1, R<=1, A<=1, B<=1, R>=0, Q+1>R, Q>=0, M<5, C>=0, C+M>=R, A>=0, 2C {M<4, Q<=1, R<=1, A<=1, B<=1, R>=0, Q+1>R, Q>=0, O>=0, 2C=0, C+M>=R, A>=0, C<=M+R, D=4, G=0, K=0, T=T__o, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f94 -----> {A>=0, C+M>=R, C>0, O>=4, Q>=0, Q+1>R, R>=0, R<=1, Q<=1, O<5, M<4, C<=M+R, C<=1, 2C {M>=4, M<5, Q<=1, R<=1, A<=1, B<=1, C<=1, R>=0, Q+1>R, Q>=0, O>=0, A>=0, C>=0, O<5, D=4, G=0, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f106 -----> {Q<=1, R<=1, A<=1, B<=1, R>=0, Q+1>R, Q>=0, O>=0, M>=0, M<5, C<=1, O<4, C>=0, A>=0, D=4, G=0, U=U__o, V=V__o, E=W__o, F=X__o, L=Y__o} f112 -----> {A>=0, C>0, M>=4, O>=0, Q>=0, Q+1>R, R>=0, R<=1, Q<=1, O<4, M<5, C<=1, B<=1, A<=1, D=4, G=0, V=V__o, U=U__o, L=Y__o, F=X__o, E=W__o} f141 -----> {O>=4, A>=0, U<=1, U+V>0, A+U>0, C+U>0, V>=0, C>=0, R>=0, Q>=0, M>=4, Q+1>R, R<=1, Q<=1, O<5, M<5, U>=0, A+B+C+U+V<=4, V<=1, C<=1, B<=1, A<=1, D=4, L=Y__o, G=V, E=W__o, F=X__o} ____f0 -----> {true} * Remember that we have no bad region * No accel has been applied * Stats = { time=4.948000; iterations=52; descendings=0; } print result in fast++ Finished !