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

Re: [tlaplus] "Final" action to check hyperproperties ?



On 02.06.20 03:58, dp.simplexum@xxxxxxxxx wrote:
> 
> In the diff you linked to, I see some calls to TLCGet with string
> arguments. Do I understand correctly that the string arguments to
> TLCGet/TLCSet reserved only for internal values like number of states,
> and for ordinary use, integer slot numbers should be used ?


Yes, TLCSet(i,v) only accepts (positive) integers for the i parameter
(see 2.2.2 of [1]).

Markus

[1] https://lamport.azurewebsites.net/tla/current-tools.pdf

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e7c541d0-6937-2b86-aaa3-6e9e79b222ad%40lemmster.de.