Spinroot

A forum for Spin users

You are not logged in.

#1 2011-05-10 10:55:42

rangu
Member
Registered: 2011-01-03
Posts: 6

unreachable state in leader election algorithm

sir, when i was verifying Leader Election Algorithm given in Exercise.html [ [url]http://spinroot.com/spin/Man/Exercises.html[/url] ] it is saying that
     unreached in proctype node
    leader:48, state 28, "out!two,nr"
i don't understand why it is saying this or is their anything missing in specification?

Offline

#2 2011-05-10 15:29:41

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

Re: unreachable state in leader election algorithm

that's correct -- it is an unreachable statement
that's of course what spin is designed to do: find the flaws in a model

Offline

#3 2011-05-10 17:06:55

rangu
Member
Registered: 2011-01-03
Posts: 6

Re: unreachable state in leader election algorithm

then for removing this flaw or to make model of leader election correct what i have to do?
Is their any correction for this?

Offline

#4 2011-05-10 17:25:39

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

Re: unreachable state in leader election algorithm

that's not anything that i can help you with
spin is designed to find errors, only you as the user or as the designer of the algorithm that you are verifying, can decide how to fix the errors that spin finds...

Offline

Board footer

Powered by FluxBB