A forum for Spin users
You are not logged in.
Thanks for help! I solved the problem. I use 7zip to unpack the .gz file. After the first extraction, the file appears an exe file, but is actually not. I have to extract the unpacked file again with 7zip and then the new file is indeed an exe file. Perhaps my experience is helpful for other Windows users.
When I open iSPIN by Wish, an error message box pops out. Here is the copy of the first a few lines.
can't read "fd": no such variable
while executing
"if {$fd == -1}{
puts "$errmsg"
exit 0
} else {
set version "Spin Version unknown"
if {[gets $fd line] > -1}{
set version "$line"
..."
.................
}
I have problem to run SPIN6.4.7.
I have been using SPIN for almost 10 years. My current working installation is SPIN6.4.6 32 bit for Windows. I am using 64 bit Windows 7 and MINGW32. I downloaded SPIN647_windows32, but it doesn't work. I also noticed that the EXE file of spin647 is only 310 kB but the EXE file of spin646 is 1010 kB.
Can you please double check your upload?
Thank you!
How about defining an internal variable, say "bool reached", in each process? The initial value of reached is false. At the begining of the propagation, assign true to the starting process and check if all these variables reached can be eventually true.
Of paramount in effectively using SPIN is to reduce the number of states. In short, a state includes the set of global variables, channels, the set of local variables and process states of the processes, and others. The state space can be reduced if we can reduce the number of any of these elements.
There are many tricks to reduce the sizes of these elements but SPIN does not directly supports them. For example, a process often contains many local temporary variables used to obtain other important results. There variables have no effect on the system properties. For example, the following is a code section for finding the maximal element in a data array of size 10.
x_max = x[0]
for (i : 1 .. 9)
{
x_max = (x_max < x[i] -> x[i] : x_max)
}
Evidently the local variable i needn't be counted in the system state. Does SPIN have any control to suppress i from the system state? I know that this is possible for global variables with the "hidden" prefix, but can we do the same thing for local variables?
Another trick is about the process states. If a process contains a long sequence of serial operations without branch or cycle, i.e., the incoming and outgoing transitions at every state are both 1. Graphically, these states construct a simple chain of operations. Then we don't need to record all these process states in the set of visited states, because they may not be repeated in the future.
More general, we only need to remember the process states which have either multiple outgoing transitions or multiple incoming transitions. Only these process states need to be recorded in the visited states set, because if the system model revisits a visited state, it must enter those with multiple incoming transitions.
This principle can be extended to the system with multiple processes. My suggestion is that a markup keyword like "hidden" should be defined for hiding non-critical process states. If the state of a process does not have multiple outgoing or incoming transitions, we can maintain the last such one visited by the process and only store them in the visited state set. Therefore, we can reduce the size the visited states set, which retains all the re-entrant states of the system model.
This is still a fuzzy idea. I hope you can understand and find it helpful for the improvement of SPIN.
The customization of "+minimized automata (slow)" might be buggy.
In the source code of ispin110.tck, at lines 3885 - 3889, the original code is
if {$V_Panel_3} {
if {$ma_mode == 1} { set cargs "$cargs -DMA=[$t.top.right.row4.ent get]" }
if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" }
} else {
}
It seems suspicious to have two if ($ma_mode == 1) consecutively together. My understanding is that the first line reads the input from the text box "Size for Minimized Automaton", and the second one uses the default value (100). If I type 200 in the text box, then the compiler option has two -DMA consecutively, e.g., -DMA=200 -DMA=100.
I boldly change the code as follows. It worked properly. Can you please confirm if my change is valid?
if {$V_Panel_3} # If the text box is modified
{
if {$ma_mode == 1} { set cargs "$cargs -DMA=[$t.top.right.row4.ent get]" } # If the checkbox is selected, use the text box value
}
else
{
if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" } # If the checkbox is selected, use the default value 100
}
I have seen an interview with NASA on how they used model-based verification and testing methods to check the defect of the Toyota software. Do you have the link to that interview?
I remember it was on IEEE Spectrum.
Thank you!
Thanks for pointing that out. Now I see. SPIN indeed explicitly casts everything into int type. All puzzles for me are clear.
I forgot to say that I run Spin with Cygwin. Gcc in Cygwin only supports 32-bit program. So int must be 32 bits in pan.c.
My computer is 64 bit W7, but when compiling the code, I choose the target as Win32. I checked the length of int and unsigned int with sizeof. They are both 4, i.e., 32 bits.
Could you please try to run the C++ code with gcc on a 32 bit machine?
The problem is not just ; you missed = in the declaration of chan.
The syntax of defining channels is wrong in your code. It should be
6. chan AB = [1] of {byte,byte,byte};
7 chan BA = [1] of {byte,byte,byte};
8 chan BC = [1] of {byte,byte,byte};
9 chan CB = [1] of {byte,byte,byte};
If the rule of casting everything to signed integers were correct, a conflict would be what if the operands are unsigned integers and the values are larger than the upper bound of signed integer. I wrote two identical programs in both Promela and C++. The results seem contradictory. I used MSVS 2012 Express for compiling the C++ program.
/****** The Promela code: ***********/
#define LENGTH 31 /* The largest length of unsigned data type in Promela */
active proctype test()
{
unsigned x : LENGTH;
byte abyte=2;
int sum_int;
unsigned sum_unsigned:LENGTH;
x = (1 << LENGTH)-1; /* The value is the upperbound of int, 2^31-1 */
sum_int = x + abyte; /* x+abyte = 2^31+1, exceeds the upperbound of int. sum_int should be negative */
assert(sum_int < 0); /* Spin does not find any error here */
sum_unsigned = x + abyte; /* x+abyte = 2^31+1 exceeds the upper bound of unsigned, but after the truncation the value is still positive. It is 1 actually */
assert(sum_unsigned > 0); /* Spin does not find any error here */
assert(x + abyte < 0); /* Which datatype is the sum if not explicit given? By Spinroot, it is int and should be < 0. By C standard, it is unsigned int and should be > 0 */
/* Indeed, Spin does not find any error here */
}
/*********** End of Promela code *************/
/********** Start of CPP code ***************/
#include <iostream>
using namespace std;
#define LENGTH 31
int main()
{
unsigned int x, sum_unsigned; /* The range of unsigned int is larger than that in Promela */
char abyte = 1;
int sum_int;
x=(1<<LENGTH)-1; /* The value is the upperbound of int, 2^31-1 */
sum_int = x + abyte; /* x+abyte = 2^31+1, exceeds the upperbound of int. sum_int should be negative */
if (sum_int < 0)
cout <<"sum_int is negative! OK!"<<endl;
else
cout << "sum_int is positive! Why?" << endl;
sum_unsigned = x + abyte; /* x+abyte = 2^31+1 is still a valid value of unsigned int. */
if (sum_unsigned > 0)
cout << "sum_unsigned is positive! OK!"<<endl;
else
cout << "sum_unsigned is negative! Why?"<<endl;
if (x + abyte > 0) // If this is true, then x and abyte are not first cast into signed integers. x remains unsigned integer.
cout << "x + abyte is positive! Different from SPIN!"<<endl; //This statement is reached. The computation between Spin and C++ are different!
else
cout << "x + abyte is negative! Same as SPIN!"<<endl;
cin >> abyte;
return 0;
}
/********** End of CPP code ****************/
In book, The SPIN Model Checker: The Primer and Reference Manual, Chapter 3, Section "Assignments and Expressions", a few paragraphs above Table 3.2, a sentence reads
"the values of all operands used in the expression on the right-hand side of the assignment operator are first cast to singed integers, before any of the operands are applied."
I wonder if this rule is specific for SPIN or inherited from C standard. It seems that C/C++ doesn't do the same thing when calculating operands with different data types. C/C++ dynamically promotes the shorter data type to the longer data type during the calculation.
The difference between SPIN and C/C++ may create confusion when building SPIN models.
The similar question was asked before in this forum about using SPIN to evaluate the maximal time delay of wireless network. It turned out that the acronym of SPIN also means Security Protocols for Sensor Networks. Perhaps that is the right SPIN you are looking for.
Currently there are 3 different ways of sending messages to a channel.
1. If the queue is full, the sender is blocked; otherwise the channel is an FIFO queue. For example chan ! x
2. If the queue is full, the sender is blocked; otherwise the channel is a sorted queue. For example chan !! x
3. If the queue is full, the sender is not blocked and the sent message is lost. With the option of -m for SPIN.
In addition to these, another option is necessary in implementation.
If the queue is full, the sender is not blocked and the new message replaces the old one in the queue.
This option is often preferred in systems transmitting data among processes. The most recent data are more important than the older ones.
In implementation, the semantics of this option is similar to a circular buffer data structure.
I might hit a bug in SPIN6.2.3 with the bitstate option. The following is the error message prompted in iSpin 1.1.0. The verification in version 6.2.2 with bitstate on the same model is successful.
My PC is 64 bit Windows 7. I run Spin with Cygwin.
verification result:
spin -a battery.pml
gcc-3 -DMEMLIM=5120 -O2 -DBITSTATE -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
/cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o:pan.c:(.text+0xbfdc): undefined reference to `_o_hash32'
/cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o:pan.c:(.text+0xc15b): undefined reference to `_o_hash64'
/usr/lib/gcc/i686-pc-cygwin/3.4.4/../../../../i686-pc-cygwin/bin/ld: /cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o: bad reloc address 0x20 in section `.data'
/usr/lib/gcc/i686-pc-cygwin/3.4.4/../../../../i686-pc-cygwin/bin/ld: final link failed: Invalid operation
collect2: ld returned 1 exit status
UPPAAL has arrays and is suitable for distributed systems, perhaps no exponential. To have more information please visit uppaal.org.
You can use embedded C code in SPIN and then you may use exponential.
Matlab has a tool box called Simulink Design Verifier, but you need to pay extra money for that.
For real-time model checking, please check uppaal. For complex computations like exponential you may use Matlab or simply a C compiler.
Thanks for sharing. Both tutorials are informative.
I am glad for you because you have made progress for your problem. For the remaining problem of flexible msg level, can you simply assign a new value to the variable? For example, in process client, you can have a line like cmsg_level = cproc_level + 1. I don't know what is the valid number of cmsg_level.
For example, multiple processes share a channel called com_chan.
chan com_chan = [1] of {byte, ... } /* The first element symbolizes the level */
proctype process(byte proc_level) /* proc_level indicates the level of the process */
{
byte msg_level; /* A local variable to receive the level of the msg */
if
:: com_chan ! proc_level, ... /* Send */
:: com_chan ? msg_level , ... ; /* Receive */
if
:: msg_level > proc_level -> /* If the level of msg is higher than the level of process */
assert(false) /* Flag an error */
:: else /*Normal operation*/
fi
fi
}
Mirza, what is the level of msgs? Do you mean the priority of the msgs? High priority msgs are sent and received before low priority ones? If my guess is right, you may consider "sorted send" (!!) and/or "random receive" (??) statements of channels.
Thank you for the answer and the cited paper. I'll check this out.
BR
Imagine a problem where the state is a set, where the order of the elements is irrelevant. In Promela, however, we have to use a data array to represent the set. Then different orders of the same group of data in the array are considered as different states by SPIN's searching algorithm. For example, {1, 2, 3} and {3, 2, 1} are two different evaluations of the data array but identical as set. The repetition will increase the space complexity of the verification process.
How can we avoid this type of redundancy in SPIN? My feeling is that we must modify the program to detect if a state has been visited. Can we customize the state comparison program in SPIN so that the user can define any type of equivalence relation on the data?