Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2011-03-09 10:56:56
- ines.md
- Member
- Registered: 2011-03-08
- Posts: 7
Spin verification cycle
Good morning,
Does the spin verify cycles, ie does it verify Termination property in case of cycles?
And can it veify the Livelock property?
Thanks
Offline
#3 2011-03-14 12:05:08
- ines.md
- Member
- Registered: 2011-03-08
- Posts: 7
Re: Spin verification cycle
So Can it also check the properties of Livelock in the case of cycles?
Offline
#5 2011-03-15 18:18:52
- ines.md
- Member
- Registered: 2011-03-08
- Posts: 7
Re: Spin verification cycle
sorry but what i want to know is, if just to check the "Non-progress" property and verify my model that means the verification of the "Livelock" property in the case of cycle??? or i have to enter a LTL property that exprime the Livelock of my model and then verify?
An other question please: what's the difference of "Acceptance" and "Non-progress" property? are used both to verify the correctness of models in the case of cycle?does "Acceptance" used to verify cyclic models but here we accept cycle and "Non-progress" used to verify cyclic models but spin should takes into consideration the non-progress cycle or to avoid its???
thanks
Offline
#6 2011-03-16 02:57:19
Re: Spin verification cycle
there are no quick one sentence answers to the questions you ask
please study the tutorial material or read the textbook that explains the context for logic model checking, and you'll understand much better how things work
a non-progress property is a special type of an acceptance property, where acceptance refers to Buchi acceptance (a form of omega acceptance).
ltl properties can express a subclass of properties that can be checked with Buchi automata.
your questions go deeper though and i recommend that you go through the material on the website that was prepared to give you a better insight in the verification process
Offline
Pages: 1