From c26f0c98341c3c6338076a7a6e76ad94f95525a8 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 12 Sep 2024 15:59:41 +0200 Subject: [PATCH] Remove requirements tool and references for feature coverage Ref. eng/recordflux/RecordFlux#1783 --- doc/language_reference/language_reference.rst | 584 ------------------ .../generated/rflx-test-s-fsm.adb | 10 +- .../fsm_append_unconstrained/test.rflx | 18 +- .../generated/rflx-test-s-fsm.adb | 4 +- .../fsm_case_expression_aggregate/test.rflx | 27 +- .../fsm_case_expression_numeric/test.rflx | 24 +- .../fsm_channel_multiplexing/test.rflx | 30 +- tests/feature/fsm_channels/test.rflx | 18 +- .../generated/rflx-test-s-fsm.adb | 34 +- .../feature/fsm_comprehension_head/test.rflx | 39 +- .../generated/rflx-test-s-fsm.adb | 28 +- .../test.rflx | 26 +- .../generated/rflx-test-s-fsm.adb | 50 +- .../fsm_comprehension_on_sequence/test.rflx | 34 +- tests/feature/fsm_conversion/test.rflx | 26 +- tests/feature/fsm_endianness/test.rflx | 4 +- .../generated/rflx-test-s-fsm.adb | 22 +- tests/feature/fsm_functions/test.rflx | 69 +-- .../generated/rflx-test-s-fsm.adb | 14 +- tests/feature/fsm_functions_opaque/test.rflx | 42 +- .../generated/rflx-test-s-fsm.adb | 4 +- tests/feature/fsm_integration/test.rflx | 23 +- .../generated/rflx-test-s-fsm.adb | 8 +- tests/feature/fsm_message_creation/test.rflx | 31 +- .../generated/rflx-test-s-fsm.adb | 68 +- .../fsm_message_optimization/test.rflx | 60 +- tests/feature/fsm_minimal/test.rflx | 16 +- tests/feature/fsm_reuse_of_message/test.rflx | 14 +- .../generated/rflx-test-s-fsm.adb | 14 +- tests/feature/fsm_sequence_append/test.rflx | 24 +- .../generated/rflx-test-s-fsm.adb | 40 +- .../fsm_sequence_append_head/test.rflx | 65 +- .../generated/rflx-test-s-fsm.adb | 22 +- .../fsm_setting_of_message_fields/test.rflx | 40 +- .../fsm_simple/generated/rflx-test-s-fsm.adb | 4 +- tests/feature/fsm_simple/test.rflx | 25 +- .../generated/rflx-test-s-fsm.adb | 8 +- .../fsm_variable_initialization/test.rflx | 31 +- .../generated/rflx-test-s-fsm.adb | 6 +- .../messages_with_implict_size/test.rflx | 19 +- .../generated/rflx-test-s-fsm.adb | 6 +- .../test.rflx | 19 +- .../feature/parameterized_messages/test.rflx | 2 +- tools/check_requirements.py | 193 ------ 44 files changed, 501 insertions(+), 1344 deletions(-) delete mode 100755 tools/check_requirements.py diff --git a/doc/language_reference/language_reference.rst b/doc/language_reference/language_reference.rst index afc489138..09cf9b373 100644 --- a/doc/language_reference/language_reference.rst +++ b/doc/language_reference/language_reference.rst @@ -255,54 +255,8 @@ Extended boolean expressions are used in state machines. The Valid attribute allows to determine the validity of a message or sequence. -.. - Valid attribute [§S-E-AT-V] - - Expressions: - - * Mathematical Expressions [§S-E-AT-V-ME] - * Boolean Expressions [§S-E-AT-V-BE] - * Literals [§S-E-AT-V-L] - * Variables [§S-E-AT-V-V] - * Message Aggregates [§S-E-AT-V-MA] - * Aggregates [§S-E-AT-V-A] - * Valid Attributes [§S-E-AT-V-VAT] - * Opaque Attributes [§S-E-AT-V-OAT] - * Size Attributes [§S-E-AT-V-SAT] - * Head Attributes [§S-E-AT-V-HAT] - * Has_Data Attributes [§S-E-AT-V-HDAT] - * Selected Expressions [§S-E-AT-V-S] - * List Comprehensions [§S-E-AT-V-LC] - * Quantified Expressions [§S-E-AT-V-Q] - * Calls [§S-E-AT-V-CL] - * Conversions [§S-E-AT-V-CV] - - Whether a channel contains data can be checked with the Has_Data attribute. -.. - Has_Data attribute [§S-E-AT-HD] - - Expressions: - - * Mathematical Expressions [§S-E-AT-HD-ME] - * Boolean Expressions [§S-E-AT-HD-BE] - * Literals [§S-E-AT-HD-L] - * Variables [§S-E-AT-HD-V] - * Message Aggregates [§S-E-AT-HD-MA] - * Aggregates [§S-E-AT-HD-A] - * Valid Attributes [§S-E-AT-HD-VAT] - * Opaque Attributes [§S-E-AT-HD-OAT] - * Size Attributes [§S-E-AT-HD-SAT] - * Head Attributes [§S-E-AT-HD-HAT] - * Has_Data Attributes [§S-E-AT-HD-HDAT] - * Selected Expressions [§S-E-AT-HD-S] - * List Comprehensions [§S-E-AT-HD-LC] - * Quantified Expressions [§S-E-AT-HD-Q] - * Calls [§S-E-AT-HD-CL] - * Conversions [§S-E-AT-HD-CV] - - Sizes ----- @@ -313,19 +267,12 @@ A size aspect defines the size of a type or message field in bits. .. productionlist:: size_aspect: "Size" "=>" `math_expression` - -.. - Types [§T] - Scalar Types ============ Integer Types ------------- -.. - Integers [§T-I] - An integer type is used to represent whole numbers. **Syntax** @@ -352,9 +299,6 @@ The bit size has to be specified explicitly. Enumeration Types ----------------- -.. - Enumerations [§T-E] - An enumeration type represents a value out of a list of possible values. **Syntax** @@ -402,9 +346,6 @@ A message field with such type is always considered valid, whether or not its va Boolean ------- -.. - Booleans [§T-B] - ``Boolean`` is a built-in enumeration type with the literals ``False => 0`` and ``True => 1`` with a size of 1 bit. Parameters and Arguments @@ -426,9 +367,6 @@ Named arguments associate a parameter with an expression. Message Types ============= -.. - Messages [§T-M] - A message type is a collection of fields. Additional `then clauses <#grammar-token-then_clause>`_ enable the definition of conditions and dependencies between fields. @@ -551,9 +489,6 @@ All bytes which were received when parsing or were written when serializing are Type Refinements ================ -.. - Type Refinements [§T-R] - A type refinement describes the relation of an opaque field in a message type to another message type. **Syntax** @@ -585,9 +520,6 @@ To indicate that a refined field is empty (i.e. does not exist) under a certain Type Derivations ================ -.. - Derived Messages [§T-D] - A type derivation enables the creation of a new message type based on an existing message type. **Syntax** @@ -611,9 +543,6 @@ Type refinements of a base message type are not inherited by the derived message Sequence Types ============== -.. - Sequences [§T-S] - A sequence type represents a list of similar elements. **Syntax** @@ -627,10 +556,6 @@ A sequence type represents a list of similar elements. A sequence consists of a number of elements with the same type. Scalar types as well as message types can be used as element type. -.. - Sequence of scalars [§T-S-S] - Sequence of messages [§T-S-M] - **Example** .. doc-check: rflx,basic_declaration @@ -641,9 +566,6 @@ Scalar types as well as message types can be used as element type. State Machines ============== -.. - State Machines [§S] - A state machine defines the dynamic behavior of a protocol using a finite state machine. The first defined state is considered the initial state. The external interface of a state machine is defined by parameters. @@ -693,9 +615,6 @@ The main part of a state machine definition is the state definitions. State Machine Parameters ------------------------ -.. - State Machine Parameters [§S-P] - Functions and channels can be defined as state machine parameters. **Syntax** @@ -708,9 +627,6 @@ Functions and channels can be defined as state machine parameters. Functions ^^^^^^^^^ -.. - Functions [§S-P-F] - Functions enable the execution of externally defined code. **Syntax** @@ -728,24 +644,11 @@ Allowed parameter types: - Definite messages - Opaque fields of messages -.. - Allowed parameter types [§S-P-F-P] - - * Scalars [§S-P-F-P-S] - * Definite messages [§S-P-F-P-M] - * Opaque fields of messages [§S-P-F-P-O] - Allowed return types: - Scalars - Definite messages -.. - Allowed return types [§S-P-F-R]: - - * Scalars [§S-P-F-R-S] - * Definite messages [§S-P-F-R-M] - Definite messages are messages with no optional fields and an explicit size (i.e. all size aspects contain no reference to ``Message``). **SPARK** @@ -768,9 +671,6 @@ The return type and parameters of a function are represented by the first and su Channels ^^^^^^^^ -.. - Channels [§S-P-C] - Channels provide a way for communicating with other systems using messages. **Syntax** @@ -785,11 +685,6 @@ Channels provide a way for communicating with other systems using messages. Channels can be readable or writable (non-exclusive). -.. - * Readable [§S-P-C-R] - * Writable [§S-P-C-W] - * Readable and writable [§S-P-C-RW] - **Example** .. doc-check: rflx,state_machine_parameter @@ -800,9 +695,6 @@ Channels can be readable or writable (non-exclusive). Declarations ------------ -.. - Declarations [§S-D] - Variables and renamings can be globally declared (i.e. for the scope of the complete state machine). **Syntax** @@ -815,9 +707,6 @@ Variables and renamings can be globally declared (i.e. for the scope of the com Variable Declaration ^^^^^^^^^^^^^^^^^^^^ -.. - Variable Declaration [§S-D-V] - A declared variable must have a type and can be optionally initialized using an expression. **Syntax** @@ -827,34 +716,6 @@ A declared variable must have a type and can be optionally initialized using an : ":" type_`qualified_name` : [ ":=" initialization_`expression` ] -.. - Types [§S-D-V-T]: - - * Scalar [§S-D-V-T-SC] - * Message [§S-D-V-T-M] - * Scalar Sequence [§S-D-V-T-SS] - * Message Sequence [§S-D-V-T-MS] - - Initialization expressions [§S-D-V-E]: - - * No initialization [§S-D-V-E-N] - * Mathematical Expressions [§S-D-V-E-ME] - * Boolean Expressions [§S-D-V-E-BE] - * Literals [§S-D-V-E-L] - * Variables [§S-D-V-E-V] - * Message Aggregates [§S-D-V-E-MA] - * Aggregates [§S-D-V-E-A] - * Valid Attributes [§S-D-V-E-VAT] - * Opaque Attributes [§S-D-V-E-OAT] - * Size Attributes [§S-D-V-E-SAT] - * Head Attributes [§S-D-V-E-HAT] - * Has_Data Attributes [§S-D-V-E-HDAT] - * Selected Expressions [§S-D-V-E-S] - * List Comprehensions [§S-D-V-E-LC] - * Quantified Expressions [§S-D-V-E-Q] - * Calls [§S-D-V-E-CL] - * Conversions [§S-D-V-E-CV] - **Example** .. doc-check: rflx,declaration @@ -865,9 +726,6 @@ A declared variable must have a type and can be optionally initialized using an Renaming Declaration ^^^^^^^^^^^^^^^^^^^^ -.. - Renaming Declaration [§S-D-R] - **Syntax** .. productionlist:: @@ -886,12 +744,6 @@ Renaming Declaration States ------ -.. - States [§S-S] - State Declarations [§S-S-D] - Variable declarations [§S-S-D-V] - Renaming declarations [§S-S-D-R] - A state defines the to be executed actions and the transitions to subsequent states. Variable declarations and renaming declarations in a state have a state-local scope, i.e., local declarations cannot be accessed from other states. @@ -915,9 +767,6 @@ Variable declarations and renaming declarations in a state have a state-local sc **Static Semantics** -.. - Exception Transition [§S-S-E] - An exception transition must be defined just in case any action might lead to a critical (potentially non-recoverable) error: - Insufficient memory for setting a field of a message @@ -932,35 +781,6 @@ See the sections `Read Attribute Statements`_ and `Write Attribute Statements`_ IO states cannot contain any declarations and they must not contain any other operations than channel IO. Each channel and each message can be read or written at most once in a given IO state. -.. - Types [§S-S-D-V-T]: - - * Scalar [§S-S-D-V-T-SC] - * Message [§S-S-D-V-T-M] - * Scalar Sequence [§S-S-D-V-T-SS] - * Message Sequence [§S-S-D-V-T-MS] - - Initialization expressions [§S-S-D-V-E]: - - * No initialization [§S-S-D-V-E-N] - * Mathematical Expressions [§S-S-D-V-E-ME] - * Boolean Expressions [§S-S-D-V-E-BE] - * Literals [§S-S-D-V-E-L] - * Variables [§S-S-D-V-E-V] - * Message Aggregates [§S-S-D-V-E-MA] - * Aggregates [§S-S-D-V-E-A] - * Valid Attributes [§S-S-D-V-E-VAT] - * Opaque Attributes [§S-S-D-V-E-OAT] - * Size Attributes [§S-S-D-V-E-SAT] - * Head Attributes [§S-S-D-V-E-HAT] - * Has_Data Attributes [§S-S-D-V-E-HDAT] - * Selected Expressions [§S-S-D-V-E-S] - * List Comprehensions [§S-S-D-V-E-LC] - * Quantified Expressions [§S-S-D-V-E-Q] - * Calls [§S-S-D-V-E-CL] - * Conversions [§S-S-D-V-E-CV] - - **Dynamic Semantics** After entering a state the declarations and actions of the state are executed. @@ -991,9 +811,6 @@ If no condition could be fulfilled or no conditional transitions were defined, t State Transitions ^^^^^^^^^^^^^^^^^ -.. - State Transitions [§S-S-T] - State transitions define the conditions for the change to subsequent states. An arbitrary number of conditional transitions can be defined. The last transition in a state definition is the default transition, which does not contain any condition. @@ -1008,28 +825,6 @@ The transition target must be either a state name or `null`, which represents th transition: "goto" state_`name` : [ "with" `description_aspect` ] -.. - Condition expressions: - - * No condition [§S-S-T-N] - * Mathematical Expressions [§S-S-T-ME] - * Boolean Expressions [§S-S-T-BE] - * Literals [§S-S-T-L] - * Variables [§S-S-T-V] - * Message Aggregates [§S-S-T-MA] - * Aggregates [§S-S-T-A] - * Valid Attributes [§S-S-T-VAT] - * Opaque Attributes [§S-S-T-OAT] - * Size Attributes [§S-S-T-SAT] - * Head Attributes [§S-S-T-HAT] - * Has_Data Attributes [§S-S-T-HDAT] - * Field Valid Attributes [§S-S-T-FVAT] - * Selected Expressions [§S-S-T-S] - * List Comprehensions [§S-S-T-LC] - * Quantified Expressions [§S-S-T-Q] - * Calls [§S-S-T-CL] - * Conversions [§S-S-T-CV] - **Example** .. doc-check: rflx,conditional_transition,9 @@ -1042,9 +837,6 @@ The transition target must be either a state name or `null`, which represents th State Actions ^^^^^^^^^^^^^ -.. - State Actions [§S-S-A] - The state actions are executed after entering a state. **Syntax** @@ -1062,9 +854,6 @@ The state actions are executed after entering a state. Assignment Statements """"""""""""""""""""" -.. - Assignment Statements [§S-S-A-A] - An assignment sets the value of variable. **Syntax** @@ -1072,26 +861,6 @@ An assignment sets the value of variable. .. productionlist:: assignment: variable_`name` ":=" `expression` -.. - Expressions: - - * Mathematical Expressions [§S-S-A-A-ME] - * Boolean Expressions [§S-S-A-A-BE] - * Literals [§S-S-A-A-L] - * Variables [§S-S-A-A-V] - * Message Aggregates [§S-S-A-A-MA] - * Aggregates [§S-S-A-A-A] - * Valid Attributes [§S-S-A-A-VAT] - * Opaque Attributes [§S-S-A-A-OAT] - * Size Attributes [§S-S-A-A-SAT] - * Head Attributes [§S-S-A-A-HAT] - * Has_Data Attributes [§S-S-A-A-HDAT] - * Selected Expressions [§S-S-A-A-S] - * List Comprehensions [§S-S-A-A-LC] - * Quantified Expressions [§S-S-A-A-Q] - * Calls [§S-S-A-A-CL] - * Conversions [§S-S-A-A-CV] - **Dynamic Semantics** An assignment always creates a copy of the original object. @@ -1106,9 +875,6 @@ An assignment always creates a copy of the original object. Message Field Assignment Statements """"""""""""""""""""""""""""""""""" -.. - Message Field Assignment Statements [§S-S-A-MFA] - A message field assignment sets the value of a message field. **Syntax** @@ -1117,26 +883,6 @@ A message field assignment sets the value of a message field. message_field_assignment: variable_`name` "." field_`name` : ":=" `expression` -.. - Expressions: - - * Mathematical Expressions [§S-S-A-MFA-ME] - * Boolean Expressions [§S-S-A-MFA-BE] - * Literals [§S-S-A-MFA-L] - * Variables [§S-S-A-MFA-V] - * Message Aggregates [§S-S-A-MFA-MA] - * Aggregates [§S-S-A-MFA-A] - * Valid Attributes [§S-S-A-MFA-VAT] - * Opaque Attributes [§S-S-A-MFA-OAT] - * Size Attributes [§S-S-A-MFA-SAT] - * Head Attributes [§S-S-A-MFA-HAT] - * Has_Data Attributes [§S-S-A-MFA-HDAT] - * Selected Expressions [§S-S-A-MFA-S] - * List Comprehensions [§S-S-A-MFA-LC] - * Quantified Expressions [§S-S-A-MFA-Q] - * Calls [§S-S-A-MFA-CL] - * Conversions [§S-S-A-MFA-CV] - **Dynamic Semantics** Message fields must be set in order. @@ -1153,9 +899,6 @@ All subsequent fields of the set message field are invalidated. Append Attribute Statements """"""""""""""""""""""""""" -.. - Append Attribute Statements [§S-S-A-AP] - An element is added to the end of a sequence using the Append attribute. **Syntax** @@ -1163,26 +906,6 @@ An element is added to the end of a sequence using the Append attribute. .. productionlist:: append: sequence_`name` "'" "Append" "(" `expression` ")" -.. - Expressions: - - * Mathematical Expressions [§S-S-A-AP-ME] - * Boolean Expressions [§S-S-A-AP-BE] - * Literals [§S-S-A-AP-L] - * Variables [§S-S-A-AP-V] - * Message Aggregates [§S-S-A-AP-MA] - * Aggregates [§S-S-A-AP-A] - * Valid Attributes [§S-S-A-AP-VAT] - * Opaque Attributes [§S-S-A-AP-OAT] - * Size Attributes [§S-S-AP-SAT] - * Head Attributes [§S-S-A-AP-HAT] - * Has_Data Attributes [§S-S-A-AP-HDAT] - * Selected Expressions [§S-S-A-AP-S] - * List Comprehensions [§S-S-A-AP-LC] - * Quantified Expressions [§S-S-A-AP-Q] - * Calls [§S-S-A-AP-CL] - * Conversions [§S-S-A-AP-CV] - **Dynamic Semantics** Appending an element to a sequence might lead to an exception transition. @@ -1197,9 +920,6 @@ Appending an element to a sequence might lead to an exception transition. Extend Attribute Statements """"""""""""""""""""""""""" -.. - Extend Attribute Statements [§S-S-A-EX] - The Extend attributes adds a sequence of elements to the end of a sequence. **Syntax** @@ -1207,26 +927,6 @@ The Extend attributes adds a sequence of elements to the end of a sequence. .. productionlist:: extend: sequence_`name` "'" "Extend" "(" `expression` ")" -.. - Expressions: - - * Mathematical Expressions [§S-S-A-EX-ME] - * Boolean Expressions [§S-S-A-EX-BE] - * Literals [§S-S-A-EX-L] - * Variables [§S-S-A-EX-V] - * Message Aggregates [§S-S-A-EX-MA] - * Aggregates [§S-S-A-EX-A] - * Valid Attributes [§S-S-A-EX-VAT] - * Opaque Attributes [§S-S-A-EX-OAT] - * Size Attributes [§S-S-A-EX-SAT] - * Head Attributes [§S-S-A-EX-HAT] - * Has_Data Attributes [§S-S-A-EX-HDAT] - * Selected Expressions [§S-S-A-EX-S] - * List Comprehensions [§S-S-A-EX-LC] - * Quantified Expressions [§S-S-A-EX-Q] - * Calls [§S-S-A-EX-CL] - * Conversions [§S-S-A-EX-CV] - **Dynamic Semantics** Extending a sequence might lead to an exception transition. @@ -1241,9 +941,6 @@ Extending a sequence might lead to an exception transition. Reset Attribute Statements """""""""""""""""""""""""" -.. - Reset Attribute Statements [§S-S-A-RS] - The state of a message or sequence can be cleared using the Reset attribute. **Syntax** @@ -1251,26 +948,6 @@ The state of a message or sequence can be cleared using the Reset attribute. .. productionlist:: reset: `name` "'" "Reset" [ "(" `named_argument_list` ")" ] -.. - Expressions: - - * Mathematical Expressions [§S-S-A-RS-ME] - * Boolean Expressions [§S-S-A-RS-BE] - * Literals [§S-S-A-RS-L] - * Variables [§S-S-A-RS-V] - * Message Aggregates [§S-S-A-RS-MA] - * Aggregates [§S-S-A-RS-A] - * Valid Attributes [§S-S-A-RS-VAT] - * Opaque Attributes [§S-S-A-RS-OAT] - * Size Attributes [§S-S-A-RS-SAT] - * Head Attributes [§S-S-A-RS-HAT] - * Has_Data Attributes [§S-S-A-RS-HDAT] - * Selected Expressions [§S-S-A-RS-S] - * List Comprehensions [§S-S-A-RS-LC] - * Quantified Expressions [§S-S-A-RS-Q] - * Calls [§S-S-A-RS-CL] - * Conversions [§S-S-A-RS-CV] - **Static Semantics** When resetting a parameterized message, the intended values for the parameters of the message must be defined. @@ -1289,9 +966,6 @@ The existing state of a message or sequence is removed (and the corresponding bu Read Attribute Statements """"""""""""""""""""""""" -.. - Read Attribute Statements [§S-S-A-RD] - The read attribute statement is used to retrieve a message from a channel. **Syntax** @@ -1299,26 +973,6 @@ The read attribute statement is used to retrieve a message from a channel. .. productionlist:: read: channel_`name` "'" "Read" "(" `expression` ")" -.. - Expressions: - - * Mathematical Expressions [§S-S-A-RD-ME] - * Boolean Expressions [§S-S-A-RD-BE] - * Literals [§S-S-A-RD-L] - * Variables [§S-S-A-RD-V] - * Message Aggregates [§S-S-A-RD-MA] - * Aggregates [§S-S-A-RD-A] - * Valid Attributes [§S-S-A-RD-VAT] - * Opaque Attributes [§S-S-A-RD-OAT] - * Size Attributes [§S-S-A-RD-SAT] - * Head Attributes [§S-S-A-RD-HAT] - * Has_Data Attributes [§S-S-A-RD-HDAT] - * Selected Expressions [§S-S-A-RD-S] - * List Comprehensions [§S-S-A-RD-LC] - * Quantified Expressions [§S-S-A-RD-Q] - * Calls [§S-S-A-RD-CL] - * Conversions [§S-S-A-RD-CV] - **Example** .. doc-check: rflx,attribute_statement @@ -1329,9 +983,6 @@ The read attribute statement is used to retrieve a message from a channel. Write Attribute Statements """""""""""""""""""""""""" -.. - Write Attribute Statements [§S-S-A-WR] - A message can be sent through a channel using a write attribute statement. **Syntax** @@ -1339,26 +990,6 @@ A message can be sent through a channel using a write attribute statement. .. productionlist:: write: channel_`name` "'" "Write" "(" `expression` ")" -.. - Expressions: - - * Mathematical Expressions [§S-S-A-WR-ME] - * Boolean Expressions [§S-S-A-WR-BE] - * Literals [§S-S-A-WR-L] - * Variables [§S-S-A-WR-V] - * Message Aggregates [§S-S-A-WR-MA] - * Aggregates [§S-S-A-WR-A] - * Valid Attributes [§S-S-A-WR-VAT] - * Opaque Attributes [§S-S-A-WR-OAT] - * Size Attributes [§S-S-A-WR-SAT] - * Head Attributes [§S-S-A-WR-HAT] - * Has_Data Attributes [§S-S-A-WR-HDAT] - * Selected Expressions [§S-S-A-WR-S] - * List Comprehensions [§S-S-A-WR-LC] - * Quantified Expressions [§S-S-A-WR-Q] - * Calls [§S-S-A-WR-CL] - * Conversions [§S-S-A-WR-CV] - **Dynamic Semantics** Writing an invalid message leads to an exception transition. @@ -1373,9 +1004,6 @@ Writing an invalid message leads to an exception transition. Expressions ----------- -.. - Expressions [§S-E] - **Syntax** .. productionlist:: @@ -1428,9 +1056,6 @@ Insufficient memory during the message creation leads to an exception transition Aggregates ^^^^^^^^^^ -.. - Aggregates [§S-E-A] - An aggregate is a collection of elements. **Syntax** @@ -1438,32 +1063,6 @@ An aggregate is a collection of elements. .. productionlist:: aggregate: "[" [ `number` { "," `number` } ] "]" -.. - Types [§S-E-A-T]: - - * Scalar [§S-E-A-T-SC] - * Message [§S-E-A-T-M] - * Opaque [§S-E-A-T-O] - - Expressions [§S-E-A-E]: - - * Mathematical Expressions [§S-E-A-E-ME] - * Boolean Expressions [§S-E-A-E-BE] - * Literals [§S-E-A-E-L] - * Variables [§S-E-A-E-V] - * Message Aggregates [§S-E-A-E-MA] - * Aggregates [§S-E-A-E-A] - * Valid Attributes [§S-E-A-E-VAT] - * Opaque Attributes [§S-E-A-E-OAT] - * Size Attributes [§S-E-A-E-SAT] - * Head Attributes [§S-E-A-E-HAT] - * Has_Data Attributes [§S-E-A-E-HDAT] - * Selected Expressions [§S-E-A-E-S] - * List Comprehensions [§S-E-A-E-LC] - * Quantified Expressions [§S-E-A-E-Q] - * Calls [§S-E-A-E-CL] - * Conversions [§S-E-A-E-CV] - **Example** .. doc-check: rflx,extended_primary @@ -1479,9 +1078,6 @@ An aggregate is a collection of elements. Attribute Expressions ^^^^^^^^^^^^^^^^^^^^^ -.. - Attribute Expressions [§S-E-AT] - **Syntax** .. productionlist:: @@ -1493,56 +1089,8 @@ Attribute Expressions The byte representation of a message can be retrieved using the Opaque attribute. -.. - Opaque attribute [§S-E-AT-O] - - Expressions: - - * Mathematical Expressions [§S-E-AT-O-ME] - * Boolean Expressions [§S-E-AT-O-BE] - * Literals [§S-E-AT-O-L] - * Variables [§S-E-AT-O-V] - * Message Aggregates [§S-E-AT-O-MA] - * Aggregates [§S-E-AT-O-A] - * Valid Attributes [§S-E-AT-O-VAT] - * Opaque Attributes [§S-E-AT-O-OAT] - * Head Attributes [§S-E-AT-O-HAT] - * Has_Data Attributes [§S-E-AT-O-HDAT] - * Selected Expressions [§S-E-AT-O-S] - * List Comprehensions [§S-E-AT-O-LC] - * Quantified Expressions [§S-E-AT-O-Q] - * Calls [§S-E-AT-O-CL] - * Conversions [§S-E-AT-O-CV] - The Head attribute returns the first element of a sequence. -.. - Head attribute [§S-E-AT-H] - - Prefix types: - - * Scalar Sequence [§S-E-AT-H-SS] - * Message Sequence [§S-E-AT-H-MS] - - Expressions: - - * Mathematical Expressions [§S-E-AT-H-ME] - * Boolean Expressions [§S-E-AT-H-BE] - * Literals [§S-E-AT-H-L] - * Variables [§S-E-AT-H-V] - * Message Aggregates [§S-E-AT-H-MA] - * Aggregates [§S-E-AT-H-A] - * Valid Attributes [§S-E-AT-H-VAT] - * Opaque Attributes [§S-E-AT-H-OAT] - * Size Attributes [§S-E-AT-H-SAT] - * Head Attributes [§S-E-AT-H-HAT] - * Has_Data Attributes [§S-E-AT-H-HDAT] - * Selected Expressions [§S-E-AT-H-S] - * List Comprehensions [§S-E-AT-H-LC] - * Quantified Expressions [§S-E-AT-H-Q] - * Calls [§S-E-AT-H-CL] - * Conversions [§S-E-AT-H-CV] - **Dynamic Semantics** The use of the Opaque attribute on an invalid message or the use of the Head attribute on an empty sequence leads to an exception transition. @@ -1557,9 +1105,6 @@ The use of the Opaque attribute on an invalid message or the use of the Head att Selected Expressions ^^^^^^^^^^^^^^^^^^^^ -.. - Selected Expressions [§S-E-S] - The Selected expression is used to get a value of a message field. **Syntax** @@ -1567,26 +1112,6 @@ The Selected expression is used to get a value of a message field. .. productionlist:: selected: message_`expression` "." field_`name` -.. - Expressions: - - * Mathematical Expressions [§S-E-S-ME] - * Boolean Expressions [§S-E-S-BE] - * Literals [§S-E-S-L] - * Variables [§S-E-S-V] - * Message Aggregates [§S-E-S-MA] - * Aggregates [§S-E-S-A] - * Valid Attributes [§S-E-S-VAT] - * Opaque Attributes [§S-E-S-OAT] - * Size Attributes [§S-E-S-SAT] - * Head Attributes [§S-E-S-HAT] - * Has_Data Attributes [§S-E-S-HDAT] - * Selected Expressions [§S-E-S-S] - * List Comprehensions [§S-E-S-LC] - * Quantified Expressions [§S-E-S-Q] - * Calls [§S-E-S-CL] - * Conversions [§S-E-S-CV] - **Dynamic Semantics** Accesses to message fields that were detected as invalid during parsing lead to an exception transition. @@ -1601,9 +1126,6 @@ Accesses to message fields that were detected as invalid during parsing lead to List Comprehensions ^^^^^^^^^^^^^^^^^^^ -.. - List Comprehensions [§S-E-LC] - A list comprehension provides a way to create a new sequence based on an existing sequence. **Syntax** @@ -1615,20 +1137,6 @@ A list comprehension provides a way to create a new sequence based on an existin : "=>" selector_`expression` : "]" -.. - * Source: Scalar sequence [§S-E-LC-SSS] - * Source: Message sequence [§S-E-LC-SMS] - * Source: Variable [§S-E-LC-V] - * Source: Selected [§S-E-LC-S] - * Target: Scalar sequence [§S-E-LC-TSS] - * Target: Message sequence [§S-E-LC-TMS] - * Condition: Selected [§S-E-LC-CS] - * Source sequence as target [§S-E-LC-SAT] - * Global declarations [§S-E-LC-GD] - * Local declarations [§S-E-LC-LD] - * State transitions [§S-E-LC-T] - * Assignment statements [§S-E-LC-A] - **Dynamic Semantics** An access to an invalid element in iterable `expression <#grammar-token-expression>`_ leads to an exception transition. @@ -1643,9 +1151,6 @@ An access to an invalid element in iterable `expression <#grammar-token-expressi Quantified Expressions ^^^^^^^^^^^^^^^^^^^^^^ -.. - Quantified Expressions [§S-E-Q] - Quantified expressions enable reasoning about properties of sequences. **Syntax** @@ -1657,45 +1162,6 @@ Quantified expressions enable reasoning about properties of sequences. : predicate_`ext_bool_expression` quantifier: "all" | "some" -.. - Iterable expressions [§S-E-Q-I]: - - * Mathematical Expressions [§S-E-Q-I-ME] - * Boolean Expressions [§S-E-Q-I-BE] - * Literals [§S-E-Q-I-L] - * Variables [§S-E-Q-I-V] - * Message Aggregates [§S-E-Q-I-MA] - * Aggregates [§S-E-Q-I-A] - * Valid Attributes [§S-E-Q-I-VAT] - * Opaque Attributes [§S-E-Q-I-OAT] - * Size Attributes [§S-E-Q-I-SAT] - * Head Attributes [§S-E-Q-I-HAT] - * Has_Data Attributes [§S-E-Q-I-HDAT] - * Selected Expressions [§S-E-Q-I-S] - * List Comprehensions [§S-E-Q-I-LC] - * Quantified Expressions [§S-E-Q-I-Q] - * Calls [§S-E-Q-I-CL] - * Conversions [§S-E-Q-I-CV] - - Predicate expressions [§S-E-Q-P]: - - * Mathematical Expressions [§S-E-Q-P-ME] - * Boolean Expressions [§S-E-Q-P-BE] - * Literals [§S-E-Q-P-L] - * Variables [§S-E-Q-P-V] - * Message Aggregates [§S-E-Q-P-MA] - * Aggregates [§S-E-Q-P-A] - * Valid Attributes [§S-E-Q-P-VAT] - * Opaque Attributes [§S-E-Q-P-OAT] - * Size Attributes [§S-E-Q-P-SAT] - * Head Attributes [§S-E-Q-P-HAT] - * Has_Data Attributes [§S-E-Q-P-HDAT] - * Selected Expressions [§S-E-Q-P-S] - * List Comprehensions [§S-E-Q-P-LC] - * Quantified Expressions [§S-E-Q-P-Q] - * Calls [§S-E-Q-P-CL] - * Conversions [§S-E-Q-P-CV] - **Example** .. doc-check: rflx,extended_primary @@ -1706,9 +1172,6 @@ Quantified expressions enable reasoning about properties of sequences. Calls ^^^^^ -.. - Calls [§S-E-CL] - All functions which are declared in the state machine parameters can be called. **Syntax** @@ -1718,27 +1181,6 @@ All functions which are declared in the state machine parameters can be called. : [ "(" argument_`expression` : { "," argument_`expression` } ")" ] -.. - Argument expressions: - - * No argument [§S-E-CL-N] - * Mathematical Expressions [§S-E-CL-ME] - * Boolean Expressions [§S-E-CL-BE] - * Literals [§S-E-CL-L] - * Variables [§S-E-CL-V] - * Message Aggregates [§S-E-CL-MA] - * Aggregates [§S-E-CL-A] - * Valid Attributes [§S-E-CL-VAT] - * Opaque Attributes [§S-E-CL-OAT] - * Size Attributes [§S-E-CL-SAT] - * Head Attributes [§S-E-CL-HAT] - * Has_Data Attributes [§S-E-CL-HDAT] - * Selected Expressions [§S-E-CL-S] - * List Comprehensions [§S-E-CL-LC] - * Quantified Expressions [§S-E-CL-Q] - * Calls [§S-E-CL-CL] - * Conversions [§S-E-CL-CV] - **Example** .. doc-check: rflx,extended_primary @@ -1749,9 +1191,6 @@ All functions which are declared in the state machine parameters can be called. Conversions ^^^^^^^^^^^ -.. - Conversions [§S-E-CV] - An opaque field of a message can be converted to a message. **Syntax** @@ -1764,26 +1203,6 @@ An opaque field of a message can be converted to a message. A conversion is only allowed if a refinement for the message field and the intended target type exists. -.. - Expressions: - - * Mathematical Expressions [§S-E-CV-ME] - * Boolean Expressions [§S-E-CV-BE] - * Literals [§S-E-CV-L] - * Variables [§S-E-CV-V] - * Message Aggregates [§S-E-CV-MA] - * Aggregates [§S-E-CV-A] - * Valid Attributes [§S-E-CV-VAT] - * Opaque Attributes [§S-E-CV-OAT] - * Size Attributes [§S-E-CV-SAT] - * Head Attributes [§S-E-CV-HAT] - * Has_Data Attributes [§S-E-CV-HDAT] - * Selected Expressions [§S-E-CV-S] - * List Comprehensions [§S-E-CV-LC] - * Quantified Expressions [§S-E-CV-Q] - * Calls [§S-E-CV-CL] - * Conversions [§S-E-CV-CV] - **Dynamic Semantics** An invalid condition of a refinement leads to an exception transition. @@ -1798,9 +1217,6 @@ An invalid condition of a refinement leads to an exception transition. Case Expressions ^^^^^^^^^^^^^^^^ -.. - Case Expressions [§S-E-CE] - A `case expression <#grammar-token-case_expression>`_ selects one of several alternative dependent `expressions <#grammar-token-expression>`_ for evaluation based on the value of a selecting `expression <#grammar-token-expression>`_. **Syntax** diff --git a/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb index fbc1d9a98..5baf04037 100644 --- a/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_append_unconstrained/generated/rflx-test-s-fsm.adb @@ -82,7 +82,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_append_unconstrained/test.rflx:14:10 + -- tests/feature/fsm_append_unconstrained/test.rflx:13:10 if not Universal.Options.Has_Element (Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -185,7 +185,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_append_unconstrained/test.rflx:16:10 + -- tests/feature/fsm_append_unconstrained/test.rflx:14:10 if not Universal.Options.Has_Element (Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -288,7 +288,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_append_unconstrained/test.rflx:18:10 + -- tests/feature/fsm_append_unconstrained/test.rflx:15:10 if not Universal.Options.Has_Element (Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -319,7 +319,7 @@ is Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); end; - -- tests/feature/fsm_append_unconstrained/test.rflx:20:10 + -- tests/feature/fsm_append_unconstrained/test.rflx:16:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -381,7 +381,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_append_unconstrained/test.rflx:29:10 + -- tests/feature/fsm_append_unconstrained/test.rflx:25:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_append_unconstrained/test.rflx b/tests/feature/fsm_append_unconstrained/test.rflx index 95c5b4b3d..44eb186c0 100644 --- a/tests/feature/fsm_append_unconstrained/test.rflx +++ b/tests/feature/fsm_append_unconstrained/test.rflx @@ -3,32 +3,28 @@ with Universal; package Test is generic - Channel : Channel with Writable; -- §S-P-C-W + Channel : Channel with Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is - Options : Universal::Options; -- §S-S-D-V-T-MS, §S-S-D-V-E-N + Options : Universal::Options; begin - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 1, Data => [1])); - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [2, 3])); - -- §S-S-A-AP-MA Options'Append (Universal::Option'(Option_Type => Universal::OT_Null)); - -- §S-S-A-A-MA Message := Universal::Message'(Message_Type => Universal::MT_Unconstrained_Options, Options => Options); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Start; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb index f08e71ca6..373c91bde 100644 --- a/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_case_expression_aggregate/generated/rflx-test-s-fsm.adb @@ -81,7 +81,7 @@ is pragma Warnings (On, "condition can only be False if invalid values present"); -- tests/feature/fsm_case_expression_aggregate/test.rflx:24:10 Recv_Type := Universal.Message.Get_Message_Type (Ctx.P.Message_Ctx); - -- tests/feature/fsm_case_expression_aggregate/test.rflx:26:10 + -- tests/feature/fsm_case_expression_aggregate/test.rflx:25:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -165,7 +165,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_case_expression_aggregate/test.rflx:45:10 + -- tests/feature/fsm_case_expression_aggregate/test.rflx:44:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_case_expression_aggregate/test.rflx b/tests/feature/fsm_case_expression_aggregate/test.rflx index 23efd6efd..1893c93ea 100644 --- a/tests/feature/fsm_case_expression_aggregate/test.rflx +++ b/tests/feature/fsm_case_expression_aggregate/test.rflx @@ -3,29 +3,28 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Prepare - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - goto null -- §S-S-T-N + if Message'Valid + goto null exception - goto null -- §S-S-E + goto null end Start; state Prepare is - Recv_Type : Universal::Message_Type; -- §S-D-V-T-SC + Recv_Type : Universal::Message_Type; begin - Recv_Type := Message.Message_Type; -- §S-S-A-A-V - -- §S-S-A-A-MA + Recv_Type := Message.Message_Type; Message := Universal::Message'(Message_Type => Universal::MT_Value, Length => 1, - Value => -- §S-E-CE + Value => (case Recv_Type is when Universal::MT_Null | Universal::MT_Data => 2, when Universal::MT_Value => 4, @@ -35,16 +34,16 @@ package Test is when Universal::MT_Unconstrained_Data => 64, when Universal::MT_Unconstrained_Options => 128)); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Prepare; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_case_expression_numeric/test.rflx b/tests/feature/fsm_case_expression_numeric/test.rflx index 61c6ca416..ad9774079 100644 --- a/tests/feature/fsm_case_expression_numeric/test.rflx +++ b/tests/feature/fsm_case_expression_numeric/test.rflx @@ -10,41 +10,41 @@ package Test is end message; generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Prepare - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - goto null -- §S-S-T-N + if Message'Valid + goto null exception - goto null -- §S-S-E + goto null end Start; state Prepare is Value : Tiny_Int; begin - Value := (case Message.Value is -- §S-E-CE + Value := (case Message.Value is when 1 | 2 => 4, when 3 => 1, when 4 => 2); - -- §S-S-A-A-MA + Message := Message'(Value => Value); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Prepare; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_channel_multiplexing/test.rflx b/tests/feature/fsm_channel_multiplexing/test.rflx index 8e90128b6..c6381f24d 100644 --- a/tests/feature/fsm_channel_multiplexing/test.rflx +++ b/tests/feature/fsm_channel_multiplexing/test.rflx @@ -3,39 +3,39 @@ with Universal; package Test is generic - I_1 : Channel with Readable; -- §S-P-C-R - I_2 : Channel with Readable; -- §S-P-C-R - O : Channel with Writable; -- §S-P-C-W + I_1 : Channel with Readable; + I_2 : Channel with Readable; + O : Channel with Writable; machine S is - Message_1 : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - Message_2 : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message_1 : Universal::Message; + Message_2 : Universal::Message; begin state Start is begin - I_1'Read (Message_1); -- §S-S-A-RD-V - I_2'Read (Message_2); -- §S-S-A-RD-V + I_1'Read (Message_1); + I_2'Read (Message_2); transition goto Reply_1 - if Message_1'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V + if Message_1'Has_Data goto Reply_2 - if Message_2'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V - goto null -- §S-S-E + if Message_2'Has_Data + goto null exception - goto null -- §S-S-E + goto null end Start; state Reply_1 is begin - O'Write (Message_1); -- §S-S-A-WR-V + O'Write (Message_1); transition - goto Start -- §S-S-T-N + goto Start end Reply_1; state Reply_2 is begin - O'Write (Message_2); -- §S-S-A-WR-V + O'Write (Message_2); transition - goto Start -- §S-S-T-N + goto Start end Reply_2; end S; diff --git a/tests/feature/fsm_channels/test.rflx b/tests/feature/fsm_channels/test.rflx index b011dd606..152ea13c8 100644 --- a/tests/feature/fsm_channels/test.rflx +++ b/tests/feature/fsm_channels/test.rflx @@ -3,27 +3,27 @@ with Universal; package Test is generic - I : Channel with Readable; -- §S-P-C-RW - O : Channel with Writable; -- §S-P-C-RW + I : Channel with Readable; + O : Channel with Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - I'Read (Message); -- §S-S-A-RD-V + I'Read (Message); transition goto Reply - if Message'Has_Data -- §S-S-T-HDAT, §S-E-AT-HD-V - goto null -- §S-S-T-N + if Message'Has_Data + goto null exception - goto null -- §S-S-E + goto null end Start; state Reply is begin - O'Write (Message); -- §S-S-A-WR-V + O'Write (Message); transition - goto Start -- §S-S-T-N + goto Start end Reply; end S; diff --git a/tests/feature/fsm_comprehension_head/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_comprehension_head/generated/rflx-test-s-fsm.adb index 205f2080b..9ccf9aaa0 100644 --- a/tests/feature/fsm_comprehension_head/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_comprehension_head/generated/rflx-test-s-fsm.adb @@ -76,7 +76,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:15:10 + -- tests/feature/fsm_comprehension_head/test.rflx:14:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -179,7 +179,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:17:10 + -- tests/feature/fsm_comprehension_head/test.rflx:15:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -240,7 +240,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:19:10 + -- tests/feature/fsm_comprehension_head/test.rflx:16:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -339,7 +339,7 @@ is Ghost; begin pragma Assert (Process_1_Invariant); - -- tests/feature/fsm_comprehension_head/test.rflx:30:10 + -- tests/feature/fsm_comprehension_head/test.rflx:26:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_1_Invariant); @@ -384,7 +384,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_head/test.rflx:30:54 + -- tests/feature/fsm_comprehension_head/test.rflx:26:54 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -410,10 +410,10 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:30:54 + -- tests/feature/fsm_comprehension_head/test.rflx:26:54 T_0 := Universal.Option.Get_Option_Type (E_Ctx); if T_0 = (Known => True, Enum => Universal.OT_Data) then - -- tests/feature/fsm_comprehension_head/test.rflx:30:92 + -- tests/feature/fsm_comprehension_head/test.rflx:26:92 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -472,7 +472,7 @@ is Ctx.P.Slots.Slot_Ptr_4 := RFLX_Copy_Options_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); end; - -- tests/feature/fsm_comprehension_head/test.rflx:32:10 + -- tests/feature/fsm_comprehension_head/test.rflx:27:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_1_Invariant); @@ -519,7 +519,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_head/test.rflx:32:47 + -- tests/feature/fsm_comprehension_head/test.rflx:27:47 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -545,7 +545,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:32:47 + -- tests/feature/fsm_comprehension_head/test.rflx:27:47 T_1 := Universal.Option.Get_Option_Type (E_Ctx); if T_1 = (Known => True, Enum => Universal.OT_Data) then if not Universal.Option.Well_Formed_Message (E_Ctx) then @@ -669,7 +669,7 @@ is Ghost; begin pragma Assert (Send_1_Invariant); - -- tests/feature/fsm_comprehension_head/test.rflx:44:10 + -- tests/feature/fsm_comprehension_head/test.rflx:38:10 Ctx.P.Next_State := S_Recv; pragma Assert (Send_1_Invariant); end Send_1; @@ -692,7 +692,7 @@ is Ghost; begin pragma Assert (Recv_Invariant); - -- tests/feature/fsm_comprehension_head/test.rflx:52:10 + -- tests/feature/fsm_comprehension_head/test.rflx:45:10 Universal.Message.Verify_Message (Ctx.P.Message_Ctx); Ctx.P.Next_State := S_Process_2; pragma Assert (Recv_Invariant); @@ -717,7 +717,7 @@ is Ghost; begin pragma Assert (Process_2_Invariant); - -- tests/feature/fsm_comprehension_head/test.rflx:61:36 + -- tests/feature/fsm_comprehension_head/test.rflx:53:36 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -733,7 +733,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:61:10 + -- tests/feature/fsm_comprehension_head/test.rflx:53:10 if not Universal.Message.Well_Formed_Message (Ctx.P.Message_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_2_Invariant); @@ -789,7 +789,7 @@ is begin Universal.Options.Switch (RFLX_Message_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_head/test.rflx:61:55 + -- tests/feature/fsm_comprehension_head/test.rflx:53:55 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -815,7 +815,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_head/test.rflx:61:55 + -- tests/feature/fsm_comprehension_head/test.rflx:53:55 T_2 := Universal.Option.Get_Option_Type (E_Ctx); if T_2 = (Known => True, Enum => Universal.OT_Data) then if not Universal.Option.Well_Formed_Message (E_Ctx) then @@ -935,7 +935,7 @@ is Ghost; begin pragma Assert (Send_2_Invariant); - -- tests/feature/fsm_comprehension_head/test.rflx:72:10 + -- tests/feature/fsm_comprehension_head/test.rflx:63:10 Ctx.P.Next_State := S_Final; pragma Assert (Send_2_Invariant); end Send_2; diff --git a/tests/feature/fsm_comprehension_head/test.rflx b/tests/feature/fsm_comprehension_head/test.rflx index bcff6d0af..00ea8dea2 100644 --- a/tests/feature/fsm_comprehension_head/test.rflx +++ b/tests/feature/fsm_comprehension_head/test.rflx @@ -3,75 +3,66 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Options : Universal::Options; -- §S-D-V-T-MS, §S-D-V-E-N - First_Option : Universal::Option; -- §S-D-V-T-M, §S-D-V-E-N - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Options : Universal::Options; + First_Option : Universal::Option; + Message : Universal::Message; begin state Start is begin - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 1, Data => [2])); - -- §S-S-A-AP-MA Options'Append (Universal::Option'(Option_Type => Universal::OT_Null)); - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [2, 3])); transition - goto Process_1 -- §S-S-T-N + goto Process_1 exception - goto null -- §S-S-E + goto null end Start; state Process_1 is - First_Option_Length : Universal::Length; -- §S-S-D-V-T-SC, §S-S-D-V-E-H + First_Option_Length : Universal::Length; begin - -- §S-S-A-A-LC, §S-S-A-A-HAT, §S-E-AT-H-SS, §S-E-AT-H-LC, §S-E-S-LC, §S-E-S-BE, §S-E-LC-SSS, §S-E-LC-TSS First_Option_Length := [for E in Options if E.Option_Type = Universal::OT_Data => E.Length]'Head; - -- §S-S-A-A-LC, §S-S-A-A-HAT, §S-E-AT-H-MS, §S-E-AT-H-LC, §S-E-S-LC, §S-E-S-BE, §S-E-LC-SMS, §S-E-LC-TMS First_Option := [for E in Options if E.Option_Type = Universal::OT_Data => E]'Head; transition - goto Send_1 -- §S-S-T-BE + goto Send_1 if First_Option_Length > 0 - goto null -- §S-S-T-N + goto null exception - goto null -- §S-S-E + goto null end Process_1; state Send_1 is begin - -- §S-S-A-WR-V Channel'Write (First_Option); transition - goto Recv -- §S-S-T-N + goto Recv end Send_1; state Recv is begin - -- §S-S-A-RD-V Channel'Read (Message); transition - goto Process_2 -- §S-S-T-N + goto Process_2 end Recv; state Process_2 is begin - -- §S-S-A-A-LC, §S-S-A-A-HAT, §S-E-AT-H-MS, §S-E-AT-H-LC, §S-E-S-LC, §S-E-S-BE, §S-E-LC-S, §S-E-LC-TMS First_Option := [for E in Message.Options if E.Option_Type = Universal::OT_Data => E]'Head; transition - goto Send_2 -- §S-S-T-N + goto Send_2 exception - goto null -- §S-S-E + goto null end Process_2; state Send_2 is begin - -- §S-S-A-WR-V Channel'Write (First_Option); transition - goto null -- §S-S-T-N + goto null end Send_2; end S; diff --git a/tests/feature/fsm_comprehension_on_message_field/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_comprehension_on_message_field/generated/rflx-test-s-fsm.adb index e6dc81ca1..1747a9407 100644 --- a/tests/feature/fsm_comprehension_on_message_field/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_comprehension_on_message_field/generated/rflx-test-s-fsm.adb @@ -130,7 +130,7 @@ is pragma Warnings (On, "unused assignment"); Universal.Option_Types.Initialize (Option_Types_Ctx, Option_Types_Buffer); pragma Assert (Process_Invariant); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:26:36 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:25:36 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -146,7 +146,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:26:10 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:25:10 Universal.Option_Types.Reset (Option_Types_Ctx); if not Universal.Message.Well_Formed_Message (Ctx.P.Message_Ctx) then Ctx.P.Next_State := S_Final; @@ -201,7 +201,7 @@ is begin Universal.Options.Switch (RFLX_Message_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:26:55 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:25:55 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -227,10 +227,10 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:26:55 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:25:55 T_3 := Universal.Option.Get_Option_Type (E_Ctx); if T_3 = (Known => True, Enum => Universal.OT_Data) then - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:26:93 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:25:93 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -289,7 +289,7 @@ is Ctx.P.Slots.Slot_Ptr_3 := RFLX_Message_Options_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_3 /= null); end; - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:36 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:27:36 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -305,7 +305,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:10 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:27:10 Universal.Option_Types.Reset (Option_Types_Ctx); if not Universal.Message.Well_Formed_Message (Ctx.P.Message_Ctx) then Ctx.P.Next_State := S_Final; @@ -360,7 +360,7 @@ is begin Universal.Options.Switch (RFLX_Message_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:55 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:27:55 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -386,10 +386,10 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:55 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:27:55 T_4 := Universal.Option.Get_Option_Type (E_Ctx); if T_4 = (Known => True, Enum => Universal.OT_Data) then - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:93 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:27:93 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -478,7 +478,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:31:51 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:29:51 T_5 := RFLX.RFLX_Types.Base_Integer (Universal.Option_Types.Size (Option_Types_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -510,7 +510,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:31:71 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:29:71 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -526,7 +526,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:30:10 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:28:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -601,7 +601,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_comprehension_on_message_field/test.rflx:41:10 + -- tests/feature/fsm_comprehension_on_message_field/test.rflx:39:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_comprehension_on_message_field/test.rflx b/tests/feature/fsm_comprehension_on_message_field/test.rflx index 9e64cbde7..589e8f76d 100644 --- a/tests/feature/fsm_comprehension_on_message_field/test.rflx +++ b/tests/feature/fsm_comprehension_on_message_field/test.rflx @@ -3,44 +3,42 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - and Message.Message_Type = Universal::MT_Options -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid + and Message.Message_Type = Universal::MT_Options + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is - Option_Types : Universal::Option_Types; -- §S-S-D-V-T-SS, §S-S-D-V-E-N + Option_Types : Universal::Option_Types; begin - -- §S-S-A-A-LC, §S-E-LC-S, §S-E-LC-SMS, §S-E-LC-TSS, §S-E-LC-CS, §S-E-LC-A, §S-E-S-V Option_Types := [for E in Message.Options if E.Option_Type = Universal::OT_Data => E.Option_Type]; -- Test that target sequence is reset by assignment Option_Types := [for E in Message.Options if E.Option_Type = Universal::OT_Data => E.Option_Type]; - -- §S-S-A-A-MA Message := Universal::Message'(Message_Type => Universal::MT_Option_Types, Length => Option_Types'Size / 8, Option_Types => Option_Types); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm.adb index c54454b2f..c15925df0 100644 --- a/tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm.adb @@ -93,7 +93,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:15:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:14:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -196,7 +196,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:17:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:15:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -257,7 +257,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:19:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:16:10 if not Universal.Options.Has_Element (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Start_Invariant); @@ -384,7 +384,7 @@ is pragma Warnings (On, "unused assignment"); Universal.Options.Initialize (Message_Options_Ctx, Message_Options_Buffer); pragma Assert (Process_Invariant); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:27:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -430,7 +430,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:47 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:27:47 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -488,7 +488,7 @@ is Ctx.P.Slots.Slot_Ptr_6 := RFLX_Copy_Options_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_6 /= null); end; - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:31:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:28:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -534,7 +534,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:31:55 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:28:55 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -592,7 +592,7 @@ is Ctx.P.Slots.Slot_Ptr_7 := RFLX_Copy_Options_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_7 /= null); end; - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:32:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:29:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -638,7 +638,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:32:62 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:29:62 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -696,7 +696,7 @@ is Ctx.P.Slots.Slot_Ptr_8 := RFLX_Copy_Options_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_8 /= null); end; - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -742,7 +742,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:47 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:47 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -768,10 +768,10 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:47 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:47 T_0 := Universal.Option.Get_Option_Type (E_Ctx); if T_0 = (Known => True, Enum => Universal.OT_Data) then - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:85 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:30:85 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -860,7 +860,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:37:53 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:32:53 T_1 := RFLX.RFLX_Types.Base_Integer (Universal.Option_Types.Size (Option_Types_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -892,7 +892,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:37:73 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:32:73 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -908,7 +908,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:36:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:31:10 Universal.Message.Reset (Ctx.P.Message_1_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_1_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -953,7 +953,7 @@ is goto Finalize_Process; end if; Universal.Message.Set_Option_Types (Ctx.P.Message_1_Ctx, Option_Types_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:40:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:10 if not Universal.Options.Valid (Ctx.P.Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -999,7 +999,7 @@ is begin Universal.Options.Switch (RFLX_Copy_Options_Ctx, E_Ctx); Universal.Option.Verify_Message (E_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:40:50 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:50 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -1025,7 +1025,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:40:50 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:34:50 T_2 := Universal.Option.Get_Option_Type (E_Ctx); if T_2 = (Known => True, Enum => Universal.OT_Data) then if @@ -1121,7 +1121,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:43:53 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:36:53 T_3 := RFLX.RFLX_Types.Base_Integer (Universal.Options.Size (Message_Options_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -1153,7 +1153,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:43:76 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:36:76 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -1169,7 +1169,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:42:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:35:10 Universal.Message.Reset (Ctx.P.Message_2_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_2_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -1214,7 +1214,7 @@ is goto Finalize_Process; end if; Universal.Message.Set_Options (Ctx.P.Message_2_Ctx, Message_Options_Ctx); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:46:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:38:10 Universal.Options.Reset (Message_Options_Ctx); Ctx.P.Next_State := S_Send_1; pragma Assert (Process_Invariant); @@ -1259,7 +1259,7 @@ is Ghost; begin pragma Assert (Send_1_Invariant); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:56:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:47:10 Ctx.P.Next_State := S_Send_2; pragma Assert (Send_1_Invariant); end Send_1; @@ -1287,7 +1287,7 @@ is Ghost; begin pragma Assert (Send_2_Invariant); - -- tests/feature/fsm_comprehension_on_sequence/test.rflx:64:10 + -- tests/feature/fsm_comprehension_on_sequence/test.rflx:54:10 Ctx.P.Next_State := S_Final; pragma Assert (Send_2_Invariant); end Send_2; diff --git a/tests/feature/fsm_comprehension_on_sequence/test.rflx b/tests/feature/fsm_comprehension_on_sequence/test.rflx index 037d250c9..e87c8d9db 100644 --- a/tests/feature/fsm_comprehension_on_sequence/test.rflx +++ b/tests/feature/fsm_comprehension_on_sequence/test.rflx @@ -3,67 +3,57 @@ with Universal; package Test is generic - Channel : Channel with Writable; -- §S-P-C-W + Channel : Channel with Writable; machine S is - Options : Universal::Options; -- §S-D-V-T-MS, §S-D-V-E-N - Message_1 : Universal::Message; -- §S-S-D-V-T-M, §S-S-D-V-E-N - Message_2 : Universal::Message; -- §S-S-D-V-T-M, §S-S-D-V-E-N + Options : Universal::Options; + Message_1 : Universal::Message; + Message_2 : Universal::Message; begin state Start is begin - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 1, Data => [2])); - -- §S-S-A-AP-MA Options'Append (Universal::Option'(Option_Type => Universal::OT_Null)); - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [2, 3])); transition - goto Process -- §S-S-T-N + goto Process exception - goto null -- §S-S-E + goto null end Start; state Process is - Option_Types : Universal::Option_Types; -- §S-S-D-V-T-SS, §S-S-D-V-E-N - Message_Options : Universal::Options; -- §S-S-D-V-T-MS, §S-S-D-V-E-N + Option_Types : Universal::Option_Types; + Message_Options : Universal::Options; begin Option_Types := [for E in Options => E.Option_Type]; Option_Types := [for E in Options if True => E.Option_Type]; Option_Types := [for E in Options if True = True => E.Option_Type]; - -- §S-S-A-A-LC, §S-E-LC-V, §S-E-LC-SMS, §S-E-LC-TSS, §S-E-LC-CS, §S-E-LC-A, §S-E-S-V Option_Types := [for E in Options if E.Option_Type = Universal::OT_Data => E.Option_Type]; - -- §S-S-A-A-MA Message_1 := Universal::Message'(Message_Type => Universal::MT_Option_Types, Length => Option_Types'Size / 8, Option_Types => Option_Types); - -- §S-S-A-A-LC, §S-E-LC-V, §S-E-LC-SMS, §S-E-LC-TMS, §S-E-LC-CS, §S-E-LC-A, §S-E-S-V Message_Options := [for E in Options if E.Option_Type = Universal::OT_Data => E]; - -- §S-S-A-A-MA Message_2 := Universal::Message'(Message_Type => Universal::MT_Options, Length => Message_Options'Size / 8, Options => Message_Options); - -- §S-S-A-RS-V Message_Options'Reset; transition - goto Send_1 -- §S-S-T-N + goto Send_1 exception - goto null -- §S-S-E + goto null end Process; state Send_1 is begin - -- §S-S-A-WR-V Channel'Write (Message_1); transition - goto Send_2 -- §S-S-T-N + goto Send_2 end Send_1; state Send_2 is begin - -- §S-S-A-WR-V Channel'Write (Message_2); transition - goto null -- §S-S-T-N + goto null end Send_2; end S; diff --git a/tests/feature/fsm_conversion/test.rflx b/tests/feature/fsm_conversion/test.rflx index 80e0e9b6f..47e85fccb 100644 --- a/tests/feature/fsm_conversion/test.rflx +++ b/tests/feature/fsm_conversion/test.rflx @@ -3,37 +3,37 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - Inner_Message : Universal::Option; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; + Inner_Message : Universal::Option; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V - goto null -- §S-S-T-N + if Message'Valid + and Message.Message_Type = Universal::MT_Data + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is begin - Inner_Message := Universal::Option (Message.Data); -- §S-S-A-A-CV, §S-E-CV-V, §S-E-S-V + Inner_Message := Universal::Option (Message.Data); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Inner_Message); -- §S-S-A-WR-V + Channel'Write (Inner_Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_endianness/test.rflx b/tests/feature/fsm_endianness/test.rflx index 525865afb..994b4a954 100644 --- a/tests/feature/fsm_endianness/test.rflx +++ b/tests/feature/fsm_endianness/test.rflx @@ -19,7 +19,7 @@ package Test is if In_Msg'Has_Data goto null exception - goto null -- §S-S-E + goto null end Start; state Copy is @@ -46,7 +46,7 @@ package Test is if In_Msg2'Has_Data goto null exception - goto null -- §S-S-E + goto null end Read2; state Copy2 is diff --git a/tests/feature/fsm_functions/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_functions/generated/rflx-test-s-fsm.adb index 8c2302a9d..c3aad455e 100644 --- a/tests/feature/fsm_functions/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_functions/generated/rflx-test-s-fsm.adb @@ -239,7 +239,7 @@ is pragma Warnings (On, "condition can only be False if invalid values present"); -- tests/feature/fsm_functions/test.rflx:58:10 Length := Test.Length (T_6) / T_7; - -- tests/feature/fsm_functions/test.rflx:60:68 + -- tests/feature/fsm_functions/test.rflx:59:68 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -255,7 +255,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions/test.rflx:60:10 + -- tests/feature/fsm_functions/test.rflx:59:10 declare Definite_Message : Test.Definite_Message.Structure; RFLX_Create_Message_Arg_2_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); @@ -314,7 +314,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_functions/test.rflx:71:10 + -- tests/feature/fsm_functions/test.rflx:70:10 Ctx.P.Next_State := S_Process_2; pragma Assert (Reply_Invariant); end Reply; @@ -366,7 +366,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions/test.rflx:79:20 + -- tests/feature/fsm_functions/test.rflx:78:20 T_8 := RFLX.RFLX_Types.Base_Integer (Universal.Message.Size (Ctx.P.Message_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -398,7 +398,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions/test.rflx:79:35 + -- tests/feature/fsm_functions/test.rflx:78:35 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -414,7 +414,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions/test.rflx:79:10 + -- tests/feature/fsm_functions/test.rflx:78:10 Length := Test.Length (T_8) / 8; pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -431,7 +431,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions/test.rflx:81:10 + -- tests/feature/fsm_functions/test.rflx:79:10 declare Definite_Message : Test.Definite_Message.Structure; RFLX_Create_Message_Arg_2_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); @@ -491,7 +491,7 @@ is Ghost; begin pragma Assert (Reply_2_Invariant); - -- tests/feature/fsm_functions/test.rflx:90:10 + -- tests/feature/fsm_functions/test.rflx:88:10 Ctx.P.Next_State := S_Process_3; pragma Assert (Reply_2_Invariant); end Reply_2; @@ -512,14 +512,14 @@ is Ghost; begin pragma Assert (Process_3_Invariant); - -- tests/feature/fsm_functions/test.rflx:99:10 + -- tests/feature/fsm_functions/test.rflx:96:10 Create_Message (Ctx.E, (Known => True, Enum => Universal.OT_Data), 2, (RFLX_Types.Byte'Val (3), RFLX_Types.Byte'Val (4)), Local_Message); if not Test.Definite_Message.Valid_Structure (Local_Message) then Ctx.P.Next_State := S_Final; pragma Assert (Process_3_Invariant); goto Finalize_Process_3; end if; - -- tests/feature/fsm_functions/test.rflx:101:10 + -- tests/feature/fsm_functions/test.rflx:97:10 if not Test.Definite_Message.Valid_Next (Ctx.P.Definite_Message_Ctx, Test.Definite_Message.F_Length) then Ctx.P.Next_State := S_Final; pragma Assert (Process_3_Invariant); @@ -588,7 +588,7 @@ is Ghost; begin pragma Assert (Reply_3_Invariant); - -- tests/feature/fsm_functions/test.rflx:112:10 + -- tests/feature/fsm_functions/test.rflx:107:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_3_Invariant); end Reply_3; diff --git a/tests/feature/fsm_functions/test.rflx b/tests/feature/fsm_functions/test.rflx index 9e91c6171..a0b591efd 100644 --- a/tests/feature/fsm_functions/test.rflx +++ b/tests/feature/fsm_functions/test.rflx @@ -15,103 +15,98 @@ package Test is end message; generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW - -- §S-P-F-R-S + Channel : Channel with Readable, Writable; + with function Get_Message_Type return Universal::Option_Type; - -- §S-P-F-P-S, §S-P-F-P-O, §S-P-F-R-M + with function Create_Message (Message_Type : Universal::Option_Type; Length : Length; Data : Opaque) return Definite_Message; - -- §S-P-F-P-S, §S-P-F-R-S + with function Valid_Message (Message_Type : Universal::Option_Type; Strict : Boolean) return Result; - -- §S-P-F-R-S + with function Byte_Size return Length; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - Definite_Message : Definite_Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; + Definite_Message : Definite_Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and Message.Length = 3 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid + and Message.Message_Type = Universal::MT_Data + and Message.Length = 3 + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is - Valid : Result; -- §S-S-D-V-T-SC - Message_Type : Universal::Option_Type; -- §S-S-D-V-T-SC, §S-S-D-V-E-N + Valid : Result; + Message_Type : Universal::Option_Type; Length : Length; begin - Message_Type := Get_Message_Type; -- §S-S-A-A-CL, §S-E-CL-N - Valid := Valid_Message (Message_Type, True); -- §S-S-A-A-CL, §S-E-CL-L - Length := Message.Data'Size / Byte_Size; -- §S-S-A-A-ME - -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S + Message_Type := Get_Message_Type; + Valid := Valid_Message (Message_Type, True); + Length := Message.Data'Size / Byte_Size; Definite_Message := Create_Message (Message_Type, Length, Message.Data); transition goto Reply - if Valid = M_Valid -- §S-S-T-BE - goto null -- §S-S-T-N + if Valid = M_Valid + goto null exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Definite_Message); -- §S-S-A-WR-V + Channel'Write (Definite_Message); transition - goto Process_2 -- §S-S-T-N + goto Process_2 end Reply; state Process_2 is Length : Length; begin - Length := Message'Size / 8; -- §S-S-A-A-ME - -- §S-S-A-A-CL, §S-E-CL-L, §S-E-CL-V, §S-E-CL-OAT + Length := Message'Size / 8; Definite_Message := Create_Message (Universal::OT_Data, Length, Message'Opaque); transition - goto Reply_2 -- §S-S-T-N + goto Reply_2 exception - goto null -- §S-S-E + goto null end Process_2; state Reply_2 is begin - Channel'Write (Definite_Message); -- §S-S-A-WR-V + Channel'Write (Definite_Message); transition - goto Process_3 -- §S-S-T-N + goto Process_3 end Reply_2; state Process_3 is Local_Message : Definite_Message; begin - -- §S-S-A-A-CL, §S-E-CL-L, §S-E-CL-A Local_Message := Create_Message (Universal::OT_Data, 2, [3, 4]); - -- §S-S-A-MFA-S Definite_Message.Length := Local_Message.Length; - -- §S-S-A-MFA-S Definite_Message.Data := Local_Message.Data; transition - goto Reply_3 -- §S-S-T-N + goto Reply_3 exception - goto null -- §S-S-E + goto null end Process_3; state Reply_3 is begin - Channel'Write (Definite_Message); -- §S-S-A-WR-V + Channel'Write (Definite_Message); transition - goto null -- §S-S-T-N + goto null end Reply_3; end S; diff --git a/tests/feature/fsm_functions_opaque/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_functions_opaque/generated/rflx-test-s-fsm.adb index f7de4e0fb..17dc9992e 100644 --- a/tests/feature/fsm_functions_opaque/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_functions_opaque/generated/rflx-test-s-fsm.adb @@ -77,7 +77,7 @@ is pragma Warnings (On, "unused assignment"); Universal.Message.Initialize (Message_Ctx, Message_Buffer); pragma Assert (Check_Message_Invariant); - -- tests/feature/fsm_functions_opaque/test.rflx:23:10 + -- tests/feature/fsm_functions_opaque/test.rflx:21:10 Universal.Message.Reset (Message_Ctx); if not Universal.Message.Sufficient_Space (Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Error; @@ -132,7 +132,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:25:10 + -- tests/feature/fsm_functions_opaque/test.rflx:22:10 declare RFLX_Check_Size_Arg_1_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); RFLX_Check_Size_Arg_1_Message_Length : constant RFLX_Types.Length := Universal.Message.Byte_Size (Message_Ctx); @@ -231,7 +231,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:39:10 + -- tests/feature/fsm_functions_opaque/test.rflx:35:10 if not Universal.Options.Has_Element (Message_Sequence_Ctx) then Ctx.P.Next_State := S_Error; pragma Assert (Check_Message_Sequence_Invariant); @@ -319,7 +319,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:41:10 + -- tests/feature/fsm_functions_opaque/test.rflx:36:10 declare RFLX_Check_Size_Arg_1_Message_Sequence : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); RFLX_Check_Size_Arg_1_Message_Sequence_Length : constant RFLX_Types.Length := Universal.Options.Byte_Size (Message_Sequence_Ctx); @@ -418,7 +418,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:55:10 + -- tests/feature/fsm_functions_opaque/test.rflx:49:10 if not Universal.Values.Has_Element (Scalar_Sequence_Ctx) or Universal.Values.Available_Space (Scalar_Sequence_Ctx) < Universal.Value'Size @@ -458,7 +458,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:57:10 + -- tests/feature/fsm_functions_opaque/test.rflx:50:10 if not Universal.Values.Has_Element (Scalar_Sequence_Ctx) or Universal.Values.Available_Space (Scalar_Sequence_Ctx) < Universal.Value'Size @@ -483,7 +483,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_functions_opaque/test.rflx:59:10 + -- tests/feature/fsm_functions_opaque/test.rflx:51:10 declare RFLX_Check_Size_Arg_1_Scalar_Sequence : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); RFLX_Check_Size_Arg_1_Scalar_Sequence_Length : constant RFLX_Types.Length := Universal.Values.Byte_Size (Scalar_Sequence_Ctx); diff --git a/tests/feature/fsm_functions_opaque/test.rflx b/tests/feature/fsm_functions_opaque/test.rflx index 8a372cd38..1e9f9a687 100644 --- a/tests/feature/fsm_functions_opaque/test.rflx +++ b/tests/feature/fsm_functions_opaque/test.rflx @@ -5,70 +5,62 @@ package Test is type Size is range 0 .. 2 ** 32 - 1 with Size => 32; generic - -- §S-P-F-P-S, §S-P-F-P-O, §S-P-F-R-S with function Check_Size (Size : Size; Data : Opaque) return Boolean; machine S is begin state Start is begin transition - goto Check_Message -- §S-S-T-N + goto Check_Message end Start; state Check_Message is - Valid : Boolean; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Message : Universal::Message; -- §S-S-D-V-T-M, §S-S-D-V-E-N + Valid : Boolean; + Message : Universal::Message; begin - -- §S-S-A-A-MA Message := Universal::Message'(Message_Type => Universal::MT_Data, Length => 2, Data => [3, 4]); - -- §S-S-A-A-CL, §S-E-CL-SAT, §S-E-CL-OAT Valid := Check_Size (Message'Size, Message'Opaque); transition goto Check_Message_Sequence - if Valid -- §S-S-T-V - goto Error -- §S-S-T-N + if Valid + goto Error exception - goto Error -- §S-S-E + goto Error end Check_Message; state Check_Message_Sequence is - Valid : Boolean; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Message_Sequence : Universal::Options; -- §S-S-D-V-T-MS, §S-S-D-V-E-N + Valid : Boolean; + Message_Sequence : Universal::Options; begin - -- §S-S-A-AP-MA Message_Sequence'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [3, 4])); - -- §S-S-A-A-CL, §S-E-CL-SAT, §S-E-CL-OAT Valid := Check_Size (Message_Sequence'Size, Message_Sequence'Opaque); transition goto Check_Scalar_Sequence - if Valid -- §S-S-T-V - goto Error -- §S-S-T-N + if Valid + goto Error exception - goto Error -- §S-S-E + goto Error end Check_Message_Sequence; state Check_Scalar_Sequence is - Valid : Boolean; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Scalar_Sequence : Universal::Values; -- §S-S-D-V-T-SS, §S-S-D-V-E-N + Valid : Boolean; + Scalar_Sequence : Universal::Values; begin - -- §S-S-A-AP-L Scalar_Sequence'Append (1); - -- §S-S-A-AP-L Scalar_Sequence'Append (2); - -- §S-S-A-A-CL, §S-E-CL-SAT, §S-E-CL-OAT Valid := Check_Size (Scalar_Sequence'Size, Scalar_Sequence'Opaque); transition goto null - if Valid -- §S-S-T-V - goto Error -- §S-S-T-N + if Valid + goto Error exception - goto Error -- §S-S-E + goto Error end Check_Scalar_Sequence; state Error is begin transition - goto null -- §S-S-T-N + goto null end Error; end S; diff --git a/tests/feature/fsm_integration/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_integration/generated/rflx-test-s-fsm.adb index 323b2d1f5..342baee9c 100644 --- a/tests/feature/fsm_integration/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_integration/generated/rflx-test-s-fsm.adb @@ -186,7 +186,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_integration/test.rflx:35:10 + -- tests/feature/fsm_integration/test.rflx:34:10 Ctx.P.Next_State := S_Next; pragma Assert (Reply_Invariant); end Reply; @@ -217,7 +217,7 @@ is pragma Warnings (On, "unused assignment"); Universal.Message.Initialize (M_Ctx, M_Buffer); pragma Assert (Next_Invariant); - -- tests/feature/fsm_integration/test.rflx:43:10 + -- tests/feature/fsm_integration/test.rflx:42:10 Universal.Message.Reset (M_Ctx); if not Universal.Message.Sufficient_Space (M_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; diff --git a/tests/feature/fsm_integration/test.rflx b/tests/feature/fsm_integration/test.rflx index 8e728fa57..2e5532b79 100644 --- a/tests/feature/fsm_integration/test.rflx +++ b/tests/feature/fsm_integration/test.rflx @@ -3,21 +3,21 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Prepare_Message - if Message'Valid = True -- §S-S-T-VAT, §S-E-AT-V-V, §S-S-T-L - and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and Message.Length = 1 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid = True + and Message.Message_Type = Universal::MT_Data + and Message.Length = 1 + goto null exception - goto null -- §S-S-E + goto null end Start; state Prepare_Message is @@ -26,15 +26,14 @@ package Test is transition goto Reply exception - goto null -- §S-S-E + goto null end Prepare_Message; state Reply is begin - -- §S-S-A-A-MA, §S-E-A-T-SC, §S-E-A-E-L - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto Next -- §S-S-T-N + goto Next end Reply; state Next is diff --git a/tests/feature/fsm_message_creation/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_message_creation/generated/rflx-test-s-fsm.adb index 156e8d07e..ddf35cdd9 100644 --- a/tests/feature/fsm_message_creation/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_message_creation/generated/rflx-test-s-fsm.adb @@ -181,7 +181,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_creation/test.rflx:31:24 + -- tests/feature/fsm_message_creation/test.rflx:30:24 T_11 := RFLX.RFLX_Types.Base_Integer (Universal.Message.Size (Ctx.P.M_R_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -213,7 +213,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_creation/test.rflx:31:35 + -- tests/feature/fsm_message_creation/test.rflx:30:35 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -244,7 +244,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_creation/test.rflx:29:10 + -- tests/feature/fsm_message_creation/test.rflx:28:10 Universal.Message.Reset (Ctx.P.M_S_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -323,7 +323,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_message_creation/test.rflx:41:10 + -- tests/feature/fsm_message_creation/test.rflx:40:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_message_creation/test.rflx b/tests/feature/fsm_message_creation/test.rflx index 06f1ba60e..48137872a 100644 --- a/tests/feature/fsm_message_creation/test.rflx +++ b/tests/feature/fsm_message_creation/test.rflx @@ -3,44 +3,43 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - M_R : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - M_S : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + M_R : Universal::Message; + M_S : Universal::Message; begin state Start is begin - Channel'Read (M_R); -- §S-S-A-RD-V + Channel'Read (M_R); transition goto Process - if M_R'Valid = True -- §S-S-T-VAT, §S-E-AT-V-V, §S-S-T-L - and M_R.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and M_R.Length = 2 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and M_R.Length'Valid -- §S-S-T-FVAT - and M_R.Data'Present -- §S-S-T-FPAT - goto null -- §S-S-T-N + if M_R'Valid = True + and M_R.Message_Type = Universal::MT_Data + and M_R.Length = 2 + and M_R.Length'Valid + and M_R.Data'Present + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is begin - -- §S-S-A-A-MA, §S-E-A-T-SC, §S-E-A-E-L M_S := Universal::Message' (Message_Type => Universal::MT_Data, Length => M_R'Size / 8, Data => M_R'Opaque); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (M_S); -- §S-S-A-WR-V + Channel'Write (M_S); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_message_optimization/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_message_optimization/generated/rflx-test-s-fsm.adb index f4f5efd0a..ded27306f 100644 --- a/tests/feature/fsm_message_optimization/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_message_optimization/generated/rflx-test-s-fsm.adb @@ -62,11 +62,11 @@ is Ghost; begin pragma Assert (Start_Invariant); - -- tests/feature/fsm_message_optimization/test.rflx:24:10 + -- tests/feature/fsm_message_optimization/test.rflx:23:10 Universal.Message.Verify_Message (Ctx.P.Message_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:27:16 + -- tests/feature/fsm_message_optimization/test.rflx:26:16 T_0 := Universal.Message.Well_Formed_Message (Ctx.P.Message_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:28:20 + -- tests/feature/fsm_message_optimization/test.rflx:27:20 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -82,14 +82,14 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:28:20 + -- tests/feature/fsm_message_optimization/test.rflx:27:20 T_1 := Universal.Message.Get_Message_Type (Ctx.P.Message_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:28:20 + -- tests/feature/fsm_message_optimization/test.rflx:27:20 T_2 := T_1 = Universal.MT_Data; - -- tests/feature/fsm_message_optimization/test.rflx:27:16 + -- tests/feature/fsm_message_optimization/test.rflx:26:16 T_3 := T_0 and then T_2; - -- tests/feature/fsm_message_optimization/test.rflx:29:20 + -- tests/feature/fsm_message_optimization/test.rflx:28:20 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -105,9 +105,9 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:29:20 + -- tests/feature/fsm_message_optimization/test.rflx:28:20 T_4 := Universal.Message.Get_Length (Ctx.P.Message_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:29:20 + -- tests/feature/fsm_message_optimization/test.rflx:28:20 T_5 := T_4 = 3; if T_3 @@ -154,9 +154,9 @@ is Ghost; begin pragma Assert (Process_Invariant); - -- tests/feature/fsm_message_optimization/test.rflx:41:10 + -- tests/feature/fsm_message_optimization/test.rflx:39:10 Option_Type := (Known => True, Enum => Universal.OT_Data); - -- tests/feature/fsm_message_optimization/test.rflx:43:42 + -- tests/feature/fsm_message_optimization/test.rflx:40:42 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -172,7 +172,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:43:10 + -- tests/feature/fsm_message_optimization/test.rflx:40:10 declare RFLX_Get_Option_Data_Arg_0_Message : RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Length'(4095)) := (others => 0); RFLX_Get_Option_Data_Arg_0_Message_Length : constant RFLX_Types.Length := RFLX_Types.To_Length (Universal.Message.Field_Size (Ctx.P.Message_Ctx, Universal.Message.F_Data)); @@ -200,11 +200,11 @@ is goto Finalize_Process; end if; end; - -- tests/feature/fsm_message_optimization/test.rflx:45:10 + -- tests/feature/fsm_message_optimization/test.rflx:41:10 Local_Length := Option_Data.Length; - -- tests/feature/fsm_message_optimization/test.rflx:47:10 + -- tests/feature/fsm_message_optimization/test.rflx:42:10 Universal.Option.Reset (Ctx.P.Option_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:49:10 + -- tests/feature/fsm_message_optimization/test.rflx:43:10 if not Universal.Option.Valid_Next (Ctx.P.Option_Ctx, Universal.Option.F_Option_Type) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -264,14 +264,14 @@ is end if; RFLX_Universal_Option_Set_Data (Ctx.P.Option_Ctx, RFLX_Types.To_Length (Test.Option_Data.Field_Size_Data (Option_Data))); end; - -- tests/feature/fsm_message_optimization/test.rflx:56:16 + -- tests/feature/fsm_message_optimization/test.rflx:48:16 T_6 := Local_Length > 0; - -- tests/feature/fsm_message_optimization/test.rflx:57:20 + -- tests/feature/fsm_message_optimization/test.rflx:49:20 T_7 := Option_Type /= (Known => True, Enum => Universal.OT_Null); - -- tests/feature/fsm_message_optimization/test.rflx:56:16 + -- tests/feature/fsm_message_optimization/test.rflx:48:16 T_8 := T_6 and then T_7; - -- tests/feature/fsm_message_optimization/test.rflx:58:34 + -- tests/feature/fsm_message_optimization/test.rflx:50:34 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -287,16 +287,16 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:58:34 + -- tests/feature/fsm_message_optimization/test.rflx:50:34 T_9 := Universal.Option.Get_Option_Type (Ctx.P.Option_Ctx); - -- tests/feature/fsm_message_optimization/test.rflx:58:20 + -- tests/feature/fsm_message_optimization/test.rflx:50:20 T_10 := Option_Type = T_9; - -- tests/feature/fsm_message_optimization/test.rflx:56:16 + -- tests/feature/fsm_message_optimization/test.rflx:48:16 T_11 := T_8 and then T_10; - -- tests/feature/fsm_message_optimization/test.rflx:59:20 + -- tests/feature/fsm_message_optimization/test.rflx:51:20 T_12 := Test.Option_Data.Valid_Structure (Option_Data); - -- tests/feature/fsm_message_optimization/test.rflx:56:16 + -- tests/feature/fsm_message_optimization/test.rflx:48:16 T_13 := T_11 and then T_12; pragma Warnings (Off, "condition can only be False if invalid values present"); @@ -329,13 +329,13 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:60:20 + -- tests/feature/fsm_message_optimization/test.rflx:52:20 T_14 := RFLX.RFLX_Types.Base_Integer (Test.Option_Data.Field_Size_Length (Option_Data)); - -- tests/feature/fsm_message_optimization/test.rflx:60:46 + -- tests/feature/fsm_message_optimization/test.rflx:52:46 T_15 := Universal.Length'Size; - -- tests/feature/fsm_message_optimization/test.rflx:60:20 + -- tests/feature/fsm_message_optimization/test.rflx:52:20 T_16 := T_14 = T_15; - -- tests/feature/fsm_message_optimization/test.rflx:56:16 + -- tests/feature/fsm_message_optimization/test.rflx:48:16 T_17 := T_13 and then T_16; pragma Warnings (Off, "condition can only be False if invalid values present"); @@ -383,7 +383,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:61:20 + -- tests/feature/fsm_message_optimization/test.rflx:53:20 T_18 := RFLX.RFLX_Types.Base_Integer (Universal.Option.Field_Size (Ctx.P.Option_Ctx, Universal.Option.F_Data)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -415,9 +415,9 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:61:39 + -- tests/feature/fsm_message_optimization/test.rflx:53:39 T_19 := RFLX.RFLX_Types.Base_Integer (Test.Option_Data.Field_Size_Data (Option_Data)); - -- tests/feature/fsm_message_optimization/test.rflx:61:20 + -- tests/feature/fsm_message_optimization/test.rflx:53:20 T_20 := T_18 = T_19; if T_17 @@ -446,7 +446,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_message_optimization/test.rflx:69:10 + -- tests/feature/fsm_message_optimization/test.rflx:61:10 Ctx.P.Next_State := S_Trigger_Error; pragma Assert (Reply_Invariant); end Reply; @@ -467,7 +467,7 @@ is Ghost; begin pragma Assert (Trigger_Error_Invariant); - -- tests/feature/fsm_message_optimization/test.rflx:78:10 + -- tests/feature/fsm_message_optimization/test.rflx:69:10 Get_Option_Data (Ctx.E, (RFLX_Types.Index'First => RFLX_Types.Byte'Val (0)), Null_Option_Data); if not Test.Option_Data.Valid_Structure (Null_Option_Data) then Ctx.P.Next_State := S_Error; @@ -504,7 +504,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_message_optimization/test.rflx:80:10 + -- tests/feature/fsm_message_optimization/test.rflx:70:10 if not Universal.Option.Valid_Next (Ctx.P.Option_Ctx, Universal.Option.F_Length) then Ctx.P.Next_State := S_Error; pragma Assert (Trigger_Error_Invariant); diff --git a/tests/feature/fsm_message_optimization/test.rflx b/tests/feature/fsm_message_optimization/test.rflx index 050fbc55c..e35952980 100644 --- a/tests/feature/fsm_message_optimization/test.rflx +++ b/tests/feature/fsm_message_optimization/test.rflx @@ -12,82 +12,72 @@ package Test is end message; generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW - -- §S-P-F-R-S + Channel : Channel with Readable, Writable; with function Get_Option_Data (Data : Opaque) return Option_Data; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - Option : Universal::Option; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; + Option : Universal::Option; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and Message.Length = 3 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid + and Message.Message_Type = Universal::MT_Data + and Message.Length = 3 + goto null exception - goto Error -- §S-S-E + goto Error end Start; state Process is - Option_Type : Universal::Option_Type; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Option_Data : Option_Data; -- §S-S-D-V-T-M, §S-S-D-V-E-N - Local_Length : Universal::Length; -- §S-S-D-V-T-SC, §S-S-D-V-E-N + Option_Type : Universal::Option_Type; + Option_Data : Option_Data; + Local_Length : Universal::Length; begin - -- §S-S-A-A-L Option_Type := Universal::OT_Data; - -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S Option_Data := Get_Option_Data (Message.Data); - -- §S-S-A-A-S Local_Length := Option_Data.Length; - -- §S-S-A-RS Option'Reset; - -- §S-S-A-MFA-L Option.Option_Type := Option_Type; - -- §S-S-A-MFA-S Option.Length := Option_Data.Length; - -- §S-S-A-MFA-S Option.Data := Option_Data.Data; transition goto Reply - if Local_Length > 0 -- §S-S-T-ME - and Option_Type /= Universal::OT_Null -- §S-S-T-ME, §S-S-T-V, §S-S-T-L - and Option_Type = Option.Option_Type -- §S-S-T-ME, §S-S-T-S, §S-S-T-L - and Option_Data'Valid -- §S-S-T-VAT - and Option_Data.Length'Size = Universal::Length'Size -- §S-S-T-ME, §S-S-T-S, §S-S-T-SAT - and Option.Data'Size = Option_Data.Data'Size -- §S-S-T-ME, §S-S-T-S, §S-S-T-SAT - goto null -- §S-S-T-N + if Local_Length > 0 + and Option_Type /= Universal::OT_Null + and Option_Type = Option.Option_Type + and Option_Data'Valid + and Option_Data.Length'Size = Universal::Length'Size + and Option.Data'Size = Option_Data.Data'Size + goto null exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Option); -- §S-S-A-WR-V + Channel'Write (Option); transition - goto Trigger_Error -- §S-S-T-N + goto Trigger_Error end Reply; state Trigger_Error is Null_Option_Data : Option_Data; begin - -- §S-S-A-A-CL, §S-E-CL-L Null_Option_Data := Get_Option_Data ([0]); - -- §S-S-A-MFA-S Option.Length := Null_Option_Data.Length; transition - goto null -- §S-S-T-N + goto null exception - goto Error -- §S-S-E + goto Error end Trigger_Error; state Error is begin transition - goto null -- §S-S-T-N + goto null end Error; end S; diff --git a/tests/feature/fsm_minimal/test.rflx b/tests/feature/fsm_minimal/test.rflx index 8f6be33e5..f4b144f7b 100644 --- a/tests/feature/fsm_minimal/test.rflx +++ b/tests/feature/fsm_minimal/test.rflx @@ -3,26 +3,26 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Reply - if Message'Valid -- §S-S-T-VAT, §S-E-AT-V-V - goto null -- §S-S-T-N + if Message'Valid + goto null exception - goto null -- §S-S-E + goto null end Start; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_reuse_of_message/test.rflx b/tests/feature/fsm_reuse_of_message/test.rflx index 05db7dd42..8388e26fb 100644 --- a/tests/feature/fsm_reuse_of_message/test.rflx +++ b/tests/feature/fsm_reuse_of_message/test.rflx @@ -3,24 +3,24 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Reply - if Message'Has_Data -- §S-S-T-HDAT, §S-E-AT-V-HDAT - goto null -- §S-S-T-N + if Message'Has_Data + goto null exception - goto null -- §S-S-E + goto null end Start; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition goto Start end Reply; diff --git a/tests/feature/fsm_sequence_append/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_sequence_append/generated/rflx-test-s-fsm.adb index 7864af38f..24a2f204d 100644 --- a/tests/feature/fsm_sequence_append/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_sequence_append/generated/rflx-test-s-fsm.adb @@ -117,7 +117,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:23:55 + -- tests/feature/fsm_sequence_append/test.rflx:22:55 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -133,7 +133,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:24:53 + -- tests/feature/fsm_sequence_append/test.rflx:23:53 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -149,7 +149,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:22:10 + -- tests/feature/fsm_sequence_append/test.rflx:21:10 if not Universal.Options.Has_Element (Options_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -268,7 +268,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:27:51 + -- tests/feature/fsm_sequence_append/test.rflx:25:51 T_0 := RFLX.RFLX_Types.Base_Integer (Universal.Options.Size (Options_Ctx)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -300,7 +300,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:27:66 + -- tests/feature/fsm_sequence_append/test.rflx:25:66 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -316,7 +316,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append/test.rflx:26:10 + -- tests/feature/fsm_sequence_append/test.rflx:24:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -394,7 +394,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_sequence_append/test.rflx:39:10 + -- tests/feature/fsm_sequence_append/test.rflx:37:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_sequence_append/test.rflx b/tests/feature/fsm_sequence_append/test.rflx index 525c8b9cf..4e2d0b5aa 100644 --- a/tests/feature/fsm_sequence_append/test.rflx +++ b/tests/feature/fsm_sequence_append/test.rflx @@ -3,42 +3,40 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Option : Universal::Option; -- §S-D-V-T-M, §S-D-V-E-N - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Option : Universal::Option; + Message : Universal::Message; begin state Start is begin - Channel'Read (Option); -- §S-S-A-RD-V + Channel'Read (Option); transition - goto Process -- §S-S-T-N + goto Process end Start; state Process is - Options : Universal::Options; -- §S-D-V-T-MS, §S-D-V-E-N + Options : Universal::Options; begin - -- §S-S-A-AP-MA Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => Option.Length, Data => Option.Data)); - -- §S-S-A-A-MA Message := Universal::Message'(Message_Type => Universal::MT_Options, Length => Options'Size / 8, Options => Options); transition goto Reply - if Options'Valid -- §S-S-T-VAT - goto null -- §S-S-T-N + if Options'Valid + goto null exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_sequence_append_head/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_sequence_append_head/generated/rflx-test-s-fsm.adb index 7508dc288..d94726d28 100644 --- a/tests/feature/fsm_sequence_append_head/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_sequence_append_head/generated/rflx-test-s-fsm.adb @@ -80,7 +80,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:17:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:16:10 if not TLV.Messages.Has_Element (Ctx.P.Messages_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Global_Invariant); @@ -183,7 +183,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:18:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:17:10 if not TLV.Tags.Has_Element (Ctx.P.Tags_Ctx) or TLV.Tags.Available_Space (Ctx.P.Tags_Ctx) < TLV.Tag'Size @@ -193,7 +193,7 @@ is goto Finalize_Global; end if; TLV.Tags.Append_Element (Ctx.P.Tags_Ctx, TLV.Msg_Error); - -- tests/feature/fsm_sequence_append_head/test.rflx:19:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:18:10 if not TLV.Messages.Valid (Ctx.P.Messages_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Global_Invariant); @@ -311,7 +311,7 @@ is Ctx.P.Slots.Slot_Ptr_4 := RFLX_Copy_Messages_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null); end; - -- tests/feature/fsm_sequence_append_head/test.rflx:20:25 + -- tests/feature/fsm_sequence_append_head/test.rflx:19:25 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -327,9 +327,9 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:20:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:19:10 Message_Tag := TLV.Message.Get_Tag (Ctx.P.Message_Ctx); - -- tests/feature/fsm_sequence_append_head/test.rflx:21:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:20:10 if not (TLV.Tags.Valid (Ctx.P.Tags_Ctx) and then TLV.Tags.Has_Element (Ctx.P.Tags_Ctx) @@ -340,9 +340,9 @@ is goto Finalize_Global; end if; Tag := TLV.Tags.Head (Ctx.P.Tags_Ctx); - -- tests/feature/fsm_sequence_append_head/test.rflx:24:16 + -- tests/feature/fsm_sequence_append_head/test.rflx:23:16 T_0 := Message_Tag = TLV.Msg_Data; - -- tests/feature/fsm_sequence_append_head/test.rflx:25:20 + -- tests/feature/fsm_sequence_append_head/test.rflx:24:20 T_1 := Tag = TLV.Msg_Error; if T_0 @@ -376,7 +376,7 @@ is Ghost; begin pragma Assert (Reply_1_Invariant); - -- tests/feature/fsm_sequence_append_head/test.rflx:33:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:32:10 Ctx.P.Next_State := S_Local; pragma Assert (Reply_1_Invariant); end Reply_1; @@ -457,7 +457,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:45:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:43:10 if not TLV.Messages.Has_Element (Local_Messages_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Local_Invariant); @@ -560,7 +560,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:47:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:44:10 if not TLV.Messages.Has_Element (Ctx.P.Messages_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Local_Invariant); @@ -663,7 +663,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:48:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:45:10 if not TLV.Tags.Has_Element (Local_Tags_Ctx) or TLV.Tags.Available_Space (Local_Tags_Ctx) < TLV.Tag'Size @@ -703,7 +703,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:49:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:46:10 if not TLV.Tags.Has_Element (Local_Tags_Ctx) or TLV.Tags.Available_Space (Local_Tags_Ctx) < TLV.Tag'Size @@ -713,7 +713,7 @@ is goto Finalize_Local; end if; TLV.Tags.Append_Element (Local_Tags_Ctx, TLV.Msg_Error); - -- tests/feature/fsm_sequence_append_head/test.rflx:50:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:47:10 if not TLV.Messages.Valid (Local_Messages_Ctx) then Ctx.P.Next_State := S_Final; pragma Assert (Local_Invariant); @@ -815,7 +815,7 @@ is Ctx.P.Slots.Slot_Ptr_6 := RFLX_Copy_Local_Messages_Buffer; pragma Assert (Ctx.P.Slots.Slot_Ptr_6 /= null); end; - -- tests/feature/fsm_sequence_append_head/test.rflx:51:25 + -- tests/feature/fsm_sequence_append_head/test.rflx:48:25 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -831,9 +831,9 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_sequence_append_head/test.rflx:51:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:48:10 Message_Tag := TLV.Message.Get_Tag (Ctx.P.Message_Ctx); - -- tests/feature/fsm_sequence_append_head/test.rflx:52:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:49:10 if not (TLV.Tags.Valid (Local_Tags_Ctx) and then TLV.Tags.Has_Element (Local_Tags_Ctx) @@ -844,9 +844,9 @@ is goto Finalize_Local; end if; Tag := TLV.Tags.Head (Local_Tags_Ctx); - -- tests/feature/fsm_sequence_append_head/test.rflx:55:16 + -- tests/feature/fsm_sequence_append_head/test.rflx:52:16 T_2 := Message_Tag = TLV.Msg_Data; - -- tests/feature/fsm_sequence_append_head/test.rflx:56:20 + -- tests/feature/fsm_sequence_append_head/test.rflx:53:20 T_3 := Tag = TLV.Msg_Data; if T_2 @@ -895,7 +895,7 @@ is Ghost; begin pragma Assert (Reply_2_Invariant); - -- tests/feature/fsm_sequence_append_head/test.rflx:64:10 + -- tests/feature/fsm_sequence_append_head/test.rflx:61:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_2_Invariant); end Reply_2; diff --git a/tests/feature/fsm_sequence_append_head/test.rflx b/tests/feature/fsm_sequence_append_head/test.rflx index 11d2c7dc9..c2497af5f 100644 --- a/tests/feature/fsm_sequence_append_head/test.rflx +++ b/tests/feature/fsm_sequence_append_head/test.rflx @@ -3,67 +3,64 @@ with TLV; package Test is generic - Channel : Channel with Writable; -- §S-P-C-W + Channel : Channel with Writable; machine S is - Messages : TLV::Messages; -- §S-D-V-T-MS, §S-D-V-E-N - Tags : TLV::Tags; -- §S-D-V-T-SS, §S-D-V-E-N - Message : TLV::Message; -- §S-D-V-T-M, §S-D-V-E-N + Messages : TLV::Messages; + Tags : TLV::Tags; + Message : TLV::Message; begin state Global is - Message_Tag : TLV::Tag; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Tag : TLV::Tag; -- §S-S-D-V-T-SC, §S-S-D-V-E-N + Message_Tag : TLV::Tag; + Tag : TLV::Tag; begin - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Messages'Append (TLV::Message'(Tag => TLV::Msg_Data, Length => 1, Value => [2])); - Tags'Append (TLV::Msg_Error); -- §S-S-A-AP-L - Message := Messages'Head; -- §S-S-A-A-HAT, §S-E-AT-H-V, §S-E-AT-H-MS - Message_Tag := Message.Tag; -- §S-S-A-A-S, §S-E-S-V - Tag := Tags'Head; -- §S-S-A-A-HAT, §S-E-AT-H-V, §S-E-AT-H-SS + Tags'Append (TLV::Msg_Error); + Message := Messages'Head; + Message_Tag := Message.Tag; + Tag := Tags'Head; transition goto Reply_1 - if Message_Tag = TLV::Msg_Data -- §S-S-T-V, §S-S-T-L - and Tag = TLV::Msg_Error -- §S-S-T-V, §S-S-T-L - goto null -- §S-S-T-N + if Message_Tag = TLV::Msg_Data + and Tag = TLV::Msg_Error + goto null exception - goto null -- §S-S-E + goto null end Global; state Reply_1 is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto Local -- §S-S-T-N + goto Local end Reply_1; state Local is - Local_Messages : TLV::Messages; -- §S-S-D-V-T-MS, §S-D-V-E-N - Local_Tags : TLV::Tags; -- §S-S-D-V-T-SS, §S-D-V-E-N - Message_Tag : TLV::Tag; -- §S-S-D-V-T-SC, §S-S-D-V-E-N - Tag : TLV::Tag; -- §S-S-D-V-T-SC, §S-S-D-V-E-N + Local_Messages : TLV::Messages; + Local_Tags : TLV::Tags; + Message_Tag : TLV::Tag; + Tag : TLV::Tag; begin - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Local_Messages'Append (TLV::Message'(Tag => TLV::Msg_Data, Length => 2, Value => [3, 4])); - -- §S-S-A-AP-MA, §S-E-A-T-SC, §S-E-A-E-L Messages'Append (TLV::Message'(Tag => TLV::Msg_Data, Length => 1, Value => [2])); - Local_Tags'Append (TLV::Msg_Data); -- §S-S-A-AP-L - Local_Tags'Append (TLV::Msg_Error); -- §S-S-A-AP-L - Message := Local_Messages'Head; -- §S-S-A-A-HAT, §S-E-AT-H-V, §S-E-AT-H-MS - Message_Tag := Message.Tag; -- §S-S-A-A-S, §S-E-S-V - Tag := Local_Tags'Head; -- §S-S-A-A-HAT, §S-E-AT-H-V, §S-E-AT-H-SS + Local_Tags'Append (TLV::Msg_Data); + Local_Tags'Append (TLV::Msg_Error); + Message := Local_Messages'Head; + Message_Tag := Message.Tag; + Tag := Local_Tags'Head; transition goto Reply_2 - if Message_Tag = TLV::Msg_Data -- §S-S-T-V, §S-S-T-L - and Tag = TLV::Msg_Data -- §S-S-T-V, §S-S-T-L - goto null -- §S-S-T-N + if Message_Tag = TLV::Msg_Data + and Tag = TLV::Msg_Data + goto null exception - goto null -- §S-S-E + goto null end Local; state Reply_2 is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply_2; end S; diff --git a/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-s-fsm.adb index d38edfa11..3792d0f29 100644 --- a/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-s-fsm.adb @@ -147,7 +147,7 @@ is pragma Warnings (On, "unused assignment"); Test.Message.Initialize (Local_Message_Ctx, Local_Message_Buffer); pragma Assert (Process_Invariant); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:43:10 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:42:10 if not Test.Message.Valid_Next (Ctx.P.Message_Ctx, Test.Message.F_Has_Data) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -236,7 +236,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:51:34 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:46:34 T_7 := RFLX.RFLX_Types.Base_Integer (Test.Message.Field_Size (Ctx.P.Message_Ctx, Test.Message.F_Data)); pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -268,7 +268,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:51:54 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:46:54 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -284,7 +284,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:53:32 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:47:32 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -300,7 +300,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:49:10 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:45:10 if not Test.Message.Valid_Next (Local_Message_Ctx, Test.Message.F_Has_Data) then Ctx.P.Next_State := S_Final; pragma Assert (Process_Invariant); @@ -363,7 +363,7 @@ is RFLX_Test_Message_Set_Data (Local_Message_Ctx, RFLX_Types.To_Length (Test.Message.Field_Size (RFLX_Ctx_P_Message_Ctx_Tmp, Test.Message.F_Data))); Ctx.P.Message_Ctx := RFLX_Ctx_P_Message_Ctx_Tmp; end; - -- tests/feature/fsm_setting_of_message_fields/test.rflx:56:16 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:50:16 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -379,9 +379,9 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:56:16 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:50:16 T_8 := Test.Message.Get_Has_Data (Ctx.P.Message_Ctx); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:56:35 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:50:35 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -397,7 +397,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:56:35 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:50:35 T_9 := Test.Message.Get_Has_Data (Local_Message_Ctx); if T_8 = T_9 then Ctx.P.Next_State := S_Reply; @@ -431,8 +431,8 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_setting_of_message_fields/test.rflx:64:10 - -- tests/feature/fsm_setting_of_message_fields/test.rflx:67:16 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:58:10 + -- tests/feature/fsm_setting_of_message_fields/test.rflx:61:16 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); diff --git a/tests/feature/fsm_setting_of_message_fields/test.rflx b/tests/feature/fsm_setting_of_message_fields/test.rflx index 8ae500369..e93938293 100644 --- a/tests/feature/fsm_setting_of_message_fields/test.rflx +++ b/tests/feature/fsm_setting_of_message_fields/test.rflx @@ -17,57 +17,51 @@ package Test is end message; generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Test::Message; -- §S-D-V-T-M, §S-D-V-E-N - Has_Data : Boolean := True; -- §S-D-V-S, §S-D-V-E-L - Length : Test::Length := 1; -- §S-D-V-S, §S-D-V-E-L + Message : Test::Message; + Has_Data : Boolean := True; + Length : Test::Length := 1; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid = True -- §S-S-T-VAT, §S-E-AT-V-V, §S-S-T-L - and Message.Has_Data = True -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and Message.Length = 2 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid = True + and Message.Has_Data = True + and Message.Length = 2 + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is Local_Message : Test::Message; begin - -- §S-S-A-MFA-V Message.Has_Data := Has_Data; - -- §S-S-A-MFA-V Message.Length := Length; - -- §S-S-A-MFA-A Message.Data := "A"; - -- §S-S-A-MFA-L Local_Message.Has_Data := True; - -- §S-S-A-MFA-L Local_Message.Length := Message.Data'Size / 8; - -- §S-S-A-MFA-A Local_Message.Data := Message.Data; transition goto Reply - if Message.Has_Data = Local_Message.Has_Data -- §S-S-T-S, §S-E-S-V - goto null -- §S-S-T-N + if Message.Has_Data = Local_Message.Has_Data + goto null exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition goto null - if Message.Has_Data -- §S-S-T-S - goto null -- §S-S-T-N + if Message.Has_Data + goto null exception - goto null -- §S-S-E + goto null end Reply; end S; diff --git a/tests/feature/fsm_simple/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_simple/generated/rflx-test-s-fsm.adb index c89e473ac..9e05e86c9 100644 --- a/tests/feature/fsm_simple/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_simple/generated/rflx-test-s-fsm.adb @@ -124,7 +124,7 @@ is Ghost; begin pragma Assert (Process_Invariant); - -- tests/feature/fsm_simple/test.rflx:26:10 + -- tests/feature/fsm_simple/test.rflx:25:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -183,7 +183,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_simple/test.rflx:35:10 + -- tests/feature/fsm_simple/test.rflx:34:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_simple/test.rflx b/tests/feature/fsm_simple/test.rflx index 796d2bcfd..1e5b861a3 100644 --- a/tests/feature/fsm_simple/test.rflx +++ b/tests/feature/fsm_simple/test.rflx @@ -3,38 +3,37 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition goto Process - if Message'Valid = True -- §S-S-T-VAT, §S-E-AT-V-V, §S-S-T-L - and Message.Message_Type = Universal::MT_Data -- §S-S-T-S, §S-E-S-V, §S-S-T-L - and Message.Length = 1 -- §S-S-T-S, §S-E-S-V, §S-S-T-L - goto null -- §S-S-T-N + if Message'Valid = True + and Message.Message_Type = Universal::MT_Data + and Message.Length = 1 + goto null exception - goto null -- §S-S-E + goto null end Start; state Process is begin - -- §S-S-A-A-MA, §S-E-A-T-SC, §S-E-A-E-L Message := Universal::Message'(Message_Type => Universal::MT_Data, Length => 1, Data => [2]); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/fsm_variable_initialization/generated/rflx-test-s-fsm.adb b/tests/feature/fsm_variable_initialization/generated/rflx-test-s-fsm.adb index 46f8a4807..1886db0c4 100644 --- a/tests/feature/fsm_variable_initialization/generated/rflx-test-s-fsm.adb +++ b/tests/feature/fsm_variable_initialization/generated/rflx-test-s-fsm.adb @@ -137,7 +137,7 @@ is pragma Warnings (On, "condition can only be False if invalid values present"); -- tests/feature/fsm_variable_initialization/test.rflx:24:10 Ctx.P.Global := Ctx.P.Uninitialized_Global + 20; - -- tests/feature/fsm_variable_initialization/test.rflx:27:51 + -- tests/feature/fsm_variable_initialization/test.rflx:26:51 T_1 := Universal.Value'Size; pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); @@ -169,7 +169,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_variable_initialization/test.rflx:27:75 + -- tests/feature/fsm_variable_initialization/test.rflx:26:75 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -185,7 +185,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/fsm_variable_initialization/test.rflx:26:10 + -- tests/feature/fsm_variable_initialization/test.rflx:25:10 Universal.Message.Reset (Ctx.P.Message_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -243,7 +243,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/fsm_variable_initialization/test.rflx:39:10 + -- tests/feature/fsm_variable_initialization/test.rflx:38:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/fsm_variable_initialization/test.rflx b/tests/feature/fsm_variable_initialization/test.rflx index e38734bbd..f7b01d30c 100644 --- a/tests/feature/fsm_variable_initialization/test.rflx +++ b/tests/feature/fsm_variable_initialization/test.rflx @@ -3,42 +3,41 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - Global : Universal::Value := 11; -- §S-D-V-T-SC, §S-D-V-E-L - Uninitialized_Global : Universal::Value; -- §S-D-V-T-SC, §S-D-V-E-N - Message : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + Global : Universal::Value := 11; + Uninitialized_Global : Universal::Value; + Message : Universal::Message; begin state Start is begin - Channel'Read (Message); -- §S-S-A-RD-V + Channel'Read (Message); transition - goto Process -- §S-S-T-N + goto Process end Start; state Process is - Local : Universal::Value := 2; -- §S-S-D-V-T-SC, §S-S-D-V-E-L + Local : Universal::Value := 2; begin - Local := Local + Message.Value; -- §S-S-A-A-ME, §S-S-A-A-L, §S-S-A-A-S, §S-S-A-A-V, §S-E-S-V - Uninitialized_Global := Local; -- §S-S-A-A-V - Global := Uninitialized_Global + 20; -- §S-S-A-A-ME, §S-S-A-A-L, §S-S-A-A-V - -- §S-S-A-A-MA + Local := Local + Message.Value; + Uninitialized_Global := Local; + Global := Uninitialized_Global + 20; Message := Universal::Message'(Message_Type => Universal::MT_Value, Length => Universal::Value'Size / 8, Value => Global); transition goto Reply - if Local < Global -- §S-S-T-V - goto null -- §S-S-T-N + if Local < Global + goto null exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (Message); -- §S-S-A-WR-V + Channel'Write (Message); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/messages_with_implict_size/generated/rflx-test-s-fsm.adb b/tests/feature/messages_with_implict_size/generated/rflx-test-s-fsm.adb index c690a0293..e8a123eba 100644 --- a/tests/feature/messages_with_implict_size/generated/rflx-test-s-fsm.adb +++ b/tests/feature/messages_with_implict_size/generated/rflx-test-s-fsm.adb @@ -60,7 +60,7 @@ is Ghost; begin pragma Assert (Process_Invariant); - -- tests/feature/messages_with_implict_size/test.rflx:21:95 + -- tests/feature/messages_with_implict_size/test.rflx:20:95 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -76,7 +76,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/messages_with_implict_size/test.rflx:21:10 + -- tests/feature/messages_with_implict_size/test.rflx:20:10 Universal.Message.Reset (Ctx.P.M_S_Ctx); if not Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Final; @@ -144,7 +144,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/messages_with_implict_size/test.rflx:30:10 + -- tests/feature/messages_with_implict_size/test.rflx:29:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/messages_with_implict_size/test.rflx b/tests/feature/messages_with_implict_size/test.rflx index 1601664f4..70732708d 100644 --- a/tests/feature/messages_with_implict_size/test.rflx +++ b/tests/feature/messages_with_implict_size/test.rflx @@ -3,33 +3,32 @@ with Universal; package Test is generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - M_R : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N - M_S : Universal::Message; -- §S-D-V-T-M, §S-D-V-E-N + M_R : Universal::Message; + M_S : Universal::Message; begin state Start is begin - Channel'Read (M_R); -- §S-S-A-RD-V + Channel'Read (M_R); transition - goto Process -- §S-S-T-N + goto Process end Start; state Process is begin - -- §S-S-A-A-MA, §S-E-A-T-SC, §S-E-A-T-O, §S-E-A-E-L, §S-E-A-E-S M_S := Universal::Message'(Message_Type => Universal::MT_Unconstrained_Data, Data => M_R.Data); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (M_S); -- §S-S-A-WR-V + Channel'Write (M_S); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-s-fsm.adb b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-s-fsm.adb index d0bf8e6d5..252d59b09 100644 --- a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-s-fsm.adb +++ b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-s-fsm.adb @@ -60,7 +60,7 @@ is Ghost; begin pragma Assert (Process_Invariant); - -- tests/feature/messages_with_single_opaque_field/test.rflx:24:34 + -- tests/feature/messages_with_single_opaque_field/test.rflx:23:34 pragma Warnings (Off, "condition can only be False if invalid values present"); pragma Warnings (Off, "condition is always False"); pragma Warnings (Off, "this code can never be executed and has been deleted"); @@ -76,7 +76,7 @@ is pragma Warnings (On, "this code can never be executed and has been deleted"); pragma Warnings (On, "condition is always False"); pragma Warnings (On, "condition can only be False if invalid values present"); - -- tests/feature/messages_with_single_opaque_field/test.rflx:24:10 + -- tests/feature/messages_with_single_opaque_field/test.rflx:23:10 Test.Message.Reset (Ctx.P.M_S_Ctx); declare pragma Warnings (Off, "is not modified, could be declared constant"); @@ -133,7 +133,7 @@ is Ghost; begin pragma Assert (Reply_Invariant); - -- tests/feature/messages_with_single_opaque_field/test.rflx:33:10 + -- tests/feature/messages_with_single_opaque_field/test.rflx:32:10 Ctx.P.Next_State := S_Final; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/feature/messages_with_single_opaque_field/test.rflx b/tests/feature/messages_with_single_opaque_field/test.rflx index e8ab0d577..16af8c33e 100644 --- a/tests/feature/messages_with_single_opaque_field/test.rflx +++ b/tests/feature/messages_with_single_opaque_field/test.rflx @@ -6,33 +6,32 @@ package Test is end message; generic - Channel : Channel with Readable, Writable; -- §S-P-C-RW + Channel : Channel with Readable, Writable; machine S is - M_R : Message; -- §S-D-V-T-M, §S-D-V-E-N - M_S : Message; -- §S-D-V-T-M, §S-D-V-E-N + M_R : Message; + M_S : Message; begin state Start is begin - Channel'Read (M_R); -- §S-S-A-RD-V + Channel'Read (M_R); transition - goto Process -- §S-S-T-N + goto Process end Start; state Process is begin - -- §S-S-A-A-MA, §S-E-A-T-O, §S-E-A-E-S M_S := Message'(Data => M_R.Data); transition - goto Reply -- §S-S-T-N + goto Reply exception - goto null -- §S-S-E + goto null end Process; state Reply is begin - Channel'Write (M_S); -- §S-S-A-WR-V + Channel'Write (M_S); transition - goto null -- §S-S-T-N + goto null end Reply; end S; diff --git a/tests/feature/parameterized_messages/test.rflx b/tests/feature/parameterized_messages/test.rflx index 42ec37089..c28e6fa92 100644 --- a/tests/feature/parameterized_messages/test.rflx +++ b/tests/feature/parameterized_messages/test.rflx @@ -38,7 +38,7 @@ package Test is if M_R'Valid goto Error exception - goto null -- §S-S-E + goto null end Receive; state Process diff --git a/tools/check_requirements.py b/tools/check_requirements.py deleted file mode 100755 index ef30abfda..000000000 --- a/tools/check_requirements.py +++ /dev/null @@ -1,193 +0,0 @@ -#!/usr/bin/env python3 - -"""Check that each requirement is referenced at least once in the given directories.""" - -from __future__ import annotations - -import argparse -import itertools -import re -import sys -from collections.abc import Sequence -from pathlib import Path - -ID_SEPARATOR = "-" -ID_REGEX = r"§(?:[A-Z0-9]+" + ID_SEPARATOR + r")*[A-Z0-9]+" - - -class ID: - def __init__(self, identifier: str): - if not re.match(ID_REGEX, identifier): - raise ValueError(f'invalid identifier "{identifier}"') - - self._parts = tuple(p for p in identifier[1:].split(ID_SEPARATOR)) - - def __str__(self) -> str: - return "§" + ID_SEPARATOR.join(str(p) for p in self._parts) - - def __lt__(self, other: object) -> bool: - if not isinstance(other, self.__class__): - return NotImplemented - return self.parts < other.parts[: len(self.parts)] - - @property - def parts(self) -> tuple[str, ...]: - return self._parts - - -class Requirement: - def __init__( - self, - identifier: str, - description: str, - referenced: bool = False, - requirements: list[Requirement] | None = None, - ): - self._identifier = identifier - self._description = description.capitalize() - self._referenced = referenced - self.requirements = requirements or [] - - def __contains__(self, value: str) -> bool: - return value == self.identifier or any(value in req for req in self.requirements) - - def __lt__(self, other: object) -> bool: - if not isinstance(other, self.__class__): - return NotImplemented - return ID(self.identifier) < ID(other.identifier) - - @property - def identifier(self) -> str: - return str(self._identifier) - - @property - def description(self) -> str: - return self._description - - @property - def referenced(self) -> bool: - if self.requirements: - return all(req.referenced for req in self.requirements) - return self._referenced - - @referenced.setter - def referenced(self, value: bool) -> None: - if self.requirements: - raise ValueError('"referenced" attribute of meta requirement must not be set') - self._referenced = value - - -def main(argv: Sequence[str]) -> bool | str: - arg_parser = argparse.ArgumentParser() - arg_parser.add_argument("requirements", metavar="REQUIREMENTS_FILE", type=Path) - arg_parser.add_argument("directories", metavar="DIRECTORY", type=Path, nargs="+") - arg_parser.add_argument("--checkbox-list", help="print checkbox list", action="store_true") - args = arg_parser.parse_args(argv[1:]) - - requirements, error = parse_requirements(args.requirements) - if not requirements: - return "no requirements found" - - references = search_references(args.directories) - - error |= check_references(requirements, references) - - if args.checkbox_list: - print_checkbox_list(requirements) - - print_statistics(requirements) - - return error - - -def parse_requirements(requirements_file: Path) -> tuple[list[Requirement], bool]: - requirements: dict[str, Requirement] = {} - error = False - - for l in requirements_file.read_text().split("\n"): - if "§" not in l: - continue - - match = re.search(r"(?:^|[-#.!?§/*] )([^-#.!?§/*]*)? \[(§[^\]]+)\]", l) - if match: - for identifier in re.findall(ID_REGEX, match.group(2)): - req = Requirement(identifier, match.group(1)) - if req.identifier in requirements or any( - identifier == req.identifier for identifier in requirements - ): - print(f'duplicate requirement "{req.identifier}"') # noqa: T201 - error = True - requirements[req.identifier] = req - - if ID_SEPARATOR in req.identifier: - parent = req.identifier.rsplit(ID_SEPARATOR, 1)[0] - if parent in requirements: - requirements[parent].requirements.append(req) - else: - print( # noqa: T201 - f'missing requirement "{parent}" for "{req.identifier}"', - ) - error = True - else: - print(f'ignored "{l}"') # noqa: T201 - - return (list(requirements.values()), error) - - -def search_references(directories: Sequence[Path]) -> list[str]: - references: list[str] = [] - - for d in directories: - for f in itertools.chain(d.rglob("*.py"), d.rglob("*.rflx")): - if f.is_file(): - content = f.read_text() - references.extend(r for r in re.findall(ID_REGEX, content)) - - return references - - -def check_references(requirements: Sequence[Requirement], references: Sequence[str]) -> bool: - error = False - - for req in requirements: - if req.identifier in references: - if not req.requirements: - req.referenced = True - else: - print(f'meta requirement "{req.identifier}" must not be referenced') # noqa: T201 - error = True - - undefined = [ - ref - for ref in references - if all(ref != req.identifier and ref not in req for req in requirements) - ] - if undefined: - for ref in undefined: - print(f'reference to undefined requirement "{ref}"') # noqa: T201 - error = True - - for r in [r for r in requirements if not r.referenced and not r.requirements]: - print(f'unreferenced requirement "{r.identifier}"') # noqa: T201 - error = True - - return error - - -def print_checkbox_list(requirements: Sequence[Requirement]) -> None: - print() # noqa: T201 - for r in sorted(requirements): - indentation = " " * r.identifier.count(ID_SEPARATOR) - status = "x" if r.referenced else " " - print(f"{indentation}- [{status}] {r.description} ({r.identifier})") # noqa: T201 - print() # noqa: T201 - - -def print_statistics(requirements: Sequence[Requirement]) -> None: - total = len(requirements) - referenced = len({r for r in requirements if r.referenced}) - print(f"{referenced} / {total} ({referenced / total * 100:.2f} %)") # noqa: T201 - - -if __name__ == "__main__": - sys.exit(main(sys.argv))