Suppose we have a system consisting a Client, a Device, and a Server. The Client talks to the Device, the Device communicates with the Server. Naturally, we would have 3 TLA+ modules, one for each system component.
What's the best way to compose the modules into a final spec?
One way is to instantiate the Device from the Client module, and the Server from the Device module. But TLC model checker does not deal with existential quantifiers of temporal logic: the Device would have to accept the Server's variables as parameters so that it could pass them to the Server when instantiating the Server module. It means the Device would have to declare variables that it does not use.
In reality, the Device does not need to know about the Server. All it needs to know about is communication channels between the Client and the Server. We can instantiate both the Device and the Server in the Client module, as shown below. In this case the Device does not need to declare Server's variables and accept them as parameters. This makes the spec cleaner. As a bonus, Next step action reminds us at the top level which variables are not used by the Device and by the Server.
What's the best way to compose the modules into a final spec?
One way is to instantiate the Device from the Client module, and the Server from the Device module. But TLC model checker does not deal with existential quantifiers of temporal logic: the Device would have to accept the Server's variables as parameters so that it could pass them to the Server when instantiating the Server module. It means the Device would have to declare variables that it does not use.
In reality, the Device does not need to know about the Server. All it needs to know about is communication channels between the Client and the Server. We can instantiate both the Device and the Server in the Client module, as shown below. In this case the Device does not need to declare Server's variables and accept them as parameters. This makes the spec cleaner. As a bonus, Next step action reminds us at the top level which variables are not used by the Device and by the Server.
From practical point, a module's interface consists of constants and variables that it accepts as parameters, TypeInvariant operator, and the Next step action. In even cleaner approach, we could create a Test module and declare all the required variables there. Then we could instantiate Client, Device, and Server modules from Test module, passing the required parameters. Then we could compose Test's TypeInvariant and Next step action using the instantiated modules. When modules are independent of each other, it is easier to test each module separately as described in this post.
No comments:
Post a Comment