ltl formula

From: Fabio (fabio.marcone_at_libero.it)
Date: Tue Jun 22 2004 - 15:45:44 MDT

Hi!
I've some problems to describe a condition to verify in vis
(bounded_model_checking).
I've 2 models:
A with output a0...an
B with output b0...bn

I need to verify that a0=b0 and ...and an=bn and I wrote in the ltl file:
G((A.a0=B.b0)*...*(A.an=B.bn));

but vis error message indicates that A.a0 isn't a known node. why?
So I wrote
G((a0=b0)*...*(an=bn));

but in this way there is an error in the RHS.

Can we help me?

Thanks,
Fabio Marcone

This archive was generated by hypermail 2.1.7 : Tue Jun 22 2004 - 15:47:13 MDT