[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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>*