Posts by awesan

awesan · General

hmmm. This is mysterious. I do have the same version. Here is the output of "spin -V" : Spin Version 6.1.0 -- 2 May 2011. I use http://spinroot.com/spin/Bin/spin610_linux on "Linux 3.0.0-12-generic-pae #20-Ubuntu SMP Fri Oct 7 16:37:17 UTC 2011 i686 i686 i386 GNU/Linux". I don't have a 64-bit machine to try it, but I would expect 64-bit to behave the same way as 32-bit. I am not sure whether building spin from sources using any special configuration parameters is required to get the simplification on LTL formula.

awesan · General

Nope. I tried that first; they are different for "spin -f". That's why I had to verify both claims to look at the output statistics. However, the never claims are same for "ltl2ba". Here is the output for both converters:

user : spin -f '!([] ((p -> !q) && (q -> !p)))'
never  {    /* !([] ((p -> !q) && (q -> !p))) */
T0_init:
	if
	:: (! (((p -> !q) && (q -> !p)))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

user : spin -f '!([] (p -> !q))'
never  {    /* !([] (p -> !q)) */
T0_init:
	if
	:: (! ((p -> !q))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

user : ltl2ba -f '!([] ((p -> !q) && (q -> !p)))'
never { /* !([] ((p -> !q) && (q -> !p))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (p && q) -> goto accept_all
	fi;
accept_all:
	skip
}

user : ltl2ba -f '!([] (p -> !q))'
never { /* !([] (p -> !q)) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (p && q) -> goto accept_all
	fi;
accept_all:
	skip
}

Well, they are the same if the formula inside the "if" condition is expanded. It is just not obvious symbolically.

awesan · General

Got it. Thanks. Just curious. In this particular example, is there a way to find out whether SPIN has done simplification of "p0a"? If the number of states stored, matched, transitions, memory usage, etc info reported by SPIN are exactly identical for both "p0a" and "p0b", does that indicate SPIN has reduced "p0a" to "p0b"?

awesan · General

The following two claims are the same as (p -> !q) and its contrapositive (q -> !p) are equivalent in the propositional logic.

ltl p0a  { [] ((p -> !q) && (q -> !p)) }
ltl p0b  { [] (p -> !q) }

However, when I see the "never" claim (using spin -f), I do not see the simplified claim for "p0a". I am curious whether SPIN internally simplifies p0a to p0b before verification or it is user's responsibility to simplify claims?

awesan · General

I see a list of static analysis tools at http://spinroot.com/static/. I have used the old generation of tools such as lint. But looking at the description/white-papers on the newer generation of tools such as CodeSonar and Coverity, it looks like they seem to do whole program analysis that finds errors such as deadlocks. They also seem to allow annotations to check temporal properties per their white-papers and allow calling into the IR (Intermediate Representation) to check more user-defined properties in the whole program analysis. Though I have not personally used these tools, if they work like a charm (I guess users may have to do with false positives to some/great extent), then it would alleviate some burden of using model checkers such as SPIN and UPPAAL. With model checkers, though learning the model checker and using it is one aspect, accurate mapping of the model to the actual program in languages such as C++, Java could be tricky and challenging and a bigger challenge would be to maintain the model as the actual program changes through different releases and patches. So, I am wondering what the gaps/advantages are in using the tools such as CodeSonar and the model checkers? What are the advantages of the model checkers that even the new generation of code analysis tools have not achieved (and they cannot possibly achieve or very hard to achieve)?

awesan · General

Q-1:
As I was reading property-based slicing and experimenting the same with SPIN, the following question arose in my mind (though I have not run into this situation). If SPIN reports the same lines of source code as redundant for all the LTL properties that are intended to be verified in the model, does that imply that those lines of source code are "completely provably irrelevant" in the model and thus the model can be simplified by removing those lines? If the answer is "no", then I assume that the user has to pay close attention to the lines of source code reported as "redundant" by SPIN and see logically whether they don't make any sense in the model and remove them, if it would be appropriate to do so. What led me asking this question is the following text in page-232 (Chapter-10) of the SPIN book : [quote] [b] Although, this method (property-based slicing) can be shown to preserve both logical soundness and logical completeness of the correctness properties that are used in deriving the abstraction, it does not necessarily have these desirable properties for some other types of correctness requirements that cannot be expressed in assertions or in LTL formulae. An example of such a property is "absence of deadlock". Note that the introduction of extra behavior in a model can result in the disappearance of system deadlocks.[/quote] [/b]

Q-2:
From the above text quoted from the book in Q-1, this question follows : "If a simplified model (simplified by removing the lines of code and variables based on the redundancies reported by SPIN's property-based slicing) is verified for the corresponding LTL properties (and assertions) and also the "safety" properties, could the original model suffer from "deadlocks" even if the simplified model does not report any "deadlocked states"?

Q-3:
SPIN reports the message "spin: no redundancies found (for given property)" only once for a model that has multiple LTL properties defined in the model. Does SPIN apply the property-based slicing algorithm for each LTL property separately or does it apply for all the LTL properties together? The reason I ask this is that it reports only once but the message says "for given property".

awesan · General

I don't have one. But, you can write a simple one that does the following: Proc-1 acquires mutex-A and mutex-B. Proc-2 acquires mutex-B and mutex-A. If you try to model this in SPIN, yes, SPIN indeed will throw an error when you verify the model for safety (and you can replay the error trail to see - where two processes are - causing the deadlock). If your intent is not to use embedded C or model extraction from C program, you can directly model this in PROMELA and try SPIN on it.

awesan · General

Interesting and thanks. I will check this out, when I get a chance.

awesan · General

I see that the shell script "_modex_.run" that gets created by modex is hard-coded to use "spin4". Well, I can fix that to use "spin" (which is the latest SPIN tool). However, I am wondering whether it is up-to-date in being compatible with the latest SPIN.

Also, can I run "modex" on a C source file in a large project and will modex simply ignore the functions that are called which are found in other source files? The interesting aspect of the C source file is that the actual state machine that I would expect to be extracted is self-contained in that single file. The reason I am asking is that I have to do quite some work to actually compile that single source file and I wanted to know the scope of modex, if possible, before delving into this much. Thanks in advance.

awesan · General

Hello,

http://cm.bell-labs.com/cm/cs/what/timeedit/index.html

I cannot find cannot find the timeline editor (timeedit?) software online. I have also checked the web-site that is provided at the bottom of the web-page mentioned above. Any idea where I can find it? Also, is that tool still up to date and compatible with the latest SPIN and still used? Thanks in advance.
PS: Similarly, I cannot find the eqltl converter also online.

awesan · iSpin related (GUI)

It would be nice to allow a session file as a command-line argument to iSpin that will restore the session in the session file.

awesan · Bug Reports

Thanks for the quick response. As a user, I would recommend at least getting a warning/prompt in one or both of the following actions:
1. While restoring a session after a file is modified outside iSpin: prompt the user whether he wants to reload the file from disk
2. Saving the buffer to the file (File -> Save) after restoring the session, if the file was modified outside iSpin : prompt the user whether he wants to still overwrite the file, since it was modified outside iSpin and suggest File->SaveAs and choose a different file.

The reason is the following:
That I can think on top of my head, most of the programming language IDEs that allow creating/saving projects/solutions (similar to iSpin session) store only the config data and not the actual source files into the project/solution file itself and the current behavior of iSpin may not be based on the principle of least surprise for some/most users (who typically are used to programming language IDEs and try iSpin), IMHO. Since the cost of this could be really high for users, an extra prompt for a GUI user might not be too annoying (a config option to suppress that would not be a bad idea but the default should be to prompt), again, IMHO.

awesan · Bug Reports

Steps to reproduce the issue:
1. Launch "iSpin x.pml"
2. In "verification tab", choose a few options to verify (for ex, -n, -q for the verifier)
3. Save session
4. Close iSpin
5. Open some other editor and modify x.pml and save it and close it
6. Launch iSpin
7. Restore the saved session
8. The file (x.pml) is opened without modifications done in Step-5. It looks like it happens because the entire model is stored in the session file and not just the file name.
9. File -> Save overwrites x.pml and all the modifications done in Step-5 are lost silently. ( I usually modify the file in iSpin very minimally, like enabling one or two compiler directives/macros, since that is not currently allowed by iSpin in the simulation tab. That's how I ended up modifying the file and saving it in iSpin)

I literally lost all the changes to the model because iSpin did not prompt any errors but overwrote the contents silently. First of all, until I saw the size of the session file, I never guessed that the model was saved in the session. I expected and assumed the iSpin session to remember the file by the path name and then reopen it. I think it would make sense to store the model in the session file only when a model is written in iSpin and the user plays with the model without saving the model to a physical file. In that case, the model can be stored in a temp file by iSpin and also the contents of the file can be saved in the session. If the use-case of exchanging session files (as opposed to session files and the model file whose path might be relative to the current directory) by themselves between users needs to be covered, then after restoring the session, "File->Save" should not be allowed, IMHO. The session file should not remember the file x.pml at all. I thought of proposing prompting the user while restoring the session by checking the time-stamp of the file, etc, but I think that also might be confusing.

awesan · General

It looks like there are mixed definitions for formal verification. Is only "theorem proving / mathematically proving" formal verification? Or, is model checking, using SPIN for instance, also a formal verification technique? Basically, this question is related to a formal write-up.

awesan · General

Hello eugen, How do you get the scrollable box for the source code of the model?

awesan · iSpin related (GUI)

As a matter of fact, "Extra Verifier Generator Options" field under "Verification" tab (like "-DTEST1") does not get passed to spin in "Guided Simulation with Trail" under "Simulate/Replay" also. You can check this by observing the text-box "Background command executed". This could be very confusing, since "Replay" actually uses a different model (without the preprocesor directive like "-DTEST1" passed to it) than the one verified with that directive. I get weird errors like "transition failed" on replaying the error trail. So, for now, if using iSpin, it is a good idea to refrain from using "Extra Verifier Generator Options" and define the directive directly in the model (for instance, #define TEST1 1). Or, use "command-line" spin directly and do NOT forget to pass the preprocessor directive while replaying the error trail also.

awesan · iSpin related (GUI)

In "Simulate/Replay" tab, if a file already exists and I click "browse" button and choose a file, I would expect the existing file name (or path name) to be cleared and the path name of the newly selected file to be entered. However, the existing contents of the text-box are not cleared.

awesan · iSpin related (GUI)

The options that I pass to "Extra Verifier Generator Options" field under "Verification" tab (like "-DTEST1") does not work in random or interactive simulation mode under "Simulate/Replay". I have to either modify these definitions in the model every time or go command-line. It would be nice either to add an extra field for "Extra Verifier Generator Options" in "Simulate/Replay" tab or allow the ones chosen in "Verification" tab to be effective for simulation. People might think former might be ideal and more intuitive but the latter is equally acceptable for me.

awesan · General

I misspoke. By "random-receive boolean function", I meant "random-poll". I am not quite "SPIN"ning right yet

Thanks for looking at the change log. Given the fact that "else" can be combined with "len", I can define the following macros and use these instead of the built-in "empty" and "nempty" and this would allow me to keep the model more crisp and terse. So, I can use "else" on all channel poll's and empty/nempty conditions, which is sweet.
************************************************
#define _empty(_ch) (len(_ch) == 0)
#define _nempty(_ch) (len(_ch) != 0)
************************************************
I am happy with this work-around. If you choose to make it consistent, I would recommend allowing "empty" and "nempty" to be combined with "else" than disallowing channel poll, if there are no strong reasons to do the other way around.

Thanks again for all the help.

awesan · General

Please look at the following PROMELA fragment:
****************************************
do
:: state == A ->
if
:: chx?? [id] ->
chx ?? id ->
ch1?msg;
:: else -> skip; // SPIN does NOT throw syntax error
fi

:: state == B ->
if
:: some_condition_1 -> ....
:: some_condition_2 -> ....
:: nempty(ch1) ->
ch1?msg;
:: else -> skip; //SPIN throws syntax error : dubious use of 'else' combined with i/o, saw 'token: ::'
//SPIN reports error at line number that has " :: state == C ->" which is a few lines below, instead of at the line above. Seems to be a minor BUG.
fi

:: state == C ->

od;
****************************************
Q-1. As mentioned in the comments, SPIN accepts "else" on a random-receive boolean function but throws syntax error on a boolean function "nempty". It looks a bit inconsistent to have different behaviors on these two cases and it would be more clear if the behavior is consistent one way or the other. I see in the documentation that !empty is not allowed and that's why SPIN has both empty and nempty. If that is the reason for syntax error on "else" case, that sounds reasonable. However, it does limit one from using "else" in an "if" statement that has several conditions with one of them being "nempty" on a channel. I understand that the model can be written with some extra lines of code and checks and worked-around, but it would be a syntactic sugar to allow "else" in an "if" statement that has "nempty" as one of the conditions, even though !nempty is not allowed by SPIN. I think it is possible that this is done for all valid reasons and limitations by design and implementation.

Q-2. The line number reported by SPIN for the syntax error "dubious use of 'else'" is incorrect as mentioned in the comments. Again, it is not a big deal and I can obviously easily spot the offending line and fix it. However, if you would like to fix this and cannot reproduce this, please let me know.

awesan · iSpin related (GUI)

When you do Alt+tab or go to the launcher bar, it would be nice to have an icon for iSpin (personally spinroot icon is good) to identify it. Now, I see a "?" in the icon. I think, if more than one application is without an icon, then it might be confusing. Just a thought..

awesan · General

Thanks very much Dr.Holzmann for the quick response and the solution. I did verify that your claim verified without errors. I replaced "l2" with "l1" in the never claim and it also verified without errors and since "rel_sem" does not block, I thought that would be a good and sufficient test. I have a few questions:

Q-1.
I tried to come up with a few never claims myself and I either got verification errors or no verification errors. But, when there was no verification error, I was not convinced that I wrote the never claim correctly (It was not resembling what you have provided). In the process, for one or two claims, I was certain I got it wrong (since the number of states reported during verification was spectacularly low (like 1 or 2) ). However, when the verification states and transitions seemed to be above 20 and 70 respectively, I could not tell for sure whether I got the claim correctly or not. Mostly, I could reason LTL formulae and simple never claims with confidence that I have got the claim right (and I should fix the model, if errors are reported). However, if the claim itself is tricky (like this one) and there is no verification error, I am just not sure whether I am verifying what I intending to verify. If you don't mind, could you please explain briefly how you came up with this claim? Especially, I did not understand how and why you got the "accept" label in the middle. When labels l0 and l2 (or l0 and l1 in the never claim written with replacing l2 by l1) point to different states, is the check for "P@l2" not redundant in the condition "P@l0 && !(P@l2)"?

Q-2.
I get the following warning:
*******************************************************************************************
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
*******************************************************************************************
Do I need to make sure that the never claim is "stutter-invariant", if I write a never claim and not use LTL as in this case? Is there a way to do it?

Q-3.
My google-search did not find one. Is there a never claim to LTL converter? (I see we can do the other way around obviously). Or, is it not theoretically possible (forgive my ignorance)?

Q-4.
iSpin threw the following error when I tried to click on "claim_never_0" to view the state diagram. However, I could create the .dot file and .ps file from command line and use a ps file viewer. So, not a big deal. However, if you want to fix it, here is the bug report.
*******************************************************************************************
unexpected "," outside function argument list
in expression "50 * 1, height="
unexpected "," outside function argument list
in expression "50 * 1, height="
(parsing expression "50 * 1, height=")
invoked from within
"expr 50 * $mf"
(procedure "find_field" line 10)
invoked from within
"find_field "width=" $line"
(procedure "display_graph" line 129)
invoked from within
"display_graph claim_never_0"
(command bound to event)
*******************************************************************************************
Thanks again for your time and help.

awesan · General

Hi there,
Thanks again for all the help so far. I have a question about verification for strong fairness in the following model :
**************************
inline acq_sem(sem)
{
atomic {
sem > 0 ->
sem--;
}
}

inline rel_sem(sem)
{
sem++;
}

#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;

active proctype P()
{
end:
do
::
skip; // in order to specify label l0 inside the loop
l0:
acq_sem(sem);
l1:
rel_sem(sem);
l2:
skip;
od;
}

active [2] proctype Q()
{
end:
do
:: acq_sem(sem);
rel_sem(sem);
od;
}
ltl p1 { [] (sem >=0 && sem <= MAX_SEM_VAL) }

ltl p2 { [] (P@l1 -> <> P@l2) }

ltl p2a { [] (P@l0 -> <> P@l2) }

ltl p2b { ([] <> P@l0) -> ([] <> P@l2) }

ltl p2c { (<> P@l0) -> (<> P@l2) }

**************************
I see that "p2a" fails when it is verified for acceptance cycles with weak-fairness constraint enforced whereas "p2" passes. This is due to the fact that P@l0 does not remain continuously executable(enabled) whereas P@l1 remains continuously executable thus satisfying the weak fairness constraint. So far, so good. Now, I want to express strong fairness constraint through LTL and my attempt is "p2b". P@l0 would be enabled infinitely often but not continuously enabled and hence I expect P to acquire semaphore eventually. However, acceptance cycle verification fails. I tried "p2c" though it does not look quite correct to me, but it also fails on verification for acceptance cycles. Can strong fairness for this example ("If P tries to acquire semaphore infinitely often and the other processes do release semaphore such that P@l0 becomes "enabled" infinitely often, it will eventually acquire the semaphore") be specified using LTL? Or, do I need to write a "never" claim for this? Thanks in advance.

awesan · General

My assumption - not selecting "weak" is "strong" - is pretty bad. Thanks for the explanation. Your prompt response keeps me getting farther in understanding model checking. Thanks very much again.

awesan · General

I found the definitions for Absolute Fairness, Strong Fairness and Weak Fairness from the following URL interesting : http://www.ccs.neu.edu/home/wahl/Publications/fairness.pdf
I guess SPIN supports "Strong Fairness" (-l option and not -f option for pan) and "Weak fairness" (-l and -f options for pan). Is that right? Or the definitions above are different from SPIN's definition of fairness? Thanks in advance.

Spinroot

#1 Re: General » Does spin reduce redundancies in LTL claims internally? » 2012-04-16 04:00:10

#2 Re: General » Does spin reduce redundancies in LTL claims internally? » 2012-04-16 00:29:10

#3 Re: General » Does spin reduce redundancies in LTL claims internally? » 2012-04-15 08:00:26

#4 General » Does spin reduce redundancies in LTL claims internally? » 2012-04-15 00:49:43

#5 General » Static/Dynamic analysis tools vs model checking tools » 2012-01-23 04:41:49

#6 General » Questions on property-based slicing in SPIN » 2012-01-16 02:25:04

#7 Re: General » example program in C language which have deadlock » 2012-01-12 06:48:22

#8 Re: General » modex on a C source file in a large project? » 2012-01-04 23:22:11

#9 General » modex on a C source file in a large project? » 2012-01-01 05:22:26

#10 General » cannot find timeline editor software (timeedit?) online » 2011-12-23 20:35:30

#11 iSpin related (GUI) » Allow session name as a command-line argument to iSpin » 2011-12-22 07:25:35

#12 Re: Bug Reports » iSpin overrwrites the model file after restoring session silently » 2011-12-22 07:20:39

#13 Bug Reports » iSpin overrwrites the model file after restoring session silently » 2011-12-22 02:55:08

#14 General » Is model-checking a formal verfication technique? » 2011-11-30 04:39:47

#15 Re: General » acceptance cycles » 2011-11-30 04:35:34

#16 Re: iSpin related (GUI) » Extra Verifier Generator Options does not work in simulation mode » 2011-11-25 05:32:22

#17 iSpin related (GUI) » Existing path/file name is not cleared when a browsed file is selected » 2011-11-24 07:22:06

#18 iSpin related (GUI) » Extra Verifier Generator Options does not work in simulation mode » 2011-11-20 02:41:38

#19 Re: General » SPIN reprots "dubious use of 'else' combined with i/o" but not always » 2011-11-20 02:34:57

#20 General » SPIN reprots "dubious use of 'else' combined with i/o" but not always » 2011-11-19 22:20:32

#21 iSpin related (GUI) » An icon for iSpin would be nice » 2011-11-18 18:55:23

#22 Re: General » strong vs weak fairness in SPIN » 2011-11-18 03:09:13

#23 Re: General » strong vs weak fairness in SPIN » 2011-11-17 07:53:58

#24 Re: General » strong vs weak fairness in SPIN » 2011-11-14 00:37:33

#25 Re: General » strong vs weak fairness in SPIN » 2011-11-13 05:27:41

Board footer