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

Use of primed variables in a temporal formula



Dear All, 

I'm a little bit confused on how to properly use primed variables in a temporal formula. I want to verify a simple statement A ~> A' so if A becomes true, A' must be true in the next state.
Can someone explain me which is the correct way to build such formula? 

Cheers,

Giulio