*** 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 * 23 variable(s) and 42 locs(s) and 129 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 : 23 vars, 42 locations, 129 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 46 vars, 130(130==130) transitions and 43 locs now * Printing option = Infile+Invars * Parsing OK, now analysing * LRA with acceleration with delay = 1