fmbt: account for aal-provided tag numbers starting at 0

[jamesjin0516]

@askervin

Original Issue

• The compiled code from fmbt-aalc, which extends aal class, returns tag indices starting at 0.
• The Awrapper::check_tags method assumes the said indices start at 1.

Fix: create an offset of 1 in Awrapper::tagaal2ada and Awrapper::tagada2aal variables.
Code has only been tested on the command line interface with a c++ program under test

[askervin]

Hi @jamesjin0516! Thank you for your patch! Would you provide some reasoning why would you need tags to be numbered starting from 0 instead of 1, please? There should be very heavy reasons to change this.

Actions are currently numbered starting from 1, too, leaving number 0 to be used as a special "invisible" action. Theoretical background for this choice is in the typical formal definition of Labelled Transition Systems (LTS) where set of transitions is often defined as a triplet: (start_state, action, end_state) and where action is one of normal actions (identified by 1, 2, ...) or a special invisible action often denoted by $\tau$ (identified by 0 in these data structures). See slide 7 onwards from this presentation for example.

I'm afraid it might be confusing if user-defined actions and user-defined tags are indexed differently. That is, tags are indexed starting from 1 for consistency.

[jamesjin0516]

Hello @askervin, I am happy to see that you replied! Actually, I would rather like the tags to be numbered starting from 1, so that they are consistent with the actions. I only made my changes when I realized fmbt-aalc produces C++ code that could number tags starting from 0 instead of 1 for some reason. I believe it only occurs in the derived implementation of aal::getprops, such as below:

virtual int getprops(int** props) {
	tags.clear();
	if ( (tag1_guard(tag_names[1]))) {
		tags.push_back(0);
	}
	if ( (tag2_guard(tag_names[2]))) {
		tags.push_back(1);
	}
	if ( (tag3_guard(tag_names[3]))) {
		tags.push_back(2);
	}
	if (tags.empty()) {
		*props = NULL;
	} else {
		*props = &tags[0];
	}
	return tags.size();
}

Furthermore, the method aal::check_tags numbers tags starting from 1. Perhaps this behaviour from fmbt-aalc is unintended?