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

[Paulo Feodrippe]

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 and running the model, 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/

[Markus Kuppe]

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

[Paulo Feodrippe]

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

[Markus Kuppe]

Hi Paulo,

you cannot use an *operator* override to override *actions*. TLC's
latest nightly builds, however, come with another mechanism with which
you can - kind of - override actions [1,2]. Beware, this doesn't work
with liveness (ENABLED act)!

Why do you want to override actions in the first place?

Markus

[1]
https://github.com/tlaplus/tlaplus/blob/0ec35c7fae688523deca1b5e7bc7c4488ee547fd/tlatools/org.lamport.tlatools/test/tlc2/tool/EvaluatingValueTest.java#L63-L71
[2]
https://github.com/tlaplus/tlaplus/commit/0ec35c7fae688523deca1b5e7bc7c4488ee547fd#

On 09.04.20 10:32, Paulo Feodrippe wrote:
> 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*

> --
> 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+u...@googlegroups.com
> <mailto:tlaplus+u...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/08977102-5185-49db-a353-2f32ffeb8894%40googlegroups.com
> <https://groups.google.com/d/msgid/tlaplus/08977102-5185-49db-a353-2f32ffeb8894%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Paulo Feodrippe]

Hi Markus,

It's not TLA+ use case, It's little hacky, I've made a library where I can "label" Clojure code and control the scheduling of concurrent code (very basic compared to TLC scheduling). I was trying to override the actions (the translated labels from pluscal) to use the implementation code instead, but probably it really could be done using operators overriding.

I will take a look at these action overriding, maybe it's what I need \o/

I think this thread can be considered "closed", I have the necessary information, thanks :)

See ya o/