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

Hi Markus, thanks for your time.

It's a simple java file which I've put in a `jar` which I've added with `-DTLALibrary` when calling TLC

bash

pcal main4.tla && JAVA_OPTS="-XX:+UseParallelGC -DTLA-Library=/Users/feodrippe/dev/my-practical-tlaplus/tests/TLCHash/clojure-from-java/target/cfj-0.1.0-SNAPSHOT-standalone.jar" tlc main4.tla

main4.java

import tlc2.value.impl.IntValue;
import tlc2.value.impl.Value;
import tlc2.value.impl.BoolValue;

public class main4 {

    public static BoolValue ADAPT(Value v) {
        return BoolValue.ValTrue;
    }
}

main4.tla

-------------------------------- MODULE main4 --------------------------------

EXTENDS Integers, Sequences, TLC

(*--algorithm transaction {
    variables c1 = "c1", c2 = "c2", account = [c \in {"c1", "c2"} |-> 10];

  define {
      ConstantBalance == account["c1"] + account["c2"] = 20
  }

  fair process (tx \in {"t1"})
    variable receiver_new_amount = 0,
    sender_new_amount = 0,
    sender = c1,
    receiver = c2,
    money \in 1..2;
    {
        ADAPT:
        skip;
        (* ADD_NEW_AMOUNTS removido *)
        TRANSFER_MONEY:
        account[sender] :=
        account[sender] - money ||
        account[receiver] := account[receiver] + money;
    }
}*)

\* BEGIN TRANSLATION
VARIABLES c1, c2, account, pc

(* define statement *)
ConstantBalance == account["c1"] + account["c2"] = 20

VARIABLES receiver_new_amount, sender_new_amount, sender, receiver, money

vars == << c1, c2, account, pc, receiver_new_amount, sender_new_amount, 
           sender, receiver, money >>

ProcSet == ({"t1"})

Init == (* Global variables *)
        /\ c1 = "c1"
        /\ c2 = "c2"
        /\ account = [c \in {"c1", "c2"} |-> 10]
        (* Process tx *)
        /\ receiver_new_amount = [self \in {"t1"} |-> 0]
        /\ sender_new_amount = [self \in {"t1"} |-> 0]
        /\ sender = [self \in {"t1"} |-> c1]
        /\ receiver = [self \in {"t1"} |-> c2]
        /\ money \in [{"t1"} -> 1..2]
        /\ pc = [self \in ProcSet |-> "ADAPT"]

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

TRANSFER_MONEY(self) == /\ pc[self] = "TRANSFER_MONEY"
                        /\ account' = [account EXCEPT ![sender[self]] = account[sender[self]] - money[self],
                                                      ![receiver[self]] = account[receiver[self]] + money[self]]
                        /\ pc' = [pc EXCEPT ![self] = "Done"]
                        /\ UNCHANGED << c1, c2, receiver_new_amount, 
                                        sender_new_amount, sender, receiver, 
                                        money >>

tx(self) == ADAPT(self) \/ TRANSFER_MONEY(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in {"t1"}: tx(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in {"t1"} : WF_vars(tx(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

CorrectTransfer ==
  \A t \in {"t1"}:
     <>(/\ pc[t] = "Done"
        /\ account["c1"] = 10 - money["t1"]
        /\ account["c2"] = 10 + money["t1"])

=============================================================================

Thank you

Em quinta-feira, 9 de abril de 2020 14:19:13 UTC-3, Markus Alexander Kuppe escreveu:

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