[tlaplus] Generalizing the initial configuration

["p.to...@xxxxxxxxxxxxxxxxx" <p.tollot@xxxxxxxxxxxxxxxxx>]

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.