Committed Locations

Uppaal has a feature called "committed locations".

The Uppaal Web Help 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