Posts by DavidFarago

DavidFarago · General

Oh, one more thing: complex_model makes simple_model only more complex by initializing certain variables differently. Those variables, however, influence the control flow. Can that already cause variables being reordered?

Thanks a lot for your help!
David

DavidFarago · General

Thanks for the explanation.

I did come from bitstate, where no error was found and the verification had 3e+08 states stored (5e+08 states matched). For MA, the verification did not find any error either, but caused an out-of-memory after 6e+08 states stored (only 5e+07 states matched).

Do you have any experience/statistics how good bitstate really is? I wonder if I only need to reach another 1.5e+08 states in MA (to reach all states matched in bitstate), or if there are likely completely new subgraphs not reached via bitstate.

Best
David

DavidFarago · General

Thank you for this concise explanation.

Too bad that local variables cannot be hidden. Do they not contribute just like global variables to the state vector?

Since I prefer smallest possible scopes, my variables that are solely used inside one d_step are always local and hence not hideable. Could this be changed in Spin? That would be awesome, because I have many of those variables.

Otherwise, what are the disadvantages if I make such a variable global just for the purpose of hiding it? Since it is hidden, turning it global will not deteriorate POR, will it?

Thanks,
David

DavidFarago · General

Hello,

I have a simple_model that required about 3e+08 states and 7GB memory using collapse compression and minimized automaton (MA) with about 1e+06 nodes.

complex_model makes simple_model a bit more complex: I expected the number of states and memory requirements to increase by a factor of 2 to 3, which would not cause an out-of-memory on my machine.

But instead, I do get out-of-memory (>30GB) after traversing about 6e+08 states. I guess the much higher memory requirements come from now having 11e+06 MA nodes when out-of-memorying (instead of the expected 2e+06 MA nodes).

Are there specific reasons for suddenly getting a 5 times higher number of MA nodes in relation to the number of states? If not, is there a way to find the cause? How can I avoid the cause?

Thanks
David

DavidFarago · General

Hello,

I have the following structure:

inline foo(parameter) {
d_step {
struct_type struct_local_var;
<code block that is the only one using struct_local_var>
}
}

To safe some memory, I wanted to switch to

hidden struct_type struct_local_var;

However, I get the error message

spin: ./foo.pml:29, Error: cannot hide non-globals (_12_5_6_8_struct_local_var)

What is a "non_global", and why is struct_local_var one? How can I enable hiding struct_local_var?

Best
David

DavidFarago · General

Hi Brishna,

maybe the following sites will also help you:

https://web.archive.org/web/20171118181253/http://www.albertolluch.com/research/promelamodels
http://paradise.fi.muni.cz/beem/

Best
David

DavidFarago · General

Thanks for the clarification.

Too bad -DHC0 does not have the effect as described in the spin book, since I have a huge state space and only 14GB of memory available. Thus using 32bit values would be a good approach in spite of the higher collision risk.

So is there a possibility to do this?

DavidFarago · General

Hi,

I would like to configure Spin so that it uses hash-compact with 14GB without running out of memory.

Unfortunately, playing with the -DHC makes no difference, case 1 with -DHC0 and case 2 with -DHC4 yield the same out of memory (see below).

So: Is this a bug or do I have to additionaly modify some other options? Which ones?

Thanks,
David

Case 1)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC0 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth= 753 States= 1e+06 Transitions= 1.01e+06 Memory= 166.672 t= 0.94 R= 1e+06
....
Depth= 813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660 t= 661 R= 5e+05
pan: reached -DMEMLIM bound
1.47324e+10 bytes used
102400 bytes more needed
1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts: 77109092 (resolved)

Stats on memory usage (in Megabytes):
78944.851 equivalent memory usage for states (stored*(State-vector + overhead))
12002.095 actual memory usage for states (compression: 15.20%)
state-vector as stored = 14 byte + 28 byte overhead
2048.000 memory used for hash table (-w28)
0.054 memory used for DFS stack (-m1000)
14049.914 total actual memory usage

Case 2)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC4 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth= 753 States= 1e+06 Transitions= 1.01e+06 Memory= 166.672 t= 1.12 R= 9e+05
...
Depth= 813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660 t= 596 R= 5e+05
pan: reached -DMEMLIM bound
1.47324e+10 bytes used
102400 bytes more needed
1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts: 77109092 (resolved)

Stats on memory usage (in Megabytes):
78944.851 equivalent memory usage for states (stored*(State-vector + overhead))
12002.095 actual memory usage for states (compression: 15.20%)
state-vector as stored = 14 byte + 28 byte overhead
2048.000 memory used for hash table (-w28)
0.054 memory used for DFS stack (-m1000)
14049.914 total actual memory usage

DavidFarago · Bug Reports

Hello,

