[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



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*
> |
> -------------------------------- 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
> 
> -- 
> 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
> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.
> 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>.

-- 
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/100f6816-95b7-db24-dc33-db9b86dc6199%40lemmster.de.