Temporal property

[vit...@xxxxxxxxxx]

Hi, is it possible in TLA to specify and check the property linking values of current and next states, like Prop == (x = 1) => (y` = 2). Seems to be the operation "=" for primed variables (as e.g. y') will be considered as assignement, but not comparison? Tq.
-- 
*The information contained in this e-mail message and any accompanying 
files is or may be confidential. If you are not the intended recipient, any 
use, dissemination, reliance, forwarding, printing or copying of this 
e-mail or any attached files is unauthorised. This e-mail is subject to 
copyright. No part of it should be reproduced, adapted or communicated 
without the written consent of the copyright owner. If you have received 
this e-mail in error please advise the sender immediately by return e-mail 
or telephone and delete all copies. UMP does not guarantee the accuracy or 
completeness of any information contained in this e-mail or attached files. 
Internet communications are not secure, therefore UMP does not accept legal 
responsibility for the contents of this message or attached files.*
*Universiti Malaysia Pahang <http://www.ump.edu.my>*