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