The intent is to remove states from the passed set once we know that we will
never need them again. To do this we will add guarded progress measures to UPPAAL.

A stable predicate is a predicate that if it is satisfied in a state,
s, it is satisfied in all states reachable from a.

A guarded progress measure is a tuple (g, p), where g is a stable
predicate and p is an expression that grows monotonically when g is
satisfied. If g is a tautology, then the guarded progress measure is a
traditional (monotone) progress measure as defined in the papers about
the sweep line method. Notice that a predicate that is a progress
measure is in fact a stable predicate.

We propose the following syntactic extension of UPPAAL: A new keyword
'progress' is added to the language. The keyword marks a progress
measure declaration section. The section looks something like this:

progress
{
  g1 : e1;
  g2 : e2;
  ...
}

where g1 and g2 are guards, and e1 and e2 are progress measures. A
progress measure declaration section is allowed in a declaration
section and after the system declaration line (where it can refer to
actual processes).

Notice that the guard could be eliminated by setting the progress
measure to -infinity when the guard is not satisfied, i.e. (g, p) is
equivalent to (true, g ? p : -infinity). However, in the
implementation we only check if expressions are syntactically
equivalent and therefore the split into a guard and a progress measure
is very useful in some cases (not for the sweep line method, but there are other
uses where this is nice).

The different progress measures can easily be combined into a single
partially ordered progress measure (see the sweep line paper about
compositional progress measures).

Three major changes are required for the implementation:

Parser: The parser needs to be updated to allow the progress measure
declaration section. This involves the bison parser, the system
builder, the type checker and the TimedAutomataSystem class.

PWList: The PWList must be updated to allow removing garbage
states. This might be done by adding a garbage collector to the PWList
(as is done traditionally for the sweep line method) or by splitting
the hash table of the PWList into several hash tables with one for
each progress value. The latter avoids the garbage collection all
together as should be faster. We propose implementing the latter idea.

Avoiding garbage: We define progress values based on the progress
measures, (gi, pi). If we have n progress measures, then a progress
value is an n-tuple (v1, v2,...,vn) where vi is the value of progress
measure pi. The progress value of a state s is a n-tuple (v1, v2,
... vn) where vi is the result of evaluating pi in s when g is
satisfied, or -infinity if g is not satisfied.

Garbage is avoided by using the sweep line method. The sweep line is
given by a progress value, which initially is -infinity. When all
states with a lower progress meassure have been explored, these can be
removed from the PWList and the progress value is increased (the sweep
line is moved). A good search order is probably to explore minimal
progress states first.