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