BA front-end crashed on ba_action

[sinkinben]

ocarina version

$ ocarina --version
Ocarina 2017.x (Working Copy from re88d7c9)
Copyright (c) 2003-2009 Telecom ParisTech, 2010-2019 ESA & ISAE

I use cheddar (supported by ocarina) to analysis an AADL system. But OCARINA BUG DETECTED occurred. Is it caused by AADL models or just by ocarina? LOG:

E:\ProgramFiles\Git\usr\local\bin\ocarina.exe -aadlv2 -g cheddar -r ShootControlComputer_init.impl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Conse_Control_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Effective_conseq_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WdCancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WeaponReady_Cancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_Wea_PackageHeadaddAADL_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Plugin_Resources\Base_Types.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Memcmp_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\EleDeto_Check_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_MisUnlo_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisReady3_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_SelfChe_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_CancelReady3_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_LaunchReadyCancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_Ready1_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\sizeof_op_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\KIO_Write_Chan_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_Battery_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_DM_WDHandleHC_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_SafeOn_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_MisLocU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_DM_WDHandleMisL_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_MisLock_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_MisChk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Single_Control_program_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Invalid_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\EleDeto_Check_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Control_Order_Process_Programs_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_HatchCoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_DM_WDHandleEC_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_NET_StateRes_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_LS1_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\DataType.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_Soft_LauReady_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_MisReady3Chk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\MisUnlock_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Invalid_conseq_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Safety_Relieve_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Plugin_Resources\Predeclared_Property_Sets\Thread_Properties.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\HatchCoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\ShootControlComputer_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_EleDeto_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Process_Level_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_WeaOperMisChk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\ExhaustCoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_NET_WorkAbnSta_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_SafeUndo_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisChk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn2_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_MisFSupU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_SafeU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\bcopy_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Driver_Level_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\HatchCoverClose_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_CT_MisSelMisKind_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LocalVarSpaceHolder_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\MotorIgni_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOPortInPipe_s_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_TimeWatchDog_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WeaponReady_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_HCoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Plugin_Resources\Data_Model.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Xor_CheckSum_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_PlatInfo_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Control_Order_Process_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn3_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Pulse_Read_24H_Counter_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\HatchCoverOpen_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_DM_WDHandle_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn3_Cancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_MisUnlocU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisReady1_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Mis_Launch_Order_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_WeaOperPow3_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Plugin_Resources\Predeclared_Property_Sets\Memory_Properties.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_CheHCC_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_Ready_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_MisFSupUC_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_CheEX0_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_CCDeto2_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Effective_conseq_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WeaponReady_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_CancelReady2_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Safety_Recovery_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\ExhaustCoverClose_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOPortInputPipe_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LogMsg_wrapper_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_BatChkOk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WdStart_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_SafeLocU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_NetCheckSum_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_LaunchReady_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_289ACheckSum_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_ExhaustCoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_CancelReady1_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Mis_Launch_Order_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\ExhaustCoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_CCDeto_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisReady3Chk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_CheHC0_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_PackageHeadaddAADL_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\SysClkRateGet_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisCmpChk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_MAN_PackageHeadaddAADL_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_Soft_LauReadyCanc_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\bzero_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_Launch_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_ECoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Conse_Control_program_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\HotBattery_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\write_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_CheEXC_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_Safe_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_HatchCoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_LS2_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_NetMessConvert_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_PowerIn_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\HatchCoverClose_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_ReadyCanc_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Single_Control_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Data_Parse_Level_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn2_Cancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\TickGet_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Effective_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_DT_422_Send_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_HCoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Launch_Ready_Invalid_conseq_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_BatChkIn_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\KIO_Read_Chan_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\WeaponReady_Cancel_train_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn1_Cancel_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_CancelReady_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_EarthO_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Read_IOIn_Resu_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LogMsg_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_PowerOn1Chk_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Control_Order_Process_thread_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_MisReady2_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_PC_ExhaustCoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\MisLock_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\LCU_WD_TRAIN_Soft_ECoverOpen_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Plugin_Resources\Predeclared_Property_Sets\Communication_Properties.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Missile_PowerOn1_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\Main_Control_Level_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOPortInput_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOOut_LauOrdU_init.aadl D:\programfiles\osate-64bit(2.2.3)\workspace\Converge\FRAME_LCU_DM_IOIn_MisLock_init.aadl
+========================== OCARINA BUG DETECTED =========================+
| Detected exception: SYSTEM.ASSERTIONS.ASSERT_FAILURE                    |
| Error: ocarina-builder-aadl_ba-actions.adb:169                          |
| Please refer to the User's Guide for more details.                      |
+=========================================================================+

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : ocarina-builder-aadl_ba-actions.adb:169

Symbolic Traceback:

