[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Checking implementation


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 Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129