This is just a typedef. location to be used in program graphs An IMPACT consists of an initial node corresponding to the initial location, and a list of nodes each with an invariant and corresponding location. Multiple expressions mean a lexicographic ranking function. Lexicographic ranking functions should be given a bound for each component. Create a new location. The argument is a skip transition from new -> old The effect is that all sharp transitions (l -phi-> old) will be replaced by (l -phi-> new) and the skip transition is added. Of, if the argument is a skip transition from old -> new, then all sharp transitions (old -phi-> l) will be replaced by (new -phi-> l) and the skip transition is added. Fresh Variable Addition: introduces a new variable x of given type into the transitions. For each (non-skip) transition one can specify in an additional formula how x should be updated, as long as it is non-conflicting.