after running out of memory with the 32bit version, trying to install the 64bit version on Windows 7 Professional 64bit yields the error message:

The version of this file is not compatible with the version of Windows you're running. Check your computer's system information to see whether you need an x86 (32-bit) or x64 (64-bit) version of the program, and then contact the software publisher.

How should we proceed?

Best
David

DavidFarago · General

Thanks, that seems to be even better than the example on page 373 of the spin book.

However, now two processes are "reading" from channel c, so xr c in the original process that really reads c is causing problems:

spin: ./powerOffFailureModel.pml:15, Error: invalid use of 'else' combined with i/o and xr/xs assertions, statement separator near 'skip'

Is there no way to keep xr c for the special case that only one process is reading c and some other processes are completely flushing c?

DavidFarago · General

I want to flush channel c, i.e. remove all contents from c without reading it. What is the most effective (yielding smallest state space) way to do that?

Details:
I have a process that models powerOffs, which also reset channel c. Should the process (atomically) read from c until it is empty (as on page 373 of the spin book)? That way, xr c in another process is broken. Should I reinitialize channel c? Or is there some channel flush command I have not yet come across?

DavidFarago · General

Thank you very much

DavidFarago · General

Great that you are open for this suggestion.

Can I somehow help or motivate to achieve this?

Bosch and I would be very glad to have it.

DavidFarago · General

Sorry, I meant multiple mtype types, not multiple mtype definitions.

For example, if you had mtype_1 statesOfProc1, mtype_2 statesOfProc2, ...., you could have up to 255 states for each mtype_i, and get a compiler error when assigning an mtype_1 element to statesOfProc2.

Is there some way to achieve this?

DavidFarago · General

Thanks, that is some good advice. We are, however, modeling close to the software, so the models need to contain the relevant details and are thus not really small.

Since the code contains a lot of enums, I would like to come back to my point 5) above: How should I translate all the enums into Promela? Is there a workaround so that I can simulate having multiple mtypes in Promela?

Currently, I am using #defines and unsigned variables to model enumerations, to avoid having one huge mtype, which causes large state vectors and weak type safety. However, #defines is even weaker typed and harder to debug (seeing numbers instead of identifiers in simulation).

DavidFarago · Bug Reports

Is the following a bug? If so, is there a workaround, so I can still use the concise select statement for 2-dimensional arrays?

2-dimensional array:

    
typedef solt
{
	byte 	Id;
	bool  Valid;
};

typedef ds 
{
	solt y[dimy];
};

ds x[dimx];

Now I want to use a simple select for one Id:

    
            select (x[0].y[0].Id : 0..2);

However, the syntax check of Spin Version 6.4.6 -- 2 December 2016 says:
[quote]Error: bad index in for-construct sector[/quote]

This error does not occur if I do the translation by hand as described at http://spinroot.com/spin/Man/select.html:

	  x[0].y[0].BlkId = 0;
	  do
	  :: (x[0].y[0].Id < 3) -> x[0].y[0].Id++
	  :: break
	  od

Now the syntax check of Spin Version 6.4.6 -- 2 December 2016 says:
[quote]No Syntax Error.[/quote]

DavidFarago · General

Hi,

are there best practices to structure your promela code when you have a lot of it?

--------------------------------

Have we made good architectural choices with the following approach?

1) We model each software part/feature (there are about 20) in a separate promela file (of 10 to 200 LOC), using either proctype or inline. This helps us to modularize, but gives warnings regarding missing init (or other active) proctype, and requires us to #include files.

2) Because we #include different promela files, we use include guards.

3) We have one main promela files which (directly or indirectly) includes all other promela files. It has many initialization proctypes for various aspects; at all times, only one of these proctypes is marked active.

4) Some "software xxx line" variants we model via #defines, others are more suitable to directly integrate into the model (i.e. via variables and promela structures instead of precompiler directives).

5) We use defines and unsigned variables to model the various enumerations we have, to avoid having one huge (untyped) mtype, at the cost of more cryptic debugging.

DavidFarago · General

Thanks for your answer, and for the very helpful never claim.

DavidFarago · General

Using Spin Version 6.4.6 -- 2 December 2016 on a Mac, I get the following errors in pan.c when checking for non-progress cycles:
* error: expected expression
* error: use of undeclared identifier 'Pclaim'

Unfortunately, I may not post the promela file, and a simplified version does not lead to these errors but to a successful non-progress cycle check.

What causes these errors? With a hint, I might be able to avoid these errors or write a simplified version that still exposes these errors.

------------------------------------

Here is the output from the problematic promela file:

Checking syntax and generating the pan.c verifier ...
/opt/local/bin/spin -a sSDPV1.pml
...
the model contains 12 never claims: ...
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N REQ0)
or use e.g.: spin -search -ltl REQ0 sSDPV1.pml
No Syntax Error.

