[aorai] clean up comments from Promela/LTL references

src/plugins/aorai/aorai_utils.ml

@@ -1103,7 +1103,7 @@ let getInitialState () =
 (** This function computes all newly introduced globals (variables, enumeration structure, invariants, etc. *)
 let initGlobals root complete =
   mk_global_comment "//****************";
-  mk_global_comment "//* BEGIN Primitives generated for LTL verification";
+  mk_global_comment "//* BEGIN Primitives generated for Aorai verification";
   mk_global_comment "//* ";
   mk_global_comment "//* ";
   mk_global_comment "//* Some constants";
@@ -1168,7 +1168,7 @@ let initGlobals root complete =
      in
      Annotations.add_global Aorai_option.emitter annot);
   mk_global_comment "//* ";
-  mk_global_comment "//* END Primitives generated for LTL verification";
+  mk_global_comment "//* END Primitives generated for Aorai verification";
   mk_global_comment "//****************";
 
   flush_globals ()

src/plugins/aorai/automaton_ast.ml

@@ -23,7 +23,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** The abstract tree of promela representation. Such tree is used by promela
+(** The abstract tree of Ya representation. Such tree is used by
     parser/lexer before its translation into Data_for_aorai module. *)
 
 type expression =
@@ -57,7 +57,7 @@ and seq_elt = {
 
 and sequence = seq_elt list
 
-(** Promela parsed abstract syntax trees. Either a sequence of event or the
+(** Ya parsed abstract syntax trees. Either a sequence of event or the
     otherwise keyword. A single condition is expressed with a singleton
     having an empty nested sequence and min_rep and max_rep being equal to one.
 *)

src/plugins/aorai/data_for_aorai.mli

@@ -35,10 +35,10 @@ open Automaton_ast
 exception Empty_automaton
 
 (* ************************************************************************* *)
-(** {2 LTL/Promela primitives} *)
+(** {2 Automaton primitives} *)
 (* ************************************************************************* *)
 
-(** Here are some operations used for generation of LTL AST or Promela AST. *)
+(** Here are some operations used for generation of automaton AST. *)
 
 module Aorai_state: Datatype.S_with_collections with type t = Automaton_ast.state
 

src/plugins/aorai/pretty_automaton.ml

@@ -249,7 +249,7 @@ struct
       let spaces = String.make fill ' ' in
       Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces
     in
-    one_line_comment "File generated by Aorai LTL2ACSL Plug-in";
+    one_line_comment "File generated by Aorai Plug-in";
     one_line_comment "";
     one_line_comment "Usage of dot files '.dot' :";
     one_line_comment "  dot <MyFile.dot> -T<DesiredType> > <OutputFile>";

src/plugins/aorai/utils_parser.mli

@@ -23,7 +23,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** utilities for parsing automata and LTL formulas *)
+(** utilities for parsing automaton's formulas *)
 
 (** returns the position corresponding to the
     current character in the lexbuf. *)