Skip to content

Bug resolution on TML to UPPAAL translation

Bastien Sultan requested to merge branch_bastien into master

Workaround for the following bug: when there is an action state in a TML behavior diagram, liveness verification with verifyta always returns "false" for this action state and all the following TML activity elements.

Workaround: in generated UPPAAL specification, the previous location shall be a committed (or urgent) location. tmltranslator/touppaal/TML2UPPAAL.java has been updated in consequence.

Furthermore a new test has been created in order to check if, in a generated UPPAAL specification, the previous location of a translated TML action state is committed or urgent. The following files (resp. the test and the TML resource file) have been added:

  • ttool/src/test/java/tmltranslator/UPPAALCommittedStateTest.java
  • ttool/src/test/resources/tmltranslator/touppaal/spec.tml

Merge request reports