Re: [tlaplus] Generalizing the initial configuration

Hello,

I am assuming that your task is to verify the executions of the system in its different configurations, rather than just static properties of these configurations. The basic idea is then to define your initial predicate as a conjunction of formulas of the form

var \in ValidInitialStates

where the set ValidInitialStates characterizes the initial values of variable var in these initial configurations.

For a simple example, look at EWD840 [1] where almost all variables can take arbitrary (type-correct) values.

Hope this helps,

Stephan

[1] https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840.tla

On 10 Jun 2021, at 10:51, p.to...@xxxxxxxxxxxxxxxxx <p.tollot@xxxxxxxxxxxxxxxxx> wrote:

Hi, i have to check a distributed system, in which different services are deployed in different machines, and there can be more than one service per machine with the constraint that services of the same kind can't be deployed in the same machine.
What i want to do is to do TLC check for all and only the possible valid configuration, i would use a structure where the values are sets (the set of service deployed for that machine), would you have any suggestion on ho to define all the possible configurations and then filter them only with the valid ones? I saw the ASSUME keyword only works with constants, i would need something similar that works also for variable i think.

Thanks,
Pietro

--
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/10c0ed3c-a6e9-4f27-bdba-ce43f3ab04a3n%40googlegroups.com.

--
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/13F08E3B-4935-4FFE-82C0-817E388103C2%40gmail.com.