*** 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 * 21 variable(s) and 12 locs(s) and 32 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 : 21 vars, 12 locations, 31 transitions * The initial state has label start0 and the associated polyhedron is { $>=0,1>0} * There is/are 0 bad node(s) * Precomputing special stuff for ranking option 42 vars, 32(32==32) transitions and 13 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * LRA with acceleration with delay = 1 main *Hum* A problem occured when accelerating the loops, now trying with -noaccel option * Name of model = main, Name of file = main.fst * 21 variable(s) and 12 locs(s) and 32 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 : 21 vars, 12 locations, 31 transitions * The initial state has label start0 and the associated polyhedron is { $>=0,1>0} * There is/are 0 bad node(s) * Precomputing special stuff for ranking option 42 vars, 32(32==32) transitions and 13 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * classical LRA (CH79) with delay = 4 main *** Results : * Invariants = start -----> {R=S, R=S__o, P=Q, P=Q__o, N=O, N=O__o, L=M, L=M__o, J=K, J=K__o, H=I, H=I__o, F=G, F=G__o, D=E, D=E__o, B=C, B=C__o, A=T, A=A__o} stop -----> {A=T, A=A__o, C=C__o, E=E__o, G=G__o, I=I__o, K=K__o, M=M__o, O=O__o, Q=Q__o, S=S__o} lbl71 -----> {A>2, A>P, 2R+1>=0, P>=R, P>=1, L=M, N=O, A=T, A=A__o, C=C__o, E=E__o, G=G__o, I=I__o, K=K__o, L=M__o, N=O__o, Q=Q__o, S=S__o} lbl271 -----> {A<=B+1, P>=0, N>=1, A>N+P+1, 4J+5>=0, B>2J, A>B, N=R, A=T, A=A__o, C=C__o, E=E__o, G=G__o, I=I__o, K=K__o, M=M__o, O=O__o, Q=Q__o, S=S__o} lbl133 -----> {4J+5>=0, A>B, A>L+N+1, N<=R, A>=L+2, A>=R, L>=0, A+3N>=R+3, A<=L+N+R+2, L+N>=1, B>2J, A<=B+1, L+1=P, A=T, A=A__o, C=C__o, E=E__o, G=G__o, I=I__o, K=K__o, M=M__o, O=O__o, Q=Q__o, S=S__o} lbl281 -----> {A>N+P+1, A<=B+1, B>2J, A>B, P>=0, N>=1, 4J+5>=0, A=R, A=T, A=A__o, C=C__o, E=E__o, G=G__o, I=I__o, K=K__o, M=M__o, O=O__o, Q=Q__o, S=S__o} lbl101 -----> {A>2, A>P, 2J+2>=R, P>=1, P>=R, R>0, 2J {A>2, A>B, B>=1, B>=R, 2J+2>=R, 2R+1>=0, 2J {A>2, A>P, 2D+2>=R, 2F+2>=R, 2J+2>=R, P>=1, P>=R, R>0, 2J {A>2, A>P, 2D+2>0, 2D+2>2R, 2D+2>2J, 2D+2>2F, 2F+2>0, 2F+2>2R, 2F+2>2J, 2J+2>0, 2J+2>2R, P>=1, P>2R, 2R+2>0, 2J<2R+2, 2J {A>2, A>P, 2D+2>=R, 2J+2>=R, P>=1, P>=R, R>0, 2J {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, T=T__o, U=U__o} ____start0 -----> {true} * Remember that we have no bad region * No accel has been applied * Stats = { time=0.487000; iterations=11; descendings=0; } print result in fast++ Finished !