AGREE Feature Request: Better support for multiple fan-in to single input port

[jendavis]

In publish-subscribe architectures such as UxAS, there are several instances of multiple fan-in to a single input port. I've pushed a simple (non-UxAS) example here:

https://github.com/loonwerks/formal-methods-workbench/tree/master/models/agree/multiple-fan-in-to-port

If one tries to run analysis on the MutlipleFanInToPort model without using AGREE connections, a helpful error message is provided (this is good):

It would be even better if some automation could be provided to help the user resolve the error. For example, uncommenting the AGREE connections and assert statement shown in the image above allows the user to then run analysis and prove the lemma shown (leveraging the guarantees on A and B, which are not shown in the image but are included in the model).

Perhaps the model itself could be transformed; or, as perhaps a safer alternative, the tool could generate some suggested text for the user to add to the model. The AGREE connection statements are probably the only "safe" thing to add since the user may or may not want to assume that the input is equal to one of the current values from the two sending components (think queues).

This is more complicated for event data ports but still very important. See MultipleFanInToEventPort.aadl.

The fundamental issue is that these pub/sub architectures use queues all over the place, and we don't have good (any) support for that in the tool suite. I understand this is a significant challenge; so, instead of saying "Please support queues," I'm suggesting a middle ground to automate at least some of the easy stuff like AGREE connections to resolve the initial error. Maybe this could even be a preference the user sets, and the requisite AGREE connections are generated under the hood (invisible to the user).