Unable to change case expression's auto-generated "otherwise" basic expression

mbeddr / mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.

https://sites.google.com/site/fastenroot/home

Apache License 2.0

23 stars 14 forks source link

Unable to change case expression's auto-generated "otherwise" basic expression #62

Closed robertguetzkow closed 3 years ago

robertguetzkow commented 3 years ago

It seems that it is currently not possible to alter the auto-generated otherwise case in a case-expression when using the DSL for STATE-MACHINE. This prevents the default case from altering state variables. For instance it is not possible to decremented a counter/timer whenever none of the guard conditions are true. While the _040_state_machines documentation states that the DSL restricts the NuSMV base language, it doesn't mention this restriction.

ratiud commented 3 years ago

thank you for reporting the issues about the documentation - I have just fixed them