Skip to content

Ytm/parse : adding new dl_open + declaration + usage of "state labels" in PINS modules.

Yann Thierry-Mieg requested to merge ytm/parse into next

See issue #436

This patch contributes an extended PINS/LTSmin API, compatible with ITS-Tools produced models, that tries to parse atomic propositions in an LTL formula to label names declared in the PINS module first.

This patch is ascendant compatible, it changes nothing for PINS modules that do not have the functions (thanks to default values for these functions), but it lets PINs module that are able to do it to give us an efficient labeling function, similar to what Etienne is providing in his branch.

I don't usually do it, but if you want me to rewrite history I can try to squash the commits.

Merge request reports