AGREE not translating all processes in Phase 2 model

[cong-liu-2000]

Only 3 out of 14 processes were translated to Lustre:
node _TOP__RADIO
node _TOP__WPM
node _TOP__MON_GEO

Model location:
https://github.com/loonwerks/case-ta6-experimental-platform-models/tree/master/Phase-2-UAV-Experimental-Platform-Transformed

[ericmercer]

I have not been able to look carefully at the Lustre model yet, but I too have been concerned about AGREE not including contracts from threads that are embedded in processes. Thomas did some work, as I recall, to lift those contracts in generating the Lustre model, but my recollection may not be correct. From what you are seeing, I am thinking that that lift is not happening because the MON_GEO has additional guarantees at the process level explaining why it appears in the top-level model.

[ericmercer]

Also, so that we can settle the contracts while sorting out the AGREE translation, Cong, will you create an SW_Lift.Impl that uses the threads rather than the processes for the implementation? We can put that in the same SW.aadl file as a secondary implementation. AGREE should work as expected on that model since there is no lift required.

[cong-liu-2000]

Eric, I do not think you can directly compose a "system" with "thread". So I introduced a dummy "top" process as an intermediate container. The result is even worse. Only "main" node is translated.

system implementation SW.Impl2
	subcomponents
		top: process top.Impl;

…
process implementation top.Impl
subcomponents
FC_UART: thread Drivers::UARTDriver.Impl;
RADIO: thread RadioDriver_Attestation_thr.Impl;
FlyZones: thread FlyZonesDatabase_thr.Impl;
UXAS: thread UxAS_thr.Impl;
WPM: thread WaypointPlanManagerService_thr.Impl;
AM: thread CASE_AttestationManager_thr.Impl;
AM_Gate: thread CASE_AttestationGate_thr.Impl;
FLT_AReq: thread CASE_Filter_AReq_thr.Impl;
FLT_OR: thread CASE_Filter_OR_thr.Impl;
FLT_LST: thread CASE_Filter_LST_thr.Impl;
MON_REQ: thread CASE_Monitor_Req_thr.Impl;
ALERT_SYNC: thread alert_sync_thr.Impl;
FLT_ARes: thread CASE_Filter_ARes_thr.Impl;
MON_GEO: thread CASE_Monitor_Geo_thr.Impl;

[kfhoech]

AGREE does not attempt to lift contracts from threads to enclosing processes, nor to processors enclosing processes.

Accordingly, the contacts for the contracts for the processes and processors are almost empty or completely empty. AGREE correctly slices this away as it does not affect the top-level contract.

Presently, one must manually write the lifts by copying the contracts from the threads to processes and modify them appropriately for the process scope. Likewise, this must also be done for the processes to the processors.

Thomas did some work on lifting contracts a couple of years ago. But, this was never completed and is currently stored on the AGREE contract lift branch. My recollection is that the semantics for the lifting were never completed and documented. Nor were the rules for checking the consistency of the lifting with manually written contract statements.

[ericmercer]

OK. We need to effectively follow what you did in the async model that composed the system with threads. We can put them in a top process with the contracts in the top process and go from there. Right?

[ericmercer]

Yup. We do exactly what you do in the async model with a process holding the threads
. That is what I was thinking.

Just committed the process version of SW.