Up  Next

Module Aadl_ast (.ml)


module Aadl_ast: sig .. end
The AADL Abstract Syntax Tree definition.

Time-stamp: <modified the 05/06/2007 (at 10:45) by Erwan Jahier>
Author(s): Louis Mandel, Erwan Jahier


Package



type package = {
   pack_id : Ident.t; (*Name of the package.*)
   pack_public : aadl_declaration list; (*Set of public declarations.*)
   pack_public_prop : property list; (*Set of public properties.*)
   pack_private : aadl_declaration list; (*Set of private declarations.*)
   pack_private_prop : property list; (*Set of private properties.*)
}

AADL declaration

AADL declarations are components or port groups. 

    component ::=
      category [implementation] component_identifier
        extends component_identifier
        [ features ( { feature | feature_refinement }+ | none ) ]
        [ refines type ( { feature_refinement }+ | none ) ]
        [ subcomponents ( { subcomponent }+ | none ) ]
        [ calls ( { subprogram_call_sequence }+ | none ) ]
        [ connections ( { connection }+ | none ) ]
        [ flows ( { flow }+ | none ) ]
        [ modes ( { mode }+ | none ) ]
        [ properties ( { property }+ | none ) ]
        { annex_subclause }*
      end component_identifier;


 
    port_group ::=
      port group defining_identifier 
        [ extends unique_port_group_type_reference ]
        ( features
            { port_spec | port_refinement |
              port_group_spec | port_group_refinement }*
          [ inverse of unique_port_group_type_reference ]
        |
          inverse of unique_port_group_type_reference
        )
        [ properties ( { portgroup_property_association }+ | none ) ]
        { annex_subclause }*
      end defining_identifier ;


type aadl_declaration =
| Component of component
| Port_group of port_group

type component = {
   comp_id : Ident.t;
   comp_kind : component_kind; (*type or implementation.*)
   comp_cate : category; (*process, thread, system, ...*)
   comp_extd : Ident.t option; (*name of the extended component.*)
   comp_feat : feature list;
   comp_fref : feature_refinement list;
   comp_subc : subcomponent list;
   comp_call : call_sequence list;
   comp_conn : connection list;
   comp_flow : flow list;
   comp_mode : mode list;
   comp_prop : property list;
   comp_annx : annex list;
   comp_normalize : bool;
}
type port_group = {
   portgrp_id : Ident.t;
   portgrp_extd : Ident.t option;
   portgrp_feat : feature list;
   portgrp_fref : feature_refinement list;
   portgrp_inve : Ident.t option;
   portgrp_prop : property list;
   portgrp_annx : annex list;
   portgrp_normalize : bool;
}
type component_kind =
| Type
| Implementation

type category =
| Data
| Subprogram
| Thread
| Thread_group
| Process
| Processor
| Memory
| Bus
| Device
| System

Feature

    feature ::=
      defining_identifier : feature_kind
      [ { { port_property_association }+ } ] ;

    feature_kind ::=
        ( ( in | out | in out ) port_type)
      | port group [ unique_port_group_type_reference ]
      | subprogram [ classifier_reference ]
      | ( provides | requires ) ( data | bus ) access [ identifier ]
      | ( in | out | in out ) parameter [ classifier_reference ]

    port_type ::=
        data port [ data_classifier_reference ]
      | event data port [ data_classifier_reference ]
      | event port


type feature = Ident.t * feature_kind * property_association list

type feature_kind =
| Feat_data_port of in_out_flag * classifier_reference option
| Feat_event_data_port of in_out_flag * classifier_reference option
| Feat_event_port of in_out_flag
| Feat_port_group of unique_port_group_type_reference option
| Feat_server_subprogram_spec of unique_subprogram_reference option
| Feat_data_subprogram_spec of classifier_reference option
| Feat_subcomponent_access of access_kind * category * Ident.t option
| Feat_parameter of in_out_flag * classifier_reference option

