Interpreter: Invariants seem to be checked in a strange way

[pglvdm]

With a model such as:

channels

  left, left1, left2, mid, right : nat

values 

  a : nat = 2

  b : nat = 5

process DataFlow = begin

state

  inseq : seq of nat := []

  outseq : seq of nat := []

inv len inseq >= len outseq and
    outseq = [a*inseq(i) + b * inseq(i) | i in set inds outseq]

actions

  X21 = left1?x -> mid!(a * x) -> X21

  X22 = left2?y -> mid?z -> (dcl r : nat := z + b*y @ right!r -> outseq := outseq ^[r]); X22

  X23 = left?x -> (inseq := inseq ^[x]; left1!x -> X24)

  X24 = left?x -> (inseq:= inseq ^[x]; left2!x -> left1!x -> X24)

@ 

  X23 [| {| left1,left2 |} |]
    ( X21 [| {| mid |} |] X22 )

end

After having selected the events:

[left.1, left1.1, left.2, left2.2, mid.2, right.12]

one gets an invariant checker error such as:

Terminated
Process invariant for 'Process DataFlow []
begin
class $actionClass0
private  inseq:seq of (nat) := []
private  outseq:seq of (nat) := []
private  inv(((len inseq) >= (len outseq)) and (outseq = [((a * inseq(i)) + (b * inseq(i))) | i in set (inds outseq)]))
public  actions X21 []
    left1?x -> mid!(a * x) -> X21
public  actions X22 []
    left2?y -> mid?z -> (
r:nat := (z + (b * y))

right!r -> outseq := (outseq ^ [r])
) ; X22
public  actions X23 []
    left?x -> (

inseq := (inseq ^ [x]) ; left1!x -> X24
)
public  actions X24 []
    left?x -> (

inseq := (inseq ^ [x]) ; left2!x -> left1!x -> X24
)
end $actionClass0
 @ X23 [| null | {| left1, left2 |} | null |] (

X21 [| null | {| mid |} | null |] X22
)
end' is violated at in 'C:\subversion\compasssvn\Common\PublicLiveCMLCaseStudies\DataFlow\DataFlow.cml' at line 19:4

and this cannot be true. Thus, it seems to check the invariant in a wrong context.

[lausdahl]

Can we simplify this example to only include the minimum number of expressions and the smallest inv that gives this problem.

[lausdahl]

@joey-coleman do you think you could help simplify this model

[pglvdm]

This is the one we need to discuss with Jim

[pglvdm]

Well it looks like this one was wrong so I close it now.