producer_consumer.aadl:123:05: warning: T references a component type
producer_consumer.aadl:127:05: warning: CPU references a component type
producer_consumer.aadl:128:05: warning: the_bus references a component type
ocarina: Total: 0 error and 3 warnings
Begin Thread
Begin Processor
Begin Types
Begin Port
Begin Main
producer_consumer.aadl:53:05 "Main.bcg"= divbranching reduction of "PRODUCER_CONSUMER_Main.lnt";
property PROPERTY_Deadlock is
deadlock of "Main.bcg";
expected FALSE;
end property;
property Scheduling_Test (ID) is
"Main_$ID.bcg"="Main.bcg"|=
[ true* . "ACTIVATION_$ID !T_Error" ] false;
expected TRUE;
end property;
module PRODUCER_CONSUMER_Threads (PRODUCER_CONSUMER_Types) is
process Thread_P_Impl [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_DATA_SOURCE: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin)
[]
ACTIVATION (T_End);
AADL_PORT_DATA_SOURCE (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_DATA_SOURCE (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_Q_Impl [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_DATA_SINK: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_DATA_SINK (AADLDATA)
[]
ACTIVATION (T_End)
[]
ACTIVATION (T_All);
AADL_PORT_DATA_SINK (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
end module
module PRODUCER_CONSUMER_Ports (PRODUCER_CONSUMER_Types) is
producer_consumer.aadl:53:05 Backends: warning : LNT generation requires the definition of Queue_Size property. For this generation, the default value (Queue_Size = 3) is used.
Begin Port
module LNT_Generic_Process_For_Port_Connections (Types) is
-- No Behavior Annex
-- data port --
process Data_Port [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data]
is
loop
select
Input (AADLDATA)
[]
Output (AADLDATA)
end select
end loop
end process
process Event_Port_Periodic [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data](
Queue_Size: Nat)
Input: LNT_Channel_Port,
Output: LNT_Channel_Port]
is
var
Nb_Input : Nat
in
Nb_Input := 0;
var Data : LNT_Type_Data in
Data := EMPTY;
loop
select
Input (AADLDATA);
if (Nb_Input < Queue_Size)
then
Nb_Input := Nb_Input + 1
end if
[]
if (Nb_Input > 0)
then
Output (AADLDATA);
Nb_Input := Nb_Input - 1
end if
Input (?Data)
[]
Output (Data)
end select
end loop
end var
end process
end process
process Event_Port_Sporadic [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data,
-- event port --
-- for no periodic threads --
process Event_Port [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
Nb_Input : Nat,
Data : LNT_Type_Data,
FIFO : LNT_Type_Data_FIFO,
Is_New : bool
in
Nb_Input := 0;
FIFO := {};
Data := EMPTY;
Is_New := false;
loop
select
Input (AADLDATA);
if (Nb_Input < Queue_Size)
then
Nb_Input := Nb_Input + 1
end if;
Is_New := true
Input (?Data);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (Data, FIFO)
[]
if (Nb_Input > 0)
then
Output (AADLDATA);
Nb_Input := Nb_Input - 1
if (FIFO != {}) then
Output (Head (FIFO));
FIFO := tail (FIFO)
else
Output (EMPTY)
end if
[]
if (Is_New)
then
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
...
...
@@ -149,293 +72,39 @@ module PRODUCER_CONSUMER_Ports (PRODUCER_CONSUMER_Types) is
end select
end loop
end var
end process
end module
module PRODUCER_CONSUMER_Types
with "==", "eq" , "<", "lt" , "<=", "le" , ">", "gt" , ">=", "ge" is
