#183 strange witness
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 :)
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.
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
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.
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.