*** 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 * 6 variable(s) and 9 locs(s) and 12 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 : 6 vars, 9 locations, 12 transitions * The initial state has label evalNestedMultiplestart and the associated polyhedron is { $>=0,1>0} * There is/are 0 bad node(s) * Precomputing special stuff for ranking option 12 vars, 13(13==13) transitions and 10 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * LRA with acceleration with delay = 1 main *** Results : * Invariants = evalNestedMultiplestart -----> {D=D__o, C=C__o, B=B__o, A=A__o, E=E__o, F=F__o} evalNestedMultipleentryin -----> {C=C__o, B=B__o, A=A__o, E=E__o, D=D__o} evalNestedMultiplebb5in -----> {D>=C__o, A=B__o, C=D__o} evalNestedMultiplebb2in -----> {D>=C__o, A>B, D<=E, A=B__o, C=D__o} evalNestedMultiplereturnin -----> {A<=B, D>=C__o, A=B__o, C=D__o} evalNestedMultiplebb4in -----> {A>B, D<=E, D>=C__o, A=B__o, C=D__o} evalNestedMultiplebb3in -----> {A>B, C>E, D>=C__o, D<=E, C=D__o, A=B__o} evalNestedMultiplebb1in -----> {A>B, D>=C__o, C>E, D<=E, A=B__o, C=D__o} evalNestedMultiplestop -----> {A<=B, D>=C__o, A=B__o, C=D__o} ____evalNestedMultiplestart -----> {true} * Remember that we have no bad region * No accel has been applied * Stats = { time=0.013000; iterations=6; descendings=0; } print result in fast++ Finished !