#183 strange witness

[j-r]

If you have somethings like that :

MACHINE
bug_with
VARIABLES
x
INVARIANTS
inv1 : x ∈ ℕ
EVENTS

INITIALISATION ≙
WHICH IS
ordinary
BEGIN
act1 : x :∈ ℕ
END

evt1 ≙
WHICH IS
ordinary
BEGIN
act1 : x :∈ ℕ
END
END

and a reffinement

MACHINE
bug_withr
REFINES
bug_with
VARIABLES
X
INVARIANTS
inv1 : X ⊆ ℕ
EVENTS

INITIALISATION ≙
WHICH IS
ordinary
BEGIN
act1 : X ≔ ∅
END

evt1 ≙
WHICH IS
ordinary
REFINES
evt1
ANY
n
WHERE
grd1 : n ∈ ℕ
WITH
x : x={n}
THEN
act1 : X ≔ {n}
END
END

Then the system ask for a witness for evt1 for the variable x cause of the assignment x :: NAT. But x is not a local variable (from the ANY) of the event evt1. Therefor it's not possible to define a witness for x.

WORKAROUND : it's possible to add a variable (say n) in the ANY clause of the abstract version of the event and to replace the x :: NAT by x := {n}. Then it's possible to add a witness for n.

But this workaround is not possible in the initialisation, cause ANY are forbidden here

BTW did you see my msg about this subject ? http://sourceforge.net/forum/forum.php?thread_id=1921596&forum_id=377229

Thanks for your attention :)

[Stefan Hallerstede]

Logged In: YES
user_id=1371449
Originator: NO

Hello,

It seems there is no gluing invariant. This will cause a problem when refining. Also, you must provide a witness for a machine variable that disappears in a refinement.

If you post your example project here as an archive, then I can have a look at it. Thanks.

[j-r]

[j-r]

Logged In: YES
user_id=1704513
Originator: YES

Hi Stefan,

thanks for your response. I attach a (another) project to show my point.
It's very simple as a refine a variable x by another one y with x=y as gluing invariant. And I refine the
INIT = x :: NAT
by
INIT = y :: NAT

And in this case I don't see how to prove the refinement.

Thanks,
Joris
File Added: witness.zip

[Laurent Voisin]

Logged In: YES
user_id=1041912
Originator: NO

Hi Joris,

I've had a look at your archive. You're missing a witness for "x'" in your initialisation (the static checker generates a warning for that). Please note that the variable is primed, as the witness is for its after value.

If you add the witness:

x' : x' = y'

then the refinement gets fully proved automatically.

Therefore I don't consider there is a bug here. Please reopen if you disagree.

Laurent.

[Nobody/Anonymous]

Logged In: NO

J'aurais du y penser !
I was not aware that primed variables can be used here. However i have read most of the docs. Maybe a small note, on this subject, in the manual will be useful.

Thank for your response.