[SAL] Help regarding compilation error in SAL

[Bruno Dutertre]

suman kasam wrote:
> Hi,
>    
>         I am facing a problem with a SAL code. Can you help me with that.
>    
>     The problem is in the SAL code attached , position[5] is initially 9 , then changes to 4 ,2 ,4,3 and 10.But when I give the specification :
>    
>      G(FORALL(i:POS): position[5] = i AND X(position[5] /= x) => X(F(position[5] /=x)));
>    
>      Then it doesn't produce any counter example.I don't understand the reason behind it. Can you help me in that. 
>    
>       Iam attaching to this mail the SAL  code(trial.sal), Sequence of position[5] (test.txt).
>    
>    
>   NOTE : running the specification required gives the entire path , and the specification i am speaking about is labelled as constraint in the code.
>    
>    
>   Please help me inthis regard.
>    
>   Thank you ,
>    
>   REgards,
>   Suman Kasam
> 
> 

Hi,

The property you're using

G(FORALL(x:POS): position[5] = x AND X(position[5] /= x) => X(F(position[5] /=x)));

has no counterexamples, because X(P) => X(F(P)) is true in LTL for any state predicate
P. So the trace where position[5] = 9, then 4, 2, 4, 3, 10 does satisfy the property.

Bruno