This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 274 - Nested path formula
Summary: Nested path formula
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 4
Hardware: All All
: P3 enhancement
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-02-22 09:59 CET by Gerd Behrmann
Modified: 2006-03-09 10:00 CET (History)
1 user (show)

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Gerd Behrmann 2006-02-22 09:59:27 CET 
At the moment it is not possible to nest path formula. However, with very little effort we could restructure 
the engine to allow at least some nesting. This would make is possible to check for, e.g., home states (A[] 
E<> p).

The amount of changes required for this is relatively small and I consider to implement this between beta 
1 and beta 2.
Comment 1 Gerd Behrmann 2006-03-09 10:00:49 CET 
Actually, the approach I thought about will have serious performance issues. Therefore slightly larger changes will be needed, so I bump this to 3.8.