From 45733c4347322e10c914672f850fbc9c8093bc3e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 11 Oct 2022 10:43:44 +0200
Subject: [PATCH] [aorai] clean up comments from Promela/LTL references
---
src/plugins/aorai/aorai_utils.ml | 4 ++--
src/plugins/aorai/automaton_ast.ml | 4 ++--
src/plugins/aorai/data_for_aorai.mli | 4 ++--
src/plugins/aorai/pretty_automaton.ml | 2 +-
src/plugins/aorai/utils_parser.mli | 2 +-
5 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 2530178dcd3..27d890da479 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/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 ()
diff --git a/src/plugins/aorai/automaton_ast.ml b/src/plugins/aorai/automaton_ast.ml
index 897f87b0ed1..d7ea342f231 100644
--- a/src/plugins/aorai/automaton_ast.ml
+++ b/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.
*)
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 8cf944ec63b..a3c5d459953 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/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
diff --git a/src/plugins/aorai/pretty_automaton.ml b/src/plugins/aorai/pretty_automaton.ml
index 1ccf2caf684..b91c1d103ba 100644
--- a/src/plugins/aorai/pretty_automaton.ml
+++ b/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>";
diff --git a/src/plugins/aorai/utils_parser.mli b/src/plugins/aorai/utils_parser.mli
index bb89f79da9f..4505784eea2 100644
--- a/src/plugins/aorai/utils_parser.mli
+++ b/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. *)
--
GitLab