Search code examples
uppaal

Uppaal : Is there a way to know the size of the state space?


In Uppaal, is there a way to know how many states exists as the combination of locations and variables


Solution

  • For predictions, one could naively multiply all automata locations and variable ranges, but this gives wastly pesimistic result, exceeding the real state space size most of the time, therefore it is meaningless.

    For estimating the state space, one can ask a query A[] true and use -u key for verifyta command line utility to get some statistics.

    Note that other search parameters (search order in particular) may yield different number of states, because the order of visited symbolic states may influence their zone size: larger zones may account as fewer states, and it takes more symbolic states with smaller zones to cover the same state space.