A forum for Spin users

You are not logged in.

#1 2011-01-12 18:13:41

Registered: 2011-01-12
Posts: 1

definition of atomic propositions


I have some questions concerning the definition of atomic propositions for the LTL model checking. In a definition I can refer to some label, e.g.

#define eat ([email protected])

holds, if the execution of the process Phil reaches the label Eat.

Now consider a process definition with a parameter, e.g.

proctype Phil(byte id) {

which is run multiple times in an init function. How do I refer to that? I have seen something like

#define eat1 (Phil[1]@Eat)

but I'm not sure what the [1] refers to. It's not the given parameter, maybe the process id?

Also, if I use the former line

#define eat ([email protected])

with a process definition that has multiple instances. How is evaluated whether eat is true of not?

One last thing: when some statements behind the label Eat are executed, does eat still hold until the next label is reached or doesn't it hold anymore immediately after executing the next statement?

Best regards,


#2 2011-01-13 01:01:56

Registered: 2010-11-18
Posts: 694

Re: definition of atomic propositions

Most of the usage guidelines on remote references can be found at the online manpages.
For instance:


A parameter is just like a local variable, so it can be refered to in the same way as a local.

The part in square brackets is the process id (the pid), which is needed if more than one instantiation of a given proctype is running.

The match of the process state on a label only holds when the process is actually paused at that label -- it no longer holds as soon as the process takes another step.


Board footer

Powered by FluxBB