[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Fwd: Regarding TLA+ coding

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 Sultana Chowdhury

Dept. of Computer Science and Engineering, 

University of Asia Pacific,

Dhaka, Bangladesh. 

Attachment: mutexEX.tla
Description: Binary data