Spinroot

A forum for Spin users

You are not logged in.

Pages: 1

#1 Re: General » ter commands by hand in spin?? » 2011-03-16 00:03:03

ines.md

Ok thanks i can now enter command manually smile.
In several documents i found that they type the command "a.out" to execute the Analyzer (verify functioning of our system), "a.out -l" to verify non-progress and "a.out -l -c0" to report all errors. but when i type a.out in the command prompt (Windows Vista) the message: "a.out is not known as internal or external command ..."  is posted. i can't found the cause of this error??

#2 Re: General » Spin verification cycle » 2011-03-15 18:18:52

ines.md

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

#3 General » ter commands by hand in spin?? » 2011-03-14 12:10:38

ines.md
Replies: 3

Please in which version of spin (jspin or  Xpin) I can enter commands by hand
exp: spin -t -p Hyman

#4 Re: General » Spin verification cycle » 2011-03-14 12:05:08

ines.md

So Can it also check the properties of Livelock in the case of cycles?

#5 General » Spin verification cycle » 2011-03-09 10:56:56

ines.md
Replies: 5

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

#6 Re: General » Signification of the counter-example (file .trail) » 2011-03-09 10:06:52

ines.md

Why and in which cases we find negative numbers? especially for the number of stages and the number of transitions?? especially for the number of steps and the number of transitions?

It's Not Meant to Be human readable. Why?
I am trying to develop a tool to model workflow net, translate language Promela and finally check whether the workflow net I modeled verif the 3 properties: termination, propre termination and Liveliness (here comes the spin's role ).
In the case where a property is not checked, the counter-example shown to the user. What I looking for is to decode the counter-example to be readable and understandable by any user.Is it possible to do this? if it's possible, can you help me to do it Please?

Thus, when a property is not verified, can we correct our model, based on the counter-example, to verify that the property is well checked?

#7 General » Signification of the counter-example (file .trail) » 2011-03-08 17:04:37

ines.md
Replies: 3

Good morning,
When you get an error checking, an counter-example is created  (file .trail), it contains 3-numbers (positive or negative) in each of its lines, separated by a colon ":".
I can not understand what expresses each of these three number???

Thank you

Pages: 1

Board footer

Powered by FluxBB