Ada: Lot of specification is exported in Ada. We use ghost code to store all states,we generate the transition pridicate but also the invariant. But two problems, occured.The first one is a visibility problem for the record which is private but must bepublic for ghost variable which have to be public for specifaction. The second...
Ada: First support for transition predicate generation.
Ada: Refactor Ada Backend to reduce redundancy, make it more modular and more simple.