[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Assign tuple to a constant


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.


> 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.