[tlaplus] Message "Successor state is not completely specified" when overriding a Action in Java

[Paulo Feodrippe <pfeodrippe@xxxxxxxxx>]

I'm trying to override the action below using Java, the action does not modify any of the variables (it's translated from PlusCal)

ADAPT(self) == /\ pc[self] = "ADAPT"

               /\ TRUE

               /\ pc' = [pc EXCEPT ![self] = "TRANSFER_MONEY"]

               /\ UNCHANGED << c1, c2, account, receiver_new_amount, 

                               sender_new_amount, sender, receiver, money >>

But when overriding it, it errors as

Error: Successor state is not completely specified by action ADAPT of the next-state relation. The following variables are not assigned: account, c1, c2, money, pc, receiver, receiver_new_amount, sender, sender_new_amount.

I understand why I receive this error, but is there some way to set the sucessor state in an override?

Thank you o/

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f9278d6f-826e-43f4-8ea8-c39f56ba5f1e%40googlegroups.com.