On Tuesday, February 2, 2016 at 3:57:03 PM UTC+2, Nira Amit wrote:
Hi Ron,
1. I didn't know that about Strings, thanks for pointing it out.
2. Regarding your suggestion: I was thinking about returning a message as you described, but couldn't find a way to make it work. If CreateGossipMsg(peer) is the set of all possible gossip messages then it quickly becomes too big for TLC to calculate.
I don't think you need to return the set of *all* possible gossip messages. If your original spec was:
CreateUpdate(peer) == \E eid \in ENTITY_ID, v \in ENTITY_VAL:
message' = [message EXCEPT ![peer] =
[mtype |-> Gossip,
mid |-> msgCounter,
mbody |-> CreateEntity(peer, eid, v),
msrc |-> peer]]
your revised one can be:
CreateUpdate(peer) = { [message EXCEPT ![peer] =
[mtype |-> Gossip,
mid |-> msgCounter,
mbody |-> CreateEntity(peer, eid, v),
msrc |-> peer]]
: eid \in ENTITY_ID, v \in ENTITY_VAL }
The number of states you'll create is the same as in your original spec, but you're right that TLC can only handle sets much smaller than the number of states it can handle. Note, however, that you can set the size of the maximal set in the "Cardinality of largest enumerable set" option in the model's Advanced Options tab.
Ron