*** 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 * 3 variable(s) and 4 locs(s) and 4 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 : 3 vars, 4 locations, 4 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 6 vars, 5(5==5) transitions and 5 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * LRA with acceleration with delay = 1 main *** Results : * Invariants = f5 -----> {A<=0, B<=0, B<=B__o, A=A__o, C=1} f0 -----> {C=C__o, B=B__o, A=A__o} f2 -----> {A__o>0, A=A__o, B=B__o, C=1} ____f0 -----> {true} f4 -----> {B<=B__o, A<=0, A=A__o, C=0} * Remember that we have no bad region * Acceleration has been applied around 1 location(s) * Stats = { time=0.001000; iterations=1; descendings=0; } print result in fast++ Finished !