PlusCal Translation problem

[luhuai...@gmail.com]

Hi,

I encounter a problem regarding with PlusCal translation. 

One simple example is below: each process in A holds a queue; 

but if a process called "b1" work on one queue like "bb: queue["a1"] := queue["a1"] \cup {"temp"};", it will be translated to queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}];

but queue doesn't have a field called "b1"...

Do you know how to deal with this problem?

Best,

Huaixi

-------------------------------- MODULE test --------------------------------

EXTENDS Integers, TLC

         

(* --algorithm test {

    define {

        A == {"a1", "a2"}

    }

    fair process (a \in A)

    variable queue = {};

    {

        aa: skip

    }

    

    fair process (b = "b1")

    {

        bb: queue["a1"] := queue["a1"] \cup {"temp"};

    }

}

*)

\* BEGIN TRANSLATION - the hash of the PCal code: PCal-a27fafedd7e2ba12347a0c996d5f9fc3

VARIABLE pc

(* define statement *)

A == {"a1", "a2"}

VARIABLE queue

vars == << pc, queue >>

ProcSet == (A) \cup {"b1"}

Init == (* Process a *)

        /\ queue = [self \in A |-> {}]

        /\ pc = [self \in ProcSet |-> CASE self \in A -> "aa"

                                        [] self = "b1" -> "bb"]

aa(self) == /\ pc[self] = "aa"

            /\ TRUE

            /\ pc' = [pc EXCEPT ![self] = "Done"]

            /\ queue' = queue

a(self) == aa(self)

bb == /\ pc["b1"] = "bb"

      /\ queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}]

      /\ pc' = [pc EXCEPT !["b1"] = "Done"]

b == bb

(* Allow infinite stuttering to prevent deadlock on termination. *)

Terminating == /\ \A self \in ProcSet: pc[self] = "Done"

               /\ UNCHANGED vars

Next == b

           \/ (\E self \in A: a(self))

           \/ Terminating

Spec == /\ Init /\ [][Next]_vars

        /\ \A self \in A : WF_vars(a(self))

        /\ WF_vars(b)

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

\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-87e5d335b185538961bc5497fdefd792

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

\* Modification History

\* Last modified Wed Jul 29 16:27:10 EDT 2020 by huaixl

\* Created Wed Jul 29 16:18:17 EDT 2020 by huaixl

[David N. Jansen]

Hi Huaixi,

> Op 29 jul. 2020, om 22:30 heeft luhuai...@gmail.com het volgende geschreven:
>
> Hi,
>
> I encounter a problem regarding with PlusCal translation.
>
> One simple example is below: each process in A holds a queue;
>
> but if a process called "b1" work on one queue like "bb: queue["a1"] := queue["a1"] \cup {"temp"};", it will be translated to queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}];
>
> but queue doesn't have a field called "b1"...
>
> Do you know how to deal with this problem?

In your code, queue is defined to be a variable of process A, not a global variable. Therefore, if process B refers to the variable, it is assumed to be a local variable as well. If you want to communicate between processes, you should define queue to be a global variable, perhaps like this:

(* --algorithm test {
variable queue = [a \in A |-> {}]; (* yes, it is ok to use A here; the translation will place the initialisation after the definition of A *)

define {
A == {"a1", "a2"}
}

fair process (a \in A)

{
aa: skip; (* refer to the queue variable as "queue[self]" *)

}

fair process (b = "b1")
{
bb: queue["a1"] := queue["a1"] \cup {"temp"};
}
}*)

Kind regards,
David N. Jansen.