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.
Best Regards,
Nahida
Nahida Sultana Chowdhury Dept. of Computer Science and Engineering,
University of Asia Pacific,
Dhaka, Bangladesh.