Sets can be used in agent definitions (restriction or synchronous merge), and in propositions (modalities). The situation becomes slightly complicated, because agent definitions notionally mention sets of names, whereas modalities genuinely contain sets of actions. If you give an action set in an agent definition explicitly, by listing its members, the CWB will prevent you from listing actions other than names and conames. However, if you use a set identifier, it cannot do this. (Sets, like other CWB entities, are bound dynamically, so at any stage you might change the contents of the set mentioned in the agent definition.) Therefore if you do use actions other than names and conames in an action set used to restrict an agent, they will simply be ignored.

It wouldn't make (much) sense for a set used to restrict an agent to contain the special actions eps or tau; really it's better to think of restricting a set of names. Therefore in the CWB you may not define a set identifier to contain eps or tau. If you want to use tau in a modality, you have to write the modality using an explicit list of actions, rather than using a set identifier.

SETS{ a,... }action set (not including eps or tau)
Vset variables begin with upper case


Edinburgh Concurrency Workbench (v7.1). Page generated: Sat Jul 17 22:16:15 BST 1999