Evaluating Variable Psets

Prism evaluates the membership of a variable pset when it is defined. If no processes meet the condition (for example, because the program is not active), Prism prints appropriate error messages, but the set is defined.

Subsequently, you can re-evaluate the membership of the pset by issuing the eval pset command, specifying the name of the pset as its argument. For example,

eval pset xon

evaluates the membership of the pset xon. This causes the display for the pset to be updated in the Psets window.

Note that this evaluation will fail if:

• Processes are running that need to be polled in evaluating the pset; or

• The pset's definition contains a variable that is not active in any of the processes being polled

For example, if you issue this command:

define pset foo { x > 0 }

you must make sure that all processes are stopped, and x is active on all processes, when you issue the command

eval pset foo

To ensure that the evaluation succeeds, you would need to use the more complicated syntax described above:

define pset foo stopped && { isactive(x) && (x > 0) }

This ensures that the evaluation takes place only in processes that are stopped and in which x is active.

If an evaluation fails, the membership of the pset remains what it was before you issued the eval pset command.

You can use the eval pset command in event actions; see " Events Taking Pset Qualifiers (MP Prism Only)".

Note the difference between dynamic and variable psets. The membership in both can change as a program executes. Dynamic psets are predefined sets like stopped and interrupted; Prism automatically updates their membership as the program executes. Variable psets are defined by the user, and the user must explicitly update their membership by issuing the eval pset command.