Checking implementation

[Pedro Paiva <pedr...@xxxxxxxxx>]

Hi,

Currently, TLA+ does not support checking temporal formulas with existential quantifier (\EE) of temporal logic. For example, suppose I have two modules M1 and M2 and I would like to verify that M2 implements M1, but with some variables of M1, hidden. Let's say

M1 has variables x,y,z

M2 has variables x,y,z,w

y and z should be treated as internal. So

M1(y,z) == INSTANCE M1

M2!Spec => \EE y, z : M1(y,z)!Spec

Can I check it somehow? Thanks.

Best regards,

Pedro

--

Pedro Yuri Arbs Paiva

Engenheiro Eletrônico

Instituto Tecnológico de Aeronáutica (T-16)

(+55) 12 98106-4129