Starting verification...
gcc -DMEMLIM=1024 -DNP -DNOFAIR -DNOCLAIM -DXUSAFE -O2 -w -o pan pan.c
pan.c:7485:26: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:18: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:51: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:43: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:8796:39: error: expected expression
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
pan.c:8796:31: error: use of undeclared identifier 'Pclaim'
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
6 errors generated.
Verification: Compile-Time Error - Process ExitValue: 1

DavidFarago · General

Thanks for your reply. Here is a <strike>minimal</strike>small example:

#define k 3
#define succ(index) ((index+1) % k)
#define pre(index) ((index+(k-1)) % k)

mtype = { C, B, F, E };
mtype arr[k];
bool u;

ltl REQ5 {[]( (arr[1]==B) -> (arr[2] != F) )}

proctype sp (byte index)
{
do
:: atomic{ (arr[index] == C && arr[pre(index)] == F)
-> assert(u == false); arr[index] = B; u = true }
:: atomic{ (arr[index] == B && arr[succ(index)] != F)
-> arr[index] = F; u = false }
:: atomic{ (arr[index] == F && arr[pre(index)]!=F && u)
-> arr[index] = E }
:: atomic{ (arr[index] == E && arr[pre(index)]!=E)
-> arr[index] = C }
od
}

init {
atomic {
byte index = 0;
do
:: index < k ->
   arr[index] = E;
   run sp (index);
   index++
:: index >= k -> break
od;
arr[0] = B; u = true;
}
}

Checking REQ5 leads to the following output:

Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
never claim + (REQ5)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 52 byte, depth reached 39, errors: 1
16 states, stored
2 states, matched
18 transitions (= stored+matched)
9 atomic steps
hash conflicts: 0 (resolved)

DavidFarago · General

Since there seem to be more questions related to Promela and Spin on stackoverflow, I have posted my question there: https://stackoverflow.com/q/44684675/750378.

However, since there are only 5 views, I am posting this link here in the hope that it will be answered.

Best
David

------------

In case the link above no longer works, here is the contents:

For verifications (with ispin) that use never claims, I get outputs with `depth reached` larger than the number of states and the number of transitions, e.g.:

Full statespace search for:
never claim + (REQ5)
assertion violations + (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by never claim)

State-vector 60 byte, depth reached 87, errors: 1
41 states, stored
10 states, matched
51 transitions (= stored+matched)
9 atomic steps
hash conflicts: 0 (resolved)

I find that a bit unintuitive. Is there a precise description of the semantics of "depth reached" somewhere (more thorough than [pan's output format description](http://spinroot.com/spin/Man/Pan.html#C))? Maybe the meaning of

> longest depth-first search path contained 87 transitions

does not refer to the 51 transitions, but to the transitions of the system automata composed with the never claim?

Spinroot

#1 Re: General » Minimized Automaton optimization drops after small change in model » 2018-11-25 21:12:40

#2 Re: General » Minimized Automaton optimization drops after small change in model » 2018-11-25 21:05:54

#3 Re: General » Hiding "local" variable yields error "cannot hide non-globals" » 2018-11-25 20:47:38

#4 General » Minimized Automaton optimization drops after small change in model » 2018-11-22 12:17:49

#5 General » Hiding "local" variable yields error "cannot hide non-globals" » 2018-11-14 17:47:07

#6 Re: General » Looking for Promela Models/Datasets » 2018-11-14 17:38:52

#7 Re: General » Optimally configuring hash-compact method » 2018-10-05 08:12:57

#8 General » Optimally configuring hash-compact method » 2018-09-11 16:20:32

#9 Bug Reports » Spin Precompiled Executable for Windows 64bit yields error » 2018-08-27 15:43:34

#10 Re: General » Most effective way to flush a channel » 2018-05-16 20:15:32

#11 General » Most effective way to flush a channel » 2018-05-09 13:51:27

#12 Re: General » Best practices to structure large promela code » 2017-08-23 12:51:40

#13 Re: General » Best practices to structure large promela code » 2017-08-22 08:40:40

#14 Re: General » Best practices to structure large promela code » 2017-08-21 19:36:40

#15 Re: General » Best practices to structure large promela code » 2017-08-21 16:56:26

#16 Re: Bug Reports » select » 2017-08-10 11:41:17

#17 General » Best practices to structure large promela code » 2017-08-09 14:10:01

#18 Re: General » What kind of states & transitions does Spin's “depth reached” consider » 2017-08-09 13:42:52

#19 General » What causes these pan.c errors when checking for non-progress cycles? » 2017-07-14 12:03:36

#20 Re: General » What kind of states & transitions does Spin's “depth reached” consider » 2017-07-14 10:45:39

#21 General » What kind of states & transitions does Spin's “depth reached” consider » 2017-06-24 09:36:16

Board footer