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

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

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.