All messages now have a message type. Modules must statically
declare what message types they may receive. Unreceivable message
types are checked for when a message is sent. Current behavior when
finding an unacceptable message type is crashing.
To make this commit smaller, I added an "Unchecked_Type" which
modules can pass when registering themselves to avoid specifying
their types. I will remove this in future commits.
I went through all the API files and added the message type to all
encoder and message type checker functions.
In this commit, I slightly change how Module IDs are used. A module
ID now refers to a type of module, with the thought being that one
module type may be present in multiple domains. This resolves an
ambiguity in how messages type is inferred in the inter-domain case.
More can be read about this decision immediately in the Eric's Notes
document and later when I write a proper rational for this refactor.
Merc will need minor modifications to generate the appropriate API
files.
Note that it is not yet possible to formally prove messages will
be send to acceptable receivers. I also still haven't SPARK proved
any of this refactor.
I've also added a test to verify the message system is filtering
messages appropriately. It is now possible for receiving modules
which specify appropriate message types to receive to stop
checking for unacceptable messages.
All messages now have a message type. Modules must statically declare what message types they may receive. Unreceivable message types are checked for when a message is sent. Current behavior when finding an unacceptable message type is crashing.
To make this commit smaller, I added an "Unchecked_Type" which modules can pass when registering themselves to avoid specifying their types. I will remove this in future commits.
I went through all the API files and added the message type to all encoder and message type checker functions.
In this commit, I slightly change how Module IDs are used. A module ID now refers to a type of module, with the thought being that one module type may be present in multiple domains. This resolves an ambiguity in how messages type is inferred in the inter-domain case.
More can be read about this decision immediately in the Eric's Notes document and later when I write a proper rational for this refactor. Merc will need minor modifications to generate the appropriate API files.
Note that it is not yet possible to formally prove messages will be send to acceptable receivers. I also still haven't SPARK proved any of this refactor.
I've also added a test to verify the message system is filtering messages appropriately. It is now possible for receiving modules which specify appropriate message types to receive to stop checking for unacceptable messages.