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:
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
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.
Prototype implementation has been checked in, although we need more work for
alternative search orders and the generalised sweep line method (with
non-monotonic progress measures).
An implementation of the generalised sweep line method has been in CVS for some time.
The main thing missing is type checking of the progress measures.
Type checking has now been implemented and the sweepline method is enabled by default.
A problem remaining is related to the use of the storage architecture (bug 30): By default, the discrete
storage classes do not deallocate memory until the storage is freed. With the sweep line method, this
means that they might hold onto a lot of memory that they could just as well be freed.
Also, with current implementation of the sweepline method, storage instances are not shared between
states with different progress values, not sharing is reduced.
Finally, choosing a progress measure with *many* different values causes the exploration to become very
slow and use a lot of memory due to the large number of state sets that will be allocated.
The issue with storage not deallocating memory has been fixed by deallocating empty state sets whenever
the sweepline is advanced. This also solves the problem with excessive memory usage when using a
progress measure that yields many different progress values.
It does however not add sharing between state set instances and it does not solve the problem that using
a progress measure with *many* values is very slow (a factor of 150 slower in my test).
Increasing priority. We should try to get this in before 3.6 alpha 2. This feature is more or less ready, but I
need to check the code to see if anything is missing and create a few test cases.
I have updated the sweepline implementation. The new implementation shares one stateset between all frontiers, thus potentially reducing memory consumption. There are still some issues: E.g. at the moment all states in a frontier are locked even when not on the waiting list. Thus they cannot be freed. However, as an inital implementation of the sweepline method, the current version is good enough.
I will resolve the bug as fixed. Further improvements should be documented in new bugs.