*** 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 * 68 variable(s) and 14 locs(s) and 30 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 : 68 vars, 14 locations, 30 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