As I understand it:
- Use ordinary assignment to assign the constant a value of any valid TLA+ _expression_ (set of numbers, set of strings, etc.)
- Use model value to assign the constant a value of a singleton object
- Use set of model values to assign the constant a value of a set of singleton objects
So when you run TLC, it creates an object instance for each of your model values. These objects can be checked for equality against each other and nothing else.
Andrew
On Tuesday, August 6, 2019 at 5:30:32 AM UTC-7, LUMING DONG wrote:
Hello, I need to check temporal properties in my spec and the picture below is the input constant value. I heard that we'd better not use symmetry set for such scenario.But I am really confused, what's the result of ordinary assignment below instead of choose Model value?Terminal == <>[] ( \A cli \in SRVLET:/\ CliState[cli] = "work"/\ CliRegState[cli] = "online"/\ (\A m \in CliSubedCache[cli] : m \in CliSubInfo[m[1]]))TCFSInit == /\ C2SMsgQ = [Cli \in SRVLET |-> <<>>]/\ S2CMsgQ = [Cli \in SRVLET |-> <<>>]/\ DataChannel = [Cli \in SRVLET |-> [idx \in SRVLET |-> <<>> ]]/\ CliState = [Cli \in SRVLET |-> "PowerOn"]/\ CliRegState = [Cli \in SRVLET |-> "offline"]