Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#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
#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
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
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
#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: 0PS: 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
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
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 secondsOffline
#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 secondsOffline
#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
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