[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Regarding TLA+ coding
- From: Nahida Sultana Nahida Sultana <nchow...@xxxxxxxxxx>
- Date: Fri, 24 Feb 2017 09:56:40 -0500
I am just a beginner of using TLA+ having difficulties.
I have a query is:
In my code I have a line like
Spec == /\ Init /\ [PNext]_stateP /\ eventually
where [PNext]_stateP represent PNext will be also true if stateP'=stateP but I don't want to add this conditiontion here, so when I am trying to change the code by replacing PNext it's saying "followed by action not of form [A]_v".
In this situation what I am supposed to do, also correct me if I am assuming something wrong.
*The source code is attached here.
Nahida Sultana Chowdhury
Dept. of Computer Science and Engineering,
University of Asia Pacific,
Description: Binary data