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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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?

Markus

-- 
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.