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 >>
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.
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
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; }}
-------------------------------- 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 TRANSLATIONVARIABLES 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"])
=============================================================================
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/