[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Use of primed variables in a temporal formula
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?