Usage of brackets in TLC config file

25 views
Skip to first unread message

Willy Schultz

unread,
Aug 18, 2021, 4:18:30 PMAug 18
to tlaplus
Is anyone familiar with the usage of brackets in a TLC config file as seen here? I have not encountered it before, and am unclear on its semantics. As far as I can tell, I don't see an explicit mention of it in Specifying Systems.

Markus Kuppe

unread,
Aug 18, 2021, 4:56:47 PMAug 18
to tla...@googlegroups.com
On 8/18/21 1:18 PM, Willy Schultz wrote:
> Is anyone familiar with the usage of brackets in a TLC config file as
> seen here
> <https://github.com/tlaplus/Examples/blob/15df8dd25e1a41fdc17f4aa79618d13dfd6e2b36/specifications/Paxos/MCPaxos.cfg#L9>?
> I have not encountered it before, and am unclear on its semantics. As
> far as I can tell, I don't see an explicit mention of it in Specifying
> Systems.

Hi Will,

Voting and Paxos both define a Ballot operator. Without the brackets,
MCPaxos.cfg override the definition of Ballot in Paxos (done a few
lines above in the .cfg), not in Voting. This feature was added in
2009. In other words, after the release of Specifying Systems.

The screenshot shows the Toolbox does the same.

M.
Screenshot from 2021-08-18 13-53-53.png

Willy Schultz

unread,
Aug 18, 2021, 5:13:19 PMAug 18
to tlaplus
Interesting, thanks! This is more or less what I figured. It turns out this is a feature I was recently needing, which is why I was curious. That is, I needed to override an operator in an auxiliary module that was instantiated by the "main" spec being parsed by TLC, and needed the bracket syntax to refer to an operator inside the auxiliary module from a config file. 
Reply all
Reply to author
Forward
0 new messages