Re: [tlaplus] Assign tuple to a constant

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

the values allowed in configuration files are indeed quite limited (see “Specifying Systems” for the precise syntax). You need to define a constant in the TLA specification, e.g.

MyTuple == << 1,2,3 >>

and then assign MyTuple to the constant. The Toolbox does the same for you behind the scenes, look at the module MC.tla in the toolbox directory created for your specification.

Regards,
Stephan


> On 1 Mar 2018, at 20:10, Affan Qureshi <affan.qu...@xxxxxxxxx> wrote:
> 
> Hi,
> 
> I have written some TLA+ specifications that use constant tuples. I am able to assign a tuple e.g. ` << {1}, {2}, {3} >> ` to a constant in the toolbox (works as expected). But when I try to do the same in a config file for the command line tools e.g. ` CONSTANT Someconstant =  << {1}, {2}, {3} >> ` I get the following error:
> 
> TLC found an error in the configuration file at line (tuple assignment line)
> It was expecting = or <-, but did not find it.
> 
> So I would like to know if and how a tuple can be assigned to a constant in the config file.
> 
> The motivation for using the command line tools is that I would like to automatically generate different config files and use them to check the model. Any suggestions for doing this with the toolbox will also be helpful.
> 
> Thanks,
> Affan
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.