A forum for Spin users
You are not logged in.
Pages: 1
Visitors of spinroot.com now have to go through a CAPTCHA. I suspect this is to protect this forum from spam.
However it also breaks all scripts that automatically download Spin for installation. Typically you get:
% wget https://spinroot.com/spin/Src/src646.tar.gz
--2017-05-24 18:15:14-- https://spinroot.com/spin/Src/src646.tar.gz
Resolving spinroot.com (spinroot.com)... 104.28.10.21, 104.28.11.21, 2400:cb00:2048:1::681c:b15, ...
Connecting to spinroot.com (spinroot.com)|104.28.10.21|:443... connected.
HTTP request sent, awaiting response... 403 Forbidden
2017-05-24 18:15:14 ERROR 403: Forbidden.Would it be possible to not put those tarballs behind such a protection?
Great. We experienced a handful of such discrepancies in a benchmark we are building to explore how different never claims impact Spin.
Can you confirm that we are safe from this bug if we use the current version with -DNOSTUTTER? This is our current workaround.
Hi,
This looks like a bug to me, yet I'm not really confident about it because I'm not sure how Spin handle deadlock states in the model when checking a neverclaim.
Here are two neverclaims that express the same property (it's GF(ap0)&&GF(!ap0)):
% cat never1
never {
T0_init:
if
:: (1) -> goto T0_init
:: ((ap0)) -> goto accept_S1
fi;
accept_S1:
if
:: ((!(ap0))) -> goto T0_init
:: (1) -> goto T0_S2
fi;
T0_S2:
if
:: ((!(ap0))) -> goto T0_init
fi;
}% cat never2
never {
T0_init:
if
:: ((ap0)) -> goto accept_S1
:: (1) -> goto T0_init
fi;
accept_S1:
if
:: ((!(ap0))) -> goto T0_init
:: (1) -> goto T0_S2
fi;
T0_S2:
if
:: ((!(ap0))) -> goto T0_init
fi;
}So just to make everything clear, the difference is just in the order of transitions of T0_init:
% diff -u never1 never2
@@ -1,8 +1,8 @@
never {
T0_init:
if
- :: (1) -> goto T0_init
:: ((ap0)) -> goto accept_S1
+ :: (1) -> goto T0_init
fi;
accept_S1:
ifNow here is what I do not understand:
% spin -N never1 -search -a -DNOREDUCE extinction.2.pm | grep -A4 error
State-vector 168 byte, depth reached 292, errors: 0
946765 states, stored (1.0977e+06 visited)
3342247 states, matched
4439942 transitions (= visited+matched)
1577441 atomic steps
% spin -N never2 -search -a -DNOREDUCE extinction.2.pm | grep -A4 error
State-vector 168 byte, depth reached 255, errors: 1
9418 states, stored (9420 visited)
24162 states, matched
33582 transitions (= visited+matched)
9170 atomic stepsIn the latter case the trail ends with
[...]
170: proc 0 (Node_0:1) extinction.2.pm:50 (state 39) [((j==1))]
172: proc 0 (Node_0:1) extinction.2.pm:54 (state 45) [lrec = (lrec+1)]
172: proc 0 (Node_0:1) extinction.2.pm:54 (state 44) [win = ((m%(10*10))/10)]
174: proc 0 (Node_0:1) extinction.2.pm:30 (state 14) [(((lrec==1)&&(win==0)))]
174: proc 0 (Node_0:1) extinction.2.pm:30 (state 13) [leaders_num = (leaders_num+1)]
<<<<<START OF CYCLE>>>>>
Never claim moves to line 4 [((leaders_num==1))]
spin: trail ends after 176 steps
#processes: 6
leaders_num = 1
176: proc 5 (chnlnel_ch_2:1) extinction.2.pm:304 (state 2)
176: proc 4 (chnlnel_ch_1:1) extinction.2.pm:292 (state 2)
176: proc 3 (chnlnel_ch_0:1) extinction.2.pm:280 (state 2)
176: proc 2 (Node_2:1) extinction.2.pm:205 (state 18)
176: proc 1 (Node_1:1) extinction.2.pm:114 (state 23)
176: proc 0 (Node_0:1) extinction.2.pm:95 (state 106)
176: proc - (never_0:1) never2:8 (state 11)
6 processes createdbut I do not understand how to read the cycle here. I believe proc 0 to 5 are
in deadlock, but the never claim is definitely not. If the system stutters in its
deadlock state (this is what should happen, right?) then the neverclaim should
be able to move to T0_S2 and (silently) die there.
The property GF(ap0)&&GF(!ap0) should not match runs ending in a deadstate if
the deadstate is made stuttering, since ap0 cannot change.
I've put all the files at https://gist.github.com/adl/1904a55e6b4b1f71ef9a/download
if you want to reproduce.
Pages: 1