<NME> pcal-tla-to-code.txt
<BEF> TLA+ Error Reports That Can Be Mapped to PCal Code
---------------------------------------------------
- Parser Errors

- TLC errors. Expression evaluation in:
   * Initial predicate   
       This seems to just report a single location,
       exactly where the error occurs.
   * process set. (sometimes reports the ProcSet token,
   * expression in statement: can be
      + the expression
      + conjunct of action containing the expression
      + a previous conjunct of action
      + the last character of a previous conjunct
        (only on the first conjunct). This seems
        to be a minor TLC bug

- Error-Trace action location.
  (Double-click needed to go to TLA+ location.)
  (Double-click needed to go to TLA+ location.)

- Coverage.  Can go to
   * conjunction of action definition
   * variable in UNCHANGED expression
   * variable in vars location

Note: assertion failure error already maps to PCal code location.
(But not if file has been edited since last translator run.)
    
The Structure of the Translation
--------------------------------
<translation> ::=
   <Variables Declaration> 
   <vars Definition>
   [<ProcSet Definition>]0,1
   <Init Definition>
   <Action Def>+
   [<Process Def>]0,1
   <Next Def>
   <Spec Def>
   <Termination Def>

<Action Def> ::=
   <label> ["(self)"]0,1 == 
   "/\" <PC enabling Predicate>
   <Action Body>

<Action Body> ::=
   [   "/\" <Expr> 
     | "/\" <Assignment> 
     | "/\" <If-Then-Else>
   ]*
   ["/\" <pc-assignment>]0,1  \* An outer-most action body must have a pc-assignment
   ["/\" <Unchanged>]0,1      

<Assignment> ::= 
   <Variable>
    "' ="
   [   <Expr>
     | "[" <Variable> "EXCEPT" "!" [ "[self]" ]0,1 
                                   [    "." <String>  
                                     |  "[" <Expr> "]" 
                                   ]*
       "]"
   ]
    
<If-Then-Else> ::=
   "IF" <Expr>
   "THEN" <Action Body>
   "ELSE" <Action Body>
           
<Unchanged> ::=
    "UNCHANGED <<" <Variable> ["," <Variable>]* ">>" 
  | <Variable> "' =" <Variable>

Note: If the translator is modified to use a single TLA+ variable for
two different local PCal variables of the same name, then a variable
name in the TLA+ spec does not map to a unique piece of PCal code.

CONSTANT Location ,  _<:_
  \* A set of locations in the file, where a location is a
  \* position in the module.  More precisely, it represents
  \* a position between two characters.  That position can
  \* lie either within the PCal source code or of its TLA+ 
  \* translation.
  \*
  \* A location will be represented by a record
  \*
  \*      [line : LineNumber, col : ColumnNumber]
  \* 
  \* where a location loc represents the position to the right of character
  \* number loc.col on line loc.line, with loc.col = 0 being the position
  \* to the left of the first character on the line.
  \*
  \* The relation <: is the "equals or is to the left of" relation on 
  \* locations.

Region == [begin : Location, end : Location]
  \* A region represents a region of text within the TLA+ translation

A mapping specifier is a sequence of the following objects:

TLAToken == [type : {"token"},
             region  : Region]
  \* This represents a section of text in the TLA+ spec

Paren == [type       : {"begin", "end"} ,
          loc : : Location]
  \* Matching parens delimit the region of PlusCal code between
  \* the two locations.  (I might be a 

            \* I don't think this is needed.
          pcalRegion : Seq(RegionLoc)]
  \* Matching parens logically contain the same pcalRegion
  \* values.  However, it might be most convenient to 
  \* put them only in the end paren.

Break == [type  |-> "break",
          depth |-> Nat]
  \* Indicates the existence of a region of PlusCal code that
  \* is NOT part of the translation of a region of spec
  \* which contains the translation of parts of the spec on either
  \* side of the break.
  \*
  \* A depth of N indicates that if this break is at depth d,
  \* then it applies to all regions specified by parentheses of
  \* depth in d-N .. d

TransSpec 

A TransSpec specifier is an element of
Seq(TLAToken \cup Paren \cup {Break}) satisfying the following
conditions:

- For two successive TLATokens T1 and T2 (even if they have
  Parens or non-TLAToken objects between them), 
     T1.region.end :< T2.region.begin
- well formed (meaning all parentheses are in properly matched pairs)
- it begins/ends with begin/end Parens that delimit the
  PCal code of the entire algorithm.
- The location of a left paren is <: that of its matching
  right paren.
- Within any matching pair of parentheses at depth d, the
  parentheses at depth d+1 have locations in non-decreasing
  order.

The Translation Algorithm
 - An output subsequence of a TransSpec is 
   a subsequence that is well formed and for which every TLAToken
   is inside parentheses.
 - The region of PCal code corresponding to an output region 
   is defined as follows:
     - if the output region contains no breaks at parenthesis 
       depth 0, then it begins at the location of the left paren 
       that begins the region and ends at the location of the right 
       paren that ends the region.
     - if the output region contains breaks at paren depth 0,
       then it is the union of the regions of PCal code obtained
       by the collection of output regions obtained by splitting
       the given output region at its paren-depth 0 breaks.

  
HOW PlusCal AST CONSTRUCTS ARE MAPPED
---------------------------------

In the following, parentheses represent Paren objects in the 
TransSpec.  Parentheses in the PCal source represent the locations
pointed to by the corresponding Parens in the TransSpec.

[abc] represents a TLAToken object for text "abc".  In this
representation, we put literal parentheses and square brackets in
quotes.

The Objects of the TransSpec are placed underneath the corresponding
parts of the TLA+ spec so that [abc] is underneath the text "abc".

Note that some text in the TLA+ spec does not have a corresponding
[...] object in the TransSpec.  As far as the mapping is concerned,
such text is equivalent to white space.

^^{n} represents a break with depth n


TLAExpr
-------
  PCal Source

  macro mac(param) {
    ...
   
    x   +   param   +   y   with: parameter param replaced by a + b
   ( ) ( ) (     ) ( ) ( )
    ... }
   ...
   mac( a   +   b )
       ( ) ( ) ( )

  Translation
     x     +    (   a     +     b   )    +     y'
  (([ ]) ([ ])  ( ([ ]) ([ ]) ([ ]) )  ([ ]) ([  ])




Assign with multiple SingleAssign children
------------------------------------------
  PCal Source

      x [ a ] := e    ||  x[b] := f ||    y := g    ||  x[c] := h
  ( (    ( )    ( ) )    (  ...    )   ( ( )  ( ) )    (  ...    )

  Translation
          /\  /\ x' = [ x EXCEPT 
                            ![a] = e, 
                            ![b] = f, 
                            ![c] = h ]
              /\ y' = g   

      /\  /\  x' =  [  x EXCEPT 
   ( [                          ]

                       !     [   a   ]  =    e     , 
                     ([ ]      ([ ])   [ ] ([ ]) )

                       !     [   b   ]  =    f     , 
                     ([ ]      ([ ])   [ ] ([ ]) )   
                      
                      ^^{0}
                  
                       !     [   c   ]  =    h        ]
                     ([ ]      ([ ])   [ ] ([ ]) )  [   ]
                      
           /\    y'    =   g   
        ( [  ] ([  ]) [ ] ( ) )
    )

        

Assign with one SingleAssign
----------------------------
  PCal Source
        x := 1
     ( ( )  ( ) )

  Translation
       /\    x'    =    1
     ([  ] ([  ]) [ ] ([ ])     
   
    or
       /\    x'    =   [     x    EXCEPT ! [ self ]  =    1     ]
     ([  ] ([  ]) [=     ] ([ ]) [                    ] ([ ]) [   ] )

  PCal Source
         x   [  a   ,    b  ]  :=  e
      ( ( )    ( )      ( )       ( ) )

   Translation
          x'    = [x EXCEPT ![     a    ,    b    ] =     e    ]  
      ( ([  ]) [               ] ([ ]) [ ] ([ ]) [    ] ([ ]) [ ] )

   or
          x'    = [x EXCEPT ![self][     a    ,    b    ] =     e    ]  
      ( ([  ]) [                     ] ([ ]) [ ] ([ ]) [    ] ([ ]) [ ] )



LabeledStmt
----------
  PCal 
     lbl :  Stmt1 ; ... ; Stmt42
   (       (     )  ...  (     ) )

  Produces

     lbl ==  /\ pc = "lbl"
  ( [                      ]

             Translation(Stmt1)
            (     ...          )
             
                  ...

             Translation(Stmt42)
            (     ...          )

             Translation(Stmt1)
            (     ...          )

            /\ pc' = "..."       \* Not present if Stmt3 is a goto
          [                 ]

            /\ UNCHANGED ...     \* May not be present
          [                 ]
   )


   Note: In the Exploded AST, the pc = "lbl" is obtained from an AST.When
         and the pc' = ... from an AST.Assign.


Call
----
  PCal Code
      procedure P(param1, param2)
      variable   pvar1 = e  ,  pvar2 = f
     (          (       ( ))  (       ( ) ) )
        { plabel: ... }
      ...
          call P( arg1 , arg2 ) ;
         (       (    ) (    ) )
   rlbl : ...

   Exploded AST for the Call:
     Assign object with:
       ass |-> << [lhs |-> [var |-> param1, sub |-> null or <<self>>],
                   rhs |-> arg1],
                  [var |-> param2, sub |-> null or <<self>>],
                   rhs |-> arg2],
                  [lhs |-> [var |-> stack, sub |-> null or <<self>>],
                   rhs |-> ...],  \* don't try to deal with this rhs.
                >>

     Assign object with:
       ass |-> << [lhs -> [var |-> pvar1, sub |-> null or <<self>>],
                   rhs |-> e] >>

     Assign object with:
       ass |-> << [lhs -> [var |-> pvar2, sub |-> null or <<self>>],
                   rhs |-> f] >>

     Assign object with:
       ass |-> << [lhs -> [var |-> pc, sub |-> null or <<self>>],
                   rhs |-> "rlbl"] >>

  Produces
         /\  /\ param1' =    arg1
   ( [                   ] ([    ])
   
             /\ param2' =    arg2
     [            ] ([    ])
   
             /\ stack' = ...
     [                       ]

         /\ pvar1' =   e     or    /\ [pvar1 EXCEPT ![self] =    e    ]
     ( ([           ] ( ) )      ([                          ] ([ ]) [ ])

         /\ pvar2' =   f     or  ...
       ([           ] ( ) )      ...
     )
        /\ pc' = ...   or [pc EXCEPT ![self] = ...]
     [                                              ]
   )


Return
------
   PCal Code
      procedure P(param1, param2)
      variable pvar1 = e, pvar2 = f
        { ... 
          return }
      ...
          call P(arg1, arg2) ;
   rlbl : ...

   Translation
      This produces a lot of stuff that, if selected, should
      map to the return.

CallReturn
----------
   PCal Code:
        call P(param1, param2);
        return

   Translation
      Essentially the same as for Call.


While
-----
  PCal Code
    lbl:   while ( e ) {  Stmt1 ;  Stmt 2 ;
   (   (          ( )    (     )  (      )   ^^{1}

                          lbl2 : ...
                     };

           Stmt3 ;
          (      )

           Stmt4:
          (      )
       )
   )

    lbl3: ...
  
  Translation
     lbl ==     /\ pc = "lbl"
  ( [      ] ( [              ]              

                /\ IF    e
               [     ] ([ ]) 

                     THEN   Trans(Stmt1)
                    [    ] (   ...      )

                            Trans(Stmt2)
                           (            )

                          /\ pc' = "lbl2"
                        [                 ]

                          /\ UNCHANGED ...
                        [                  ]
               ^^^{1}

                     ELSE    Trans(Stmt3)
                    [    ]  (   ...      )

                             Trans(Stmt4)
                            (    ...     )

                          /\ pc' = "lbl3"
                        [                 ]

                          /\ UNCHANGED ..
                        [                 ]
              )
      )

NOTES
-----
- If the translator is modified to use a single TLA+ variable for
two different local PCal variables of the same name, then a variable
name in the TLA+ spec does not map to a unique piece of PCal code
in the <Variables Declaration> and <Init Definition>.  And additional
information will need to be kept to map variable names to the correct
PCal declaration for cases where there is a unique mapping.

- For a multi-assignment such as 

   x[i] := ... || x[j] := ...
   
the <Variable> of an <Assignment> does not correspond to a unique
occurrence of the variable in the PCal code.

- Among the stuff added in the translation are parentheses around expressions.

- The definition section should be handled by a 1-1 mapping between an area 
  of the spec and an area of the code.  That must be fit into any framework.

- Portions of the AST that result from macro expansion can be 
  indicated by a new AST subclass AST.MacroMarker whose objects
  mark the beginning and end of macro expansion, containing the
  location in the PlusCal code of the beginning and end of the
  macro statement. I don't think it needs to indicate the location
  of the arguments.

<MSG> 

git-svn-id: svn+ssh://svn.msr-inria.inria.fr/var/lib/svn/repository/tla/trunk/tla2-inria@24812 76a6fc44-f60b-0410-a9a8-e67b0e8fc65c

<DFF> @@ -10,10 +10,10 @@ TLA+ Error Reports That Can Be Mapped to PCal Code
    * expression in statement: can be
       + the expression
       + conjunct of action containing the expression
-      + a previous conjunct of action
-      + the last character of a previous conjunct
-        (only on the first conjunct). This seems
-        to be a minor TLC bug
+      + a previous conjunct of that action
+      + the last character (and perhaps more) of 
+        the first conjunct of that action.
+        This seems to be a minor TLC bug
 
 - Error-Trace action location.
   (Double-click needed to go to TLA+ location.)
@@ -75,4 +75,7 @@ The Structure of the Translation
 
 Note: If the translator is modified to use a single TLA+ variable for
 two different local PCal variables of the same name, then a variable
-name in the TLA+ spec does not map to a unique piece of PCal code.
+name in the TLA+ spec does not map to a unique piece of PCal code
+in the <Variables Declaration> and <Init Definition>.  And additional
+information will need to be kept to map variable names to the correct
+PCal declaration for cases where there is a unique mapping.

{'commit': 'diff --git a/general/docs/pcal-tla-to-code.txt b/general/docs/pcal-tla-to-code.txt\nindex ce7a20ddd..3096a2b2c 100644\n--- a/general/docs/pcal-tla-to-code.txt\n+++ b/general/docs/pcal-tla-to-code.txt\n@@ -10,10 +10,10 @@ TLA+ Error Reports That Can Be Mapped to PCal Code\n    * expression in statement: can be\r\n       + the expression\r\n       + conjunct of action containing the expression\r\n-      + a previous conjunct of action\r\n-      + the last character of a previous conjunct\r\n-        (only on the first conjunct). This seems\r\n-        to be a minor TLC bug\r\n+      + a previous conjunct of that action\r\n+      + the last character (and perhaps more) of \r\n+        the first conjunct of that action.\r\n+        This seems to be a minor TLC bug\r\n \r\n - Error-Trace action location.\r\n   (Double-click needed to go to TLA+ location.)\r\n@@ -75,4 +75,7 @@ The Structure of the Translation\n \r\n Note: If the translator is modified to use a single TLA+ variable for\r\n two different local PCal variables of the same name, then a variable\r\n-name in the TLA+ spec does not map to a unique piece of PCal code.\r\n+name in the TLA+ spec does not map to a unique piece of PCal code\r\n+in the <Variables Declaration> and <Init Definition>.  And additional\r\n+information will need to be kept to map variable names to the correct\r\n+PCal declaration for cases where there is a unique mapping.\r\n', 'commit_subject': '', 'repo_name': 'tlaplus/tlaplus', 'committer': {'name': 'lamport', 'email': 'c357616dd61d2ecbc8f5c427eb31f61e7f68ce4b@76a6fc44-f60b-0410-a9a8-e67b0e8fc65c', 'time_sec': '1322452100', 'tz_offset': '0', 'date': {'seconds': '1322452100'}}, 'commit_tree': '5cb0c086cae9141b98b9c8e576ad69f1b27d632b', 'commit_message': '\n\ngit-svn-id: svn+ssh://svn.msr-inria.inria.fr/var/lib/svn/repository/tla/trunk/tla2-inria@24812 76a6fc44-f60b-0410-a9a8-e67b0e8fc65c\n', 'language_name': 'R', 'license': 'mit', 'hunks': '@@ -10,10 +10,10 @@ TLA+ Error Reports That Can Be Mapped to PCal Code\n    * expression in statement: can be\r\n       + the expression\r\n       + conjunct of action containing the expression\r\n-      + a previous conjunct of action\r\n-      + the last character of a previous conjunct\r\n-        (only on the first conjunct). This seems\r\n-        to be a minor TLC bug\r\n+      + a previous conjunct of that action\r\n+      + the last character (and perhaps more) of \r\n+        the first conjunct of that action.\r\n+        This seems to be a minor TLC bug\r\n \r\n - Error-Trace action location.\r\n   (Double-click needed to go to TLA+ location.)\r\n@@ -75,4 +75,7 @@ The Structure of the Translation\n \r\n Note: If the translator is modified to use a single TLA+ variable for\r\n two different local PCal variables of the same name, then a variable\r\n-name in the TLA+ spec does not map to a unique piece of PCal code.\r\n+name in the TLA+ spec does not map to a unique piece of PCal code\r\n+in the <Variables Declaration> and <Init Definition>.  And additional\r\n+information will need to be kept to map variable names to the correct\r\n+PCal declaration for cases where there is a unique mapping.\r\n', 'addition_count': 8, 'deletion_count': 5, 'src_file': 'a/general/docs/pcal-tla-to-code.txt', 'tgt_file': 'b/general/docs/pcal-tla-to-code.txt', 'file_extension': '.txt', 'before_file': 'TLA+ Error Reports That Can Be Mapped to PCal Code\n---------------------------------------------------\n- Parser Errors\n\n- TLC errors. Expression evaluation in:\n   * Initial predicate   \n       This seems to just report a single location,\n       exactly where the error occurs.\n   * process set. (sometimes reports the ProcSet token,\n   * expression in statement: can be\r\n      + the expression\r\n      + conjunct of action containing the expression\r\n      + a previous conjunct of action\r\n      + the last character of a previous conjunct\r\n        (only on the first conjunct). This seems\r\n        to be a minor TLC bug\r\n\r\n- Error-Trace action location.\r\n  (Double-click needed to go to TLA+ location.)\r\n  (Double-click needed to go to TLA+ location.)\n\n- Coverage.  Can go to\n   * conjunction of action definition\n   * variable in UNCHANGED expression\n   * variable in vars location\n\nNote: assertion failure error already maps to PCal code location.\n(But not if file has been edited since last translator run.)\n    \nThe Structure of the Translation\n--------------------------------\n<translation> ::=\n   <Variables Declaration> \n   <vars Definition>\n   [<ProcSet Definition>]0,1\n   <Init Definition>\n   <Action Def>+\n   [<Process Def>]0,1\n   <Next Def>\n   <Spec Def>\n   <Termination Def>\n\n<Action Def> ::=\n   <label> ["(self)"]0,1 == \n   "/\\" <PC enabling Predicate>\n   <Action Body>\n\n<Action Body> ::=\n   [   "/\\" <Expr> \n     | "/\\" <Assignment> \n     | "/\\" <If-Then-Else>\n   ]*\n   ["/\\" <pc-assignment>]0,1  \\* An outer-most action body must have a pc-assignment\n   ["/\\" <Unchanged>]0,1      \n\n<Assignment> ::= \n   <Variable>\n    "\' ="\n   [   <Expr>\n     | "[" <Variable> "EXCEPT" "!" [ "[self]" ]0,1 \n                                   [    "." <String>  \n                                     |  "[" <Expr> "]" \n                                   ]*\n       "]"\n   ]\n    \n<If-Then-Else> ::=\n   "IF" <Expr>\n   "THEN" <Action Body>\n   "ELSE" <Action Body>\n           \n<Unchanged> ::=\n    "UNCHANGED <<" <Variable> ["," <Variable>]* ">>" \n  | <Variable> "\' =" <Variable>\n\r\nNote: If the translator is modified to use a single TLA+ variable for\r\ntwo different local PCal variables of the same name, then a variable\r\nname in the TLA+ spec does not map to a unique piece of PCal code.\r\n\nCONSTANT Location ,  _<:_\n  \\* A set of locations in the file, where a location is a\n  \\* position in the module.  More precisely, it represents\n  \\* a position between two characters.  That position can\n  \\* lie either within the PCal source code or of its TLA+ \n  \\* translation.\n  \\*\n  \\* A location will be represented by a record\n  \\*\n  \\*      [line : LineNumber, col : ColumnNumber]\n  \\* \n  \\* where a location loc represents the position to the right of character\n  \\* number loc.col on line loc.line, with loc.col = 0 being the position\n  \\* to the left of the first character on the line.\n  \\*\n  \\* The relation <: is the "equals or is to the left of" relation on \n  \\* locations.\n\nRegion == [begin : Location, end : Location]\n  \\* A region represents a region of text within the TLA+ translation\n\nA mapping specifier is a sequence of the following objects:\n\nTLAToken == [type : {"token"},\n             region  : Region]\n  \\* This represents a section of text in the TLA+ spec\n\nParen == [type       : {"begin", "end"} ,\n          loc : : Location]\n  \\* Matching parens delimit the region of PlusCal code between\n  \\* the two locations.  (I might be a \n\n            \\* I don\'t think this is needed.\n          pcalRegion : Seq(RegionLoc)]\n  \\* Matching parens logically contain the same pcalRegion\n  \\* values.  However, it might be most convenient to \n  \\* put them only in the end paren.\n\nBreak == [type  |-> "break",\n          depth |-> Nat]\n  \\* Indicates the existence of a region of PlusCal code that\n  \\* is NOT part of the translation of a region of spec\n  \\* which contains the translation of parts of the spec on either\n  \\* side of the break.\n  \\*\n  \\* A depth of N indicates that if this break is at depth d,\n  \\* then it applies to all regions specified by parentheses of\n  \\* depth in d-N .. d\n\nTransSpec \n\nA TransSpec specifier is an element of\nSeq(TLAToken \\cup Paren \\cup {Break}) satisfying the following\nconditions:\n\n- For two successive TLATokens T1 and T2 (even if they have\n  Parens or non-TLAToken objects between them), \n     T1.region.end :< T2.region.begin\n- well formed (meaning all parentheses are in properly matched pairs)\n- it begins/ends with begin/end Parens that delimit the\n  PCal code of the entire algorithm.\n- The location of a left paren is <: that of its matching\n  right paren.\n- Within any matching pair of parentheses at depth d, the\n  parentheses at depth d+1 have locations in non-decreasing\n  order.\n\nThe Translation Algorithm\n - An output subsequence of a TransSpec is \n   a subsequence that is well formed and for which every TLAToken\n   is inside parentheses.\n - The region of PCal code corresponding to an output region \n   is defined as follows:\n     - if the output region contains no breaks at parenthesis \n       depth 0, then it begins at the location of the left paren \n       that begins the region and ends at the location of the right \n       paren that ends the region.\n     - if the output region contains breaks at paren depth 0,\n       then it is the union of the regions of PCal code obtained\n       by the collection of output regions obtained by splitting\n       the given output region at its paren-depth 0 breaks.\n\n  \nHOW PlusCal AST CONSTRUCTS ARE MAPPED\n---------------------------------\n\nIn the following, parentheses represent Paren objects in the \nTransSpec.  Parentheses in the PCal source represent the locations\npointed to by the corresponding Parens in the TransSpec.\n\n[abc] represents a TLAToken object for text "abc".  In this\nrepresentation, we put literal parentheses and square brackets in\nquotes.\n\nThe Objects of the TransSpec are placed underneath the corresponding\nparts of the TLA+ spec so that [abc] is underneath the text "abc".\n\nNote that some text in the TLA+ spec does not have a corresponding\n[...] object in the TransSpec.  As far as the mapping is concerned,\nsuch text is equivalent to white space.\n\n^^{n} represents a break with depth n\n\n\nTLAExpr\n-------\n  PCal Source\n\n  macro mac(param) {\n    ...\n   \n    x   +   param   +   y   with: parameter param replaced by a + b\n   ( ) ( ) (     ) ( ) ( )\n    ... }\n   ...\n   mac( a   +   b )\n       ( ) ( ) ( )\n\n  Translation\n     x     +    (   a     +     b   )    +     y\'\n  (([ ]) ([ ])  ( ([ ]) ([ ]) ([ ]) )  ([ ]) ([  ])\n\n\n\n\nAssign with multiple SingleAssign children\n------------------------------------------\n  PCal Source\n\n      x [ a ] := e    ||  x[b] := f ||    y := g    ||  x[c] := h\n  ( (    ( )    ( ) )    (  ...    )   ( ( )  ( ) )    (  ...    )\n\n  Translation\n          /\\  /\\ x\' = [ x EXCEPT \n                            ![a] = e, \n                            ![b] = f, \n                            ![c] = h ]\n              /\\ y\' = g   \n\n      /\\  /\\  x\' =  [  x EXCEPT \n   ( [                          ]\n\n                       !     [   a   ]  =    e     , \n                     ([ ]      ([ ])   [ ] ([ ]) )\n\n                       !     [   b   ]  =    f     , \n                     ([ ]      ([ ])   [ ] ([ ]) )   \n                      \n                      ^^{0}\n                  \n                       !     [   c   ]  =    h        ]\n                     ([ ]      ([ ])   [ ] ([ ]) )  [   ]\n                      \n           /\\    y\'    =   g   \n        ( [  ] ([  ]) [ ] ( ) )\n    )\n\n        \n\nAssign with one SingleAssign\n----------------------------\n  PCal Source\n        x := 1\n     ( ( )  ( ) )\n\n  Translation\n       /\\    x\'    =    1\n     ([  ] ([  ]) [ ] ([ ])     \n   \n    or\n       /\\    x\'    =   [     x    EXCEPT ! [ self ]  =    1     ]\n     ([  ] ([  ]) [=     ] ([ ]) [                    ] ([ ]) [   ] )\n\n  PCal Source\n         x   [  a   ,    b  ]  :=  e\n      ( ( )    ( )      ( )       ( ) )\n\n   Translation\n          x\'    = [x EXCEPT ![     a    ,    b    ] =     e    ]  \n      ( ([  ]) [               ] ([ ]) [ ] ([ ]) [    ] ([ ]) [ ] )\n\n   or\n          x\'    = [x EXCEPT ![self][     a    ,    b    ] =     e    ]  \n      ( ([  ]) [                     ] ([ ]) [ ] ([ ]) [    ] ([ ]) [ ] )\n\n\n\nLabeledStmt\n----------\n  PCal \n     lbl :  Stmt1 ; ... ; Stmt42\n   (       (     )  ...  (     ) )\n\n  Produces\n\n     lbl ==  /\\ pc = "lbl"\n  ( [                      ]\n\n             Translation(Stmt1)\n            (     ...          )\n             \n                  ...\n\n             Translation(Stmt42)\n            (     ...          )\n\n             Translation(Stmt1)\n            (     ...          )\n\n            /\\ pc\' = "..."       \\* Not present if Stmt3 is a goto\n          [                 ]\n\n            /\\ UNCHANGED ...     \\* May not be present\n          [                 ]\n   )\n\n\n   Note: In the Exploded AST, the pc = "lbl" is obtained from an AST.When\n         and the pc\' = ... from an AST.Assign.\n\n\nCall\n----\n  PCal Code\n      procedure P(param1, param2)\n      variable   pvar1 = e  ,  pvar2 = f\n     (          (       ( ))  (       ( ) ) )\n        { plabel: ... }\n      ...\n          call P( arg1 , arg2 ) ;\n         (       (    ) (    ) )\n   rlbl : ...\n\n   Exploded AST for the Call:\n     Assign object with:\n       ass |-> << [lhs |-> [var |-> param1, sub |-> null or <<self>>],\n                   rhs |-> arg1],\n                  [var |-> param2, sub |-> null or <<self>>],\n                   rhs |-> arg2],\n                  [lhs |-> [var |-> stack, sub |-> null or <<self>>],\n                   rhs |-> ...],  \\* don\'t try to deal with this rhs.\n                >>\n\n     Assign object with:\n       ass |-> << [lhs -> [var |-> pvar1, sub |-> null or <<self>>],\n                   rhs |-> e] >>\n\n     Assign object with:\n       ass |-> << [lhs -> [var |-> pvar2, sub |-> null or <<self>>],\n                   rhs |-> f] >>\n\n     Assign object with:\n       ass |-> << [lhs -> [var |-> pc, sub |-> null or <<self>>],\n                   rhs |-> "rlbl"] >>\n\n  Produces\n         /\\  /\\ param1\' =    arg1\n   ( [                   ] ([    ])\n   \n             /\\ param2\' =    arg2\n     [            ] ([    ])\n   \n             /\\ stack\' = ...\n     [                       ]\n\n         /\\ pvar1\' =   e     or    /\\ [pvar1 EXCEPT ![self] =    e    ]\n     ( ([           ] ( ) )      ([                          ] ([ ]) [ ])\n\n         /\\ pvar2\' =   f     or  ...\n       ([           ] ( ) )      ...\n     )\n        /\\ pc\' = ...   or [pc EXCEPT ![self] = ...]\n     [                                              ]\n   )\n\n\nReturn\n------\n   PCal Code\n      procedure P(param1, param2)\n      variable pvar1 = e, pvar2 = f\n        { ... \n          return }\n      ...\n          call P(arg1, arg2) ;\n   rlbl : ...\n\n   Translation\n      This produces a lot of stuff that, if selected, should\n      map to the return.\n\nCallReturn\n----------\n   PCal Code:\n        call P(param1, param2);\n        return\n\n   Translation\n      Essentially the same as for Call.\n\n\nWhile\n-----\n  PCal Code\n    lbl:   while ( e ) {  Stmt1 ;  Stmt 2 ;\n   (   (          ( )    (     )  (      )   ^^{1}\n\n                          lbl2 : ...\n                     };\n\n           Stmt3 ;\n          (      )\n\n           Stmt4:\n          (      )\n       )\n   )\n\n    lbl3: ...\n  \n  Translation\n     lbl ==     /\\ pc = "lbl"\n  ( [      ] ( [              ]              \n\n                /\\ IF    e\n               [     ] ([ ]) \n\n                     THEN   Trans(Stmt1)\n                    [    ] (   ...      )\n\n                            Trans(Stmt2)\n                           (            )\n\n                          /\\ pc\' = "lbl2"\n                        [                 ]\n\n                          /\\ UNCHANGED ...\n                        [                  ]\n               ^^^{1}\n\n                     ELSE    Trans(Stmt3)\n                    [    ]  (   ...      )\n\n                             Trans(Stmt4)\n                            (    ...     )\n\n                          /\\ pc\' = "lbl3"\n                        [                 ]\n\n                          /\\ UNCHANGED ..\n                        [                 ]\n              )\n      )\n\nNOTES\n-----\n- If the translator is modified to use a single TLA+ variable for\ntwo different local PCal variables of the same name, then a variable\nname in the TLA+ spec does not map to a unique piece of PCal code\nin the <Variables Declaration> and <Init Definition>.  And additional\ninformation will need to be kept to map variable names to the correct\nPCal declaration for cases where there is a unique mapping.\n\n- For a multi-assignment such as \n\n   x[i] := ... || x[j] := ...\n   \nthe <Variable> of an <Assignment> does not correspond to a unique\noccurrence of the variable in the PCal code.\n\n- Among the stuff added in the translation are parentheses around expressions.\n\n- The definition section should be handled by a 1-1 mapping between an area \n  of the spec and an area of the code.  That must be fit into any framework.\n\n- Portions of the AST that result from macro expansion can be \n  indicated by a new AST subclass AST.MacroMarker whose objects\n  mark the beginning and end of macro expansion, containing the\n  location in the PlusCal code of the beginning and end of the\n  macro statement. I don\'t think it needs to indicate the location\n  of the arguments.\n', 'message': '\n\ngit-svn-id: svn+ssh://svn.msr-inria.inria.fr/var/lib/svn/repository/tla/trunk/tla2-inria@24812 76a6fc44-f60b-0410-a9a8-e67b0e8fc65c\n', 'author_name': 'lamport', 'lang': 'txt'}