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

Bug 274

Summary:	Nested path formula
Product:	UPPAAL	Reporter:	Gerd Behrmann <behrmann>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	ASSIGNED ---
Severity:	enhancement	CC:	paupet
Priority:	P3
Version:	3.6 Alpha 4
Hardware:	All
OS:	All
Architecture:

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.