[yoogx]

Looks like there is a bug in the BA parser that is triggered by your model Can you share the model so that I investigate ?

Also, note that the BA is not taken into account by the Cheddar back-end. You may add "-disable-annexes=all" to disable all annexes to the command line

[sinkinben]

I'm sorry that this AADL model can't be shared with you for copyright reasons. Thanks for your reply : ） I will discuss this with my mentor Yang. I close this issue.

[sinkinben]

I have add -disable-annexes=all to cmd line. But there is still something wrong. (OCARINA BUG DETECTED) The log:

$ ocarina.exe -disable-annexes=all -aadlv2 -g cheddar -r dpu.impl dpu_aadl2_no_comment.aadl MyProperties.aadl
dpu_aadl2_no_comment.aadl:488:02: warning: mem references a component type
dpu_aadl2_no_comment.aadl:489:02: warning: sysbus references a component type
dpu_aadl2_no_comment.aadl:490:02: warning: lan references a component type
dpu_aadl2_no_comment.aadl:492:02: warning: cpu1 references a component type
dpu_aadl2_no_comment.aadl:494:02: warning: fibgyr1 references a component type
dpu_aadl2_no_comment.aadl:495:02: warning: fibgyr2 references a component type
dpu_aadl2_no_comment.aadl:496:02: warning: fibgyr3 references a component type
dpu_aadl2_no_comment.aadl:497:02: warning: fibgyr4 references a component type
dpu_aadl2_no_comment.aadl:498:02: warning: fibgyr5 references a component type
dpu_aadl2_no_comment.aadl:500:02: warning: mecgyr references a component type
dpu_aadl2_no_comment.aadl:430:02: warning: buf references a component type
dpu_aadl2_no_comment.aadl:431:02: warning: N1 references a component type
dpu_aadl2_no_comment.aadl:432:02: warning: N2 references a component type
ocarina: Total: 0 error and 13 warnings
+========================== OCARINA BUG DETECTED =========================+
| Detected exception: SYSTEM.ASSERTIONS.ASSERT_FAILURE                    |
| Error: failed precondition from ocarina-backends-cheddar-mapping.ads:61 |
| Please refer to the User's Guide for more details.                      |
+=========================================================================+

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ocarina-backends-cheddar-mapping.ads:61

Symbolic Traceback:

I have sent the aadl models to your mailbox (My email is sinkinben@outlook.com). PS: I am sorry that the model can't be published on git. Could you please help me to check the model? Thanks a lot.

[yoogx]

From this exception, it is likely than one of your processor does not define the Scheduling_Protocol property

[sinkinben]

What schedule protocol property do Ocarina & Cheddar support? I have defined theScheduling_Protocol property in processor, and tested several schedule protocols such as POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL, RMS. But they did not work. Is there something wrong with my schedule protocol declaration?

POSIX_1003 Test Log

processor intel_80c32
properties
    Scheduling_Protocol => (POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL);
end intel_80c32;

$ ocarina.exe -disable-annexes=all -aadlv2 -g cheddar dpu.impl *.aadl
dpu_aadl2_no_comment.aadl:488:02: warning: mem references a component type
dpu_aadl2_no_comment.aadl:489:02: warning: sysbus references a component type
dpu_aadl2_no_comment.aadl:490:02: warning: lan references a component type
dpu_aadl2_no_comment.aadl:492:02: warning: cpu1 references a component type
dpu_aadl2_no_comment.aadl:494:02: warning: fibgyr1 references a component type
dpu_aadl2_no_comment.aadl:495:02: warning: fibgyr2 references a component type
dpu_aadl2_no_comment.aadl:496:02: warning: fibgyr3 references a component type
...
ocarina: Total: 0 error and 13 warnings
+========================== OCARINA BUG DETECTED =========================+
| Detected exception: SYSTEM.ASSERTIONS.ASSERT_FAILURE                    |
| Error: failed precondition from ocarina-backends-cheddar-mapping.ads:81 |
| Please refer to the User's Guide for more details.                      |
+=========================================================================+

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ocarina-backends-cheddar-mapping.ads:81

Symbolic Traceback:

RMS Test log

processor intel_80c32
properties
    Scheduling_Protocol => (RMS);
end intel_80c32;

The log is the same as above.

[yoogx]

Check the source code, the.ads error moved from line 61 (scheduler) to 81 81 indicates your thread does not define compute_execution_time

[sinkinben]

Thanks for your quick reply. I will check my AADL model in detail. By the way, could you please provide me with a simple AADL model example? In this way, maybe I can find out what the problem is in my AADL model. Thanks a lot.

[yoogx]

Check the AADLib project for examples, in particular RMA and Radar

[yoogx]

No example provided to investigate this bug, closing