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

[tlaplus] About ordinary assignment



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"]



捕获.PNG


--
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/c8ec1d1c-b08a-4169-9c08-7dde3d85756b%40googlegroups.com.