Spinroot

A forum for Spin users

You are not logged in.

#1 General » definition of atomic propositions » 2011-01-12 18:13:41

steffen
Replies: 1

Hi,

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 (Phil@Eat)

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 (Phil@Eat)

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,
Steffen

Board footer

Powered by FluxBB