In Uppaal, is there a way to know how many states exists as the combination of locations and variables
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.