Spinroot

A forum for Spin users

You are not logged in.

#1 2017-07-21 16:18:43

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Proctype priorities and partial order reduction

Hello everybody,

I have a two questions regarding priorities of proctypes in Spin.
* The manpage on priorities (http://spinroot.com/spin/Man/priority.html) concludes with the remark that "for a full verification partial order reduction should be disabled". What confuses me is the "should" in the remark. My question is: are there any potential errors that I might miss in my model if I use proctype priorities in combination with POR?
* What does "full verification" mean in this context? The behavior that a low-prio proctype cannot execute a statement if a higher-prio proctype can execute some statement is absolutely intended in my model and also guaranteed by the system that shall be verified. It is clear, however, that the verification would not capture the entire statespace if the priorities weren't enforce in the verified system.

Cheers,
Christian

Offline

#2 2017-07-21 17:31:24

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Proctype priorities and partial order reduction

Q1: yes, the priority mechanism isn't consistent with POR
in practice though you will still find counter-examples, but
if there are none, that doesn't mean that there are none if POR is
enabled and you use priorities
Q2: the priorities would still be enforced, with or without POR.
the only issue is the completeness of the verification under POR
with the priorities being enforced -- so it's best for a final check to
then disable POR

Offline

#3 2017-07-28 07:13:19

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Re: Proctype priorities and partial order reduction

Thanks for your quick answer.

Just out of curiosity, what is the reason for POR being incompatible with proctype priorities and also with provided clauses? It seems to me that provided clauses only contribute as additional guards to the transitions of the underlying automaton, which occurs to me as being quite similar to an if-statement with a conjunction of conditions in each option. But that's probably to simple :-).

Offline

#4 2017-07-28 17:56:00

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Proctype priorities and partial order reduction

True, they are additional guards, but they are not evaluated
for their global or conditional safety under the POR rules, so these
additional clauses could introduce dependencies that are not
tracked, which makes the POR potentially invalid

Offline

Board footer

Powered by FluxBB