| Summary: | Implement sweep line method | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Gerd Behrmann <behrmann> |
| Component: | Engine | Assignee: | Gerd Behrmann <behrmann> |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | CC: | martijnh |
| Priority: | P1 | ||
| Version: | unspecified | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
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. |
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.