Remove automaton DSL

[amarmaduke]

Note that there are a lot of warnings in the old frontend after this change. I tried to just disable them with [@@@ocaml.warning "-.."] but maybe did something wrong. Since all that code is getting deleted soon I didn't bother investigating further. The only code I did remove from the old frontend was just what was needed to make kind2 compile.

[daniel-larraz]

The temporal operator last should be removed too. It was only used within the definition of an automaton.

I also found functions to print automata in lustre/lustrePath.ml, and a reference to automata in a comment in lustre/lustreDeclarations.ml. In addition, Ocaml 4.13 reports the following warning:

File "src/lustre/lustreAstInlineConstants.ml", line 358, characters 4-5:
358 |   | e -> e
          ^
Warning 11 [redundant-case]: this match case is unused.

@amarmaduke, could you please address these issues?
Thanks.

[rxzephyr]

Hi, the recent release seems to have removed support for the automata. In my rough understanding, the automaton structure is more like a syntactic sugar but in some cases it may be possible to simplify the modeling. I am just curious about the decision and could you please tell me the reason?

[daniel-larraz]

Hi @rxzephyr. The support for automata was an experimental feature. The automaton DSL was designed to capture the full expressiveness of SCADE 6 automata, which led to the use of an internal encoding in Kind 2 that was suboptimal for the verification of properties. In particular, several users reported performance issues verifying models with automata when compared to model checking desugared versions of their models. These models were only using a subset of the features offered by SCADE 6 automata. So when we implemented the new Kind 2's language front-end included in the latest release, we decided to drop the support for automata. Our plan for future versions of the tool is to offer alternative constructs that focus on the actual needs of Kind 2's users. In particular, we are considering adding an imperative-style if-statement to the language to allow the user group a set of stream updates under the same condition while keeping the rest of stream values unchanged. This new construct combined with the use of enumerated types would cover some of the use cases we saw, and would simplify the internal encoding. But we would appreciate any feedback you may have. Were you using automata on your models? If so, would the imperative-style if-statement be helpful? Were you using any of the advanced features of the automaton DSL?

Thanks.

[rxzephyr]

In my use case, the imperative-style if-statement would be enough. Thank you for the explanation.

[daniel-larraz]

Thank you for your feedback.