type in_out_flag =
| In
| Out
| In_Out 
type unique_port_group_type_reference = Ident.t 
type classifier_reference = Ident.t 
type unique_subprogram_reference = Ident.t

type access_kind =
| Provided
| Required

Feature refinement


type feature_refinement
TODO

Subcomponent

    subcomponent ::=
      defining_subcomponent_identifier :
        component_category [ component_classifier_reference ]
        [ { { property_association }+ } ]
        [ in_modes ] ;


type subcomponent = Ident.t * category * classifier_reference option *
       property_association list

Calls

    subprogram_call_sequence ::=
      [ identifier : ]
        { { subprogram_call }+ } [ in_modes ] ;

    subprogram_call ::=
      defining_call_identifier : subprogram called_subprogram
        [ { { subcomponent_call_property_association }+ } ] ;


type call_sequence = Ident.t option *
       (Ident.t * Ident.t * property_association list) list

Connection

    connection ::=
      [ defining_connection_identifier :] connection_kind 
        source_identifier ( -> | ->> ) destination_identifier
      [ { { property_association }+ } ]
      [ in_modes_and_transitions ] ;


type connection = Ident.t option * connection_kind * Ident.t *
       connection_arrow * Ident.t * property_association list

type connection_kind =
| Conn_data_port
| Conn_event_port
| Conn_event_data_port
| Conn_port_group
| Conn_parameter
| Conn_bus_access
| Conn_data_access

type connection_arrow =
| Conn_arrow (*->*)
| Conn_delayed_arrow (*->>*)

Flow

    flow ::= 
      flow_spec
      | flow_implementation

    flow_spec ::=
      identifier : 
	( ( flow source identifier
          | flow path identifier -> identifier
          | flow sink identifier )
          [ { { property_association }+ } ] ;
        | refined to flow (source | sink | path) { { property_association }+ })


type flow =
| FlowSpec of Ident.t * flow_kind * property_association list
| FlowImpl of Ident.t * flow_impl_kind

type flow_kind =
| Flow_source of Ident.t
| Flow_sink of Ident.t
| Flow_path of Ident.t * Ident.t
| Flow_refined_source
| Flow_refined_sink
| Flow_refined_path

type flow_impl_kind =
| FlowImpl_source of Ident.t list * Ident.t
| FlowImpl_sink of Ident.t * Ident.t list
| FlowImpl_path of Ident.t list * Ident.t * Ident.t * Ident.t list
| FlowImpl_refined_source (*TODO*)
| FlowImpl_refined_sink (*TODO*)
| FlowImpl_refined_path (*TODO*)

Mode


type mode
TODO

Property

    property_association ::=
      identifier ( => | +=> ) [ constant ] [ access ] property_value
      [ applies to identifier [ in_modes ] [ in_bindings ] ]; 


type property = property_association 
type property_association = Ident.t * property_arrow * property_value * Ident.t option

TODO : constant, access, in_modes, in_bindings

type property_arrow =
| Prop_arrow
| Prop_plus_arrow 
type property_value = property_expression list

type property_expression =
| Prop_expr_immediate of immediate_expression
| Prop_expr_integer_range of aadl_intger_or_constant * aadl_intger_or_constant
* int option
| Prop_expr_real_range of aadl_real_or_constant * aadl_real_or_constant
* float option
| Prop_expr_enumeration of Ident.t
| Prop_expr_property_term of Ident.t
| Prop_expr_component_classifier_term of category * Ident.t
| Prop_expr_reference_term of Ident.t

type immediate =
| Imm_bool of bool
| Imm_int of aadl_intger_or_constant
| Imm_real of aadl_real_or_constant
| Imm_string of string

type immediate_expression =
| Imm_const of immediate
| Imm_op1 of string * immediate_expression
| Imm_op2 of string * immediate_expression * immediate_expression

type aadl_intger_or_constant =
| Int of int * Ident.t option
| Int_const of Ident.t

type aadl_real_or_constant =
| Real of float * Ident.t option
| Real_const of Ident.t

Annex


type annex
TODO
val category_to_string : category -> string