Uppaal has a feature called "*committed locations*". The [Uppaal Web Help](http://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Locations.shtml) describes it as follows: > Like urgent locations, committed locations freeze time. Furthermore, if any process is in a committed location, the next transition must involve an edge from one of the committed locations. This has the potential of reducing the state space a lot. For example if we have five locations where each has an enabled (and urgent) transition. - if _none_ of them are committed, we have `5! = 120` distinct sequences - if _one_ location is committed, we have `1! * 4! = 24` distinct sequences - if _two_ locations are committed, we have `2! * 3! = 12` distinct sequences