PlusCal Translation Problem

[Lu, Huaixi]

Hi,

 

I came across a problem related to PlusCal Translation.

Each process in A maintains a queue, but if another process called “b1” tries to work on one of the queues like “bb: queue["a1"] := queue["a1"] \cup {"temp"};”, it will be translated into “queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}]”. But queue doesn’t have a field named “b1” or a variable called queue…

 

Do you know how to deal with this problem? The example code is attached.

 

Best,

Huaixi

 

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

EXTENDS Integers, TLC

\* TLC is used to assert

 

         

(* --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