Map clocks to DBM/Zone indices

[senniraf]

Hi, I'm currently evaluating the exploration engine of momba for timed automata. I got the problem that I cannot determine which index in the DBM/Zone refers to which clock. There is a function in the clock-zones crate that iterates through the clocks:

momba/engine/crates/clock-zones/src/zones.rs

Lines 215 to 217 in 4c202d4

	pub fn clocks<Z: Zone>(zone: &Z) -> impl Iterator<Item = Clock> {
	(0..zone.num_clocks()).map(Clock)
	}

Could this function be made accessible from python? Or is there another way to determine which clock is mapped to which index?

[koehlma]

Exposing this function would not help as it does not provide the mapping.

The mapping itself can be reconstructed by using the Translation object which is in principle accessible through the explorer via ._compiled.translation. The Translation contains Declarations which are used for the clock_variables:

momba/momba/engine/translator.py

Lines 859 to 863 in 4c202d4

	"clock_variables": [
	declaration.identifier
	for declaration in declarations.all_declarations
	if declaration.typ == model.types.CLOCK
	]

The clocks are later in the same order as in this list (starting at index 1).

I am sorry, that there currently is no more convenient way to access the mapping. What would be required is a function similar to

momba/momba/engine/explore.py

Line 224 in 4c202d4

def get_local_env(self, instance: model.Instance) -> t.Mapping[str, Value]:

which accesses the declarations in order to find the correct clock index.