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,