Spinroot

A forum for Spin users

You are not logged in.

#1 2019-04-17 19:28:37

marc15
Member
Registered: 2019-02-07
Posts: 34

option -q == require empty chans in valid end states

I translated the following bpmn-process to promela:
https://www.bilder-upload.eu/bild-9baca3-1555515962.png.html

Because of the loop inside the and_gates there should be a deadlock because as soon as the loop path is went there is at least one token/message too few at the closing and_gate at some point.
With spin -run -a file.pml and without a ltl-formulae I get the expected error.
But with ltl {[]<>end} I get no errors. Even with option -q ('require empty chans in valid end states) there is no error although the process is not in a valid end state. What do I do wrong?

active proctype closing_and_gate(){
	bit received0,received1    
	end_label:
	if
	::(bus[3]?[1]) ; atomic{receive(3); received0=1}
	::(bus[4]?[1]) ; atomic{receive(4); received1=1}
	fi
	/* with ltl {[]<>(end && last_is_endevent)} I get the error as expected (but not with {[]<>(end))}
	atomic{
		last_is_endevent = 0
	}
	*/
	do
	::(!received0 && bus[3]?[1]); atomic{receive(3); received0=1}
	::(!received1 && bus[4]?[1]); atomic{receive(4); received1=1}
	::(received0 && received1) ; atomic{received0=0; received1=0; break}
	od
    ...
    ...
    goto end_label
}

btw, what is the recommended way/coding to receive messages in unknown order? (for many channels)

Offline

#2 2019-04-17 23:24:39

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

how is "end" defined?

Offline

#3 2019-04-18 08:40:15

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

end-EndEvent is now EndEvent_1qh2a0m
bpmn-process with channel captions:
https://www.bilder-upload.eu/bild-0cb540-1555570626.png.html


chan bus[5] = [2] of {bit} 

bit last_is_endevent

inline send(ch){
    bus[ch]!1
}
inline receive(ch){
    bus[ch]?1
}

inline execute(ele){
    atomic{
        last_is_endevent = 0
        if
            ::ele < 2 ; ele++
            ::else
        fi
    }
}


/*------------------------------------------------------------------------------*/
byte StartEvent_09szjq4

/*closing ExclusiveGateway*/
byte ExclusiveGateway_1rx54c1

/*opening ExclusiveGateway*/
byte ExclusiveGateway_07tkdkl

byte EndEvent_1qh2a0m

/* opening and_gate */
byte ExclusiveGateway_1vbaox5

/* closing and_gate */
byte ExclusiveGateway_1lsle44
/*------------------------------------------------------------------------------*/

active proctype seq4(){
	bit received0,received1
	end_label:
	/*incoming channels of the closing and_gate*/
	if
	::(bus[3]?[1]) ; atomic{receive(3); received0=1}
	::(bus[4]?[1]) ; atomic{receive(4); received1=1}
	fi
	do
	::(!received0 && bus[3]?[1]); atomic{receive(3); received0=1}
	::(!received1 && bus[4]?[1]); atomic{receive(4); received1=1}
	::(received0 && received1) ; atomic{received0=0; received1=0; break}
	od
	
	/* closing and_gate */
	execute(ExclusiveGateway_1lsle44)
	
	atomic{
		execute(EndEvent_1qh2a0m)
		last_is_endevent = 1
	}
	goto end_label
}

active proctype seq3(){
	byte out0,out1
	end_label:
	receive(2)
	
	/*opening ExclusiveGateway*/
	execute(ExclusiveGateway_07tkdkl)
	
	/*forcing strong fairness / (out0<n) with n depending on the branches of all exclusive and inclusive gates (not parallel) */
	if_ExclusiveGateway_07tkdkl:
	if
	::(out0<1) ; atomic{send(1);out0++}
	::(out1<1) ; atomic{send(4);out1++}
	::else ; atomic{out0=0;out1=0;goto if_ExclusiveGateway_07tkdkl}
	fi
	goto end_label
}

active proctype seq2(){
	end_label:
	if
	::receive(0)
	::receive(1)
	fi
	
	/*closing ExclusiveGateway*/
	execute(ExclusiveGateway_1rx54c1)
	/* opening and_gate */
	execute(ExclusiveGateway_1vbaox5)
	
	atomic{
		send(2)
		send(3)
	}
	goto end_label
}

active proctype seq1(){
	execute(StartEvent_09szjq4)
	send(0)
}

Offline

#4 2019-04-18 15:56:54

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

In the two verification runs you're checking for different properties.
Without the ltl property, you're looking for assertion violations and invalid end-states,
but with the ltl property you're only verifying that all executions eventually lead to the value of EndEvent_1qh2a0m being nonzero.
Note that in the counter-example you find in the first run (without the ltl property) the final value of EndEvent_... is also 1, so not a violation of the ltl property....

Offline

#5 2019-04-18 19:07:52

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

ah, and -q just means when you are "in a valid end state then ..." and not "you have to be", got it. Thank you!!
Nevertheless, in the interest of safety:
if processes are in valid end states will never be checked in conjunction with never claims/ltl formulae?

Offline

#6 2019-04-18 19:21:53

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

deadlocks (invalid end-states) are not checked when your check an ltl formulae, that's correct: it's a different kind of check.
so you'd have to comment out the ltl formulae to get the basic deadlock/assertion check enabled

Offline

#7 2019-05-26 07:07:21

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

Instead of commenting out ltl-claims I tried the noclaim option. But with

spin -run -noclaim  -a  file.pml

one of the ltl claims will be checked and not the basic deadlock/assertion check.

Is my understanding of the noclaim option wrong?

Offline

#8 2019-05-26 17:15:26

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

Can you show the output of that run? Especially the first couple of lines where it should say:
      never claim - (not selected)

Offline

#9 2019-05-26 17:33:43

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

spin -run -noclaim  -a promela_.pml
ltl test: <> (EndEvent_1qh2a0m)

(Spin Version 6.4.8 -- 2 March 2018)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (not selected)
	assertion violations	+
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	+

State-vector 92 byte, depth reached 40, errors: 0

PS: If there is no LTL-claim in promela_.pml,
then I get an "errors:1"
with "spin -run -noclaim  -a promela_.pml"

Offline

#10 2019-05-26 18:17:24

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

It tells you that there is a claim, but it did not enable it in the run, because "never claim - (not selected)" is shown.
If there is no claim, then -noclaim would have no effect, but you also should not get any errors that you don't get without -noclaim.
Do you have an example of where that's not the case?

Offline

#11 2019-05-26 18:33:48

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

I took the promela-model from this page,
id: http://spinroot.com/fluxbb/viewtopic.php?pid=3552#p3552
(2019-04-18 08:40:15)

and added inside from the file with the promela model #3552
"ltl test {<>EndEvent_1qh2a0m}"

expected results:
model #3552 holds ltlc-claim test,
but not the basic deadlock/assertion check

but as said, there are differents outputs with the noclaim-command depending on ltl-claim test inside and or not

Offline

#12 2019-05-26 18:45:46

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

Just so I understand the issue better:  if you do two separate verification runs:
1. with the ltl claim inside the promela model commented out, verifying without -noclaim
2. with the ltl claim *not* commented out and verifying with -ncolaim
you get different results?
Can you show the two results and how they differ?

Offline

#13 2019-05-26 19:14:33

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

case 1. with the ltl claim inside the promela model commented out, verifying without -noclaim

spin -run  -a promela_.pml
warning: no accept labels are defined, so option -a has no effect (ignored)
pan:1: invalid end state (at depth 39)
pan: wrote promela_translation.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	- (not selected)
	invalid end states	+

State-vector 92 byte, depth reached 40, errors: 1
       30 states, stored
        0 states, matched
       30 transitions (= stored+matched)
       11 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.003	equivalent memory usage for states (stored*(State-vector + overhead))
    0.276	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage



pan: elapsed time 0 seconds

Offline

#14 2019-05-26 19:16:12

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

2. with the ltl claim *not* commented out and verifying with -noclaim

spin -run -noclaim  -a promela_.pml
ltl test: <> (EndEvent_1qh2a0m)

(Spin Version 6.4.8 -- 2 March 2018)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (not selected)
	assertion violations	+
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	+

State-vector 92 byte, depth reached 40, errors: 0
       72 states, stored
       26 states, matched
       98 transitions (= stored+matched)
       23 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.008	equivalent memory usage for states (stored*(State-vector + overhead))
    0.276	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage


unreached in proctype seq4
	promela_translation.pml:63, state 50, "-end-"
	(1 of 50 states)
unreached in proctype seq3
	promela_translation.pml:81, state 29, "-end-"
	(1 of 29 states)
unreached in proctype seq2
	promela_translation.pml:100, state 29, "-end-"
	(1 of 29 states)
unreached in proctype seq1
	(0 of 11 states)
unreached in claim test
	_spin_nvr.tmp:4, state 3, "(!(EndEvent_1qh2a0m))"
	_spin_nvr.tmp:6, state 6, "-end-"
	(2 of 6 states)

pan: elapsed time 0 seconds

Offline

#15 2019-05-26 19:17:03

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

interesting! -- I'll try to find out what's happening there.

Offline

#16 2019-05-26 19:20:28

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

ah: to find the deadlock error: omit the -a flag

Offline

#17 2019-05-26 19:25:22

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

but the -a flag shouldn't hurt, should it?

Offline

#18 2019-05-26 19:26:52

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: option -q == require empty chans in valid end states

it shouldn't, but it looks like it did make a difference.
i'll try to find out later why that is, but for now that solves the problem.
technically, -a is just for liveness (cycles), although it should report other
errors as well when the verification runs into them

Offline

#19 2019-05-26 19:39:40

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: option -q == require empty chans in valid end states

thank you very much!!!

Offline

Board footer

Powered by FluxBB