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

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

On 09.04.20 09:56, Paulo Feodrippe wrote:
> 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?

Hi Paulo,

what does your Java override look like?


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/3c59c585-1025-b2eb-aa6d-9524410f1f3f%40lemmster.de.