A forum for Spin users
You are not logged in.
If the manual pages and your help were so good, I wouldn't have been at the point to ask questions.
yes, of course, the manual helps and it helps to know there is the answer;
so for me it's to name the claim
never npc { /* <>[] np_ */
do
:: true
:: np_ -> break
od;
accept: do
:: np_
od
}
spin -run -ltl npc file.pml
./pan -r -v -N npc
(otherwise the spin output 'the model contains ...' doesn't contain a name for the np_ claim)
:-) not when my mind is on the trace of -N
yes, of course, this works, Thank you!!
but lost again, cannot find the name for np_
how can I address non-progress cycles,
'spin -t -k file.pml.trail -r -s file.pml' would work, but I like more the trail with './pan -r -v'
./pan -r -v -N ??non-progress cycles??
perfect, this works!!
sorry for not reading :-(
./pan -r -v -N ltl_or_never_claim_name [or e.g. never_0]
but how can I address the counterexample for invalid end states
after
'spin -run -noclaim file.pml'
?
when I've got 2 never claims inside a model, I can address the 2nd never claim with ''spin -run -ltl never_1 -a model.pml''
But if there should be a counterexample, I'm getting in trouble.
Therefore my question, should this work with 2 never claims inside?
(with ltl-formulae it works)
Thank you very much!!!
I've specified the inline ltl-property prop with <>a
the promela model incl. inline ltl-property is:
//////////////////////////////////////////////////////////
/* file.pml */
bit x,a,y
active proctype seq1(){
x = 1
}
active proctype seq2(){
a = 0
y = 1
}
ltl prop {<>a}
//////////////////////////////////////////////////////////
the output for 'spin -run -a file.pml' is
//////////////////////////////////////////////////////////
ltl prop: <> (a)
pan:1: acceptance cycle (at depth 10)
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 + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 11, errors: 1
6 states, stored
0 states, matched
6 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 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
//////////////////////////////////////////////////////////
the counterexample with ./pan -r -v :
//////////////////////////////////////////////////////////
depth 1: Claim, state 3 (line 4)
1: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
2: proc 2 (seq2) file.pml:9 (state 1) trans {2,5} [a = 0]
global vars:
bit a: 0
3: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
4: proc 2 (seq2) file.pml:10 (state 2) trans {3,6} [y = 1]
global vars:
bit a: 0
5: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
6: proc 2 (seq2) -:0 (state 0) trans {4,7} [-end-]
global vars:
bit a: 0
7: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
8: proc 1 (seq1) file.pml:4 (state 1) trans {0,8} [x = 1]
global vars:
bit a: 0
9: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
10: proc 1 (seq1) -:0 (state 0) trans {1,9} [-end-]
global vars:
bit a: 0
<<<<<START OF CYCLE>>>>>
11: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
12: proc 0 (ltl_0) file.pml:4 (state 3) trans {5,3} [(!(a))]
global vars:
bit a: 0
spin: trail ends after 12 steps
#processes 1:
12: proc 0 (ltl_0) file.pml:4 (state 3) (invalid end state)
(!(a))
global vars:
bit a: 0
//////////////////////////////////////////////////////////
"START OF CYCLE" inside the counterexample is confusing me, because the negation of the inline ltl-property <>a is safety.
But why is then "START OF CYCLE" there? (<=> SPIN output 'pan:1: acceptance cycle (at depth 10)')
the never claim for the negation of the inline ltl-property is
never { /* []!a */
accept_init:
T0_init:
do
:: (! ((a))) -> goto T0_init
od;
}
Is there really a pattern to tell safety in a never claim?
yes, that was my thinking,
but why is the counterexample with "START OF CYCLE" ?
it is stating there was an intersection of automaton M and 'negation' with liveness,
but the 'negation' of <>a is safety
where is my mistake?
oah, perhaps (at least :- ) one step back,
property shall be <>a (Liveness)
'negation' !(<>a) <=> []!a (Safety)
SPIN looks for an intersection of automata M and 'negation',
if intersection is empty, then M |=property,
(2) if intersection is not empty, SPIN found a counterexample (there is a state found, where M does not hold the property)
to my surprise, for the property <>a the counterexample is with 'START OF CYCLE' (so there was another negation?)
so I'm completely wrong when I thought the counterexample is the result
from step (2)?
I'm still confused,
#define p ([](x -> (a U y)))
p is not(safe) and not(live) but it can be REpresented by an intersection of a live and a safe property?
https://cstheory.stackexchange.com/questions/29400/ltl-property-safety-or-liveness
regarding p U false
in The SPIN model checker: Primer and reference manual is written:
"Note that the truth of this formula only depends on the value of sub-formula p."
I thought the difference between strong until and weak until is
p U q, q must become true
p W q, q can become true
so, was really p U false intended and not p W false in the meaning of always/[]p?
thank you very much!!!
but the -a flag shouldn't hurt, should it?
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 secondscase 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 secondsI 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
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"
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?
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?
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)
}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)
thank you very much!!
#define p (<>x) (Liveness)
M |= p
!p <=> Never claim
so !p is still a liveness property, because !p would be a cycle in absence of x, or in other words, must be a cycle to show there is no x
"The negation of a liveness property is a safety property." == false
I think I got it now :-)
//////////////////////
ltl, yes, of course, assignments in ltl are not possible,
but I wanted to ask, additionally, how do you express a sequence of x,y,z in ltl?
(!y U x) && (!z U y) && (true U z)
you wrote there is a nested solution, but how does it look in detail?
yes, that was the missing link, thank you!!
not sure about liveness and safety, actually, stupid question: is not liveness in ltl-formulae getting safety in a never claim?
another question, c,d,e, just the sequence, independent of a,b,f,g: how would the perfect ltl-formulae be with nested UNTIL? (without a,b,f,g)
bit val_a, val_b,val_f,val_g
never {
do
::!c
::e||d -> goto no_accept
::atomic { c -> val_a = a; val_b = b; val_f = f; val_g = g; break }
od
#define INV (val_a!=a)||(val_b!=b)||(val_f!=f)||(val_g!=g)
do
::e||INV -> goto no_accept
::d-> break
od
do
::INV -> goto no_accept
::e-> break
od
do
::skip
od
/* is it a safety property? if yes, acceptance cycle is not needed?*/
no_accept: skip
}
not sure, but I think this could be a solution, in any case, it's good I cannot specify the future :-)
(I had problems with precedence from c to e. Moreover, how can the first part of l1 formulae be shortened?)
#define seq (c && d && e)
#define seqneg (!c && !d && !e)
/* M |= l1 */
ltl l1 {
(
((!a U seq)||(seqneg U a))
&& ((!b U seq)||(seqneg U b))
&& ((!f U seq)||(seqneg U f))
&& ((!g U seq)||(seqneg U g))
/* c before d && d before e*/
&& ((!d U c) && (!e U d) && (true U e))
)
}
before the process starts INV is not known, the combination of a,b,f,g before c = 1 is not deterministic or at least unknown
Thank you very much!!
But what, if sum of a,b,f,g is 2 or 3 before c = 1?