1. In the meeting on 25.7.06 it was suggested to adopt the SVA semantics and not trigger procedural blocks on the empty word. see details (here)
2. Cindy: in {a;b[*]$A$;c}, 'A' should be triggered after each 'a' (because we have seen b[*]).
3. Johan: If we adopt the SVA expansion rule for psl we would have b[*]$A$ ==> b[*]:1$A$. one could still express what Cindy is suggesting by (a;b[*])$A$;c
4. Dmitry P: A problem in SVA's semantics: while a;b[*];c holds on the trace 'ac', a;b[*]$A$;c does not hold on this trace, because it requires a cycle between the occurences of a and c. That is, adding a procedural block to the sequence changes its semantics.
5. Dana: To avoid this problem the syntax should require the procedural block to be attached to a certain boolean expression rather than a certain sub-sere.
6. Dmitry P: the requirement on R to be a simple boolean is too restrictive. It is not possible to write things like b[*2]$A$.
7. We thought of separating p.b. into two cathegories: "pure" and "impure" procedural blocks.
   • Pure procedural blocks are guaranteed not to change the model (change of local variable is not considered model change). Tools should ensure this policy is not violated.
   • Impure procedural blocks are totally free and can do everything.
   • New keyword "impure" is introduced to differentiate impure procedural blocks. All procedural blocks are considered pure by default, unless "impure" is specified.
8. Procedural blocks can contain any code as defined by the flavor language as long as it obeys the pure/impure classification.
9. We realized impure procedural blocks are not well-defined. Particularly, when assignments to global variables are performed is not well defined.
10. We decided to give-up impure procedural blocks. The 2 requirements that will not be achieved without them are cooperation between assertions and chanign the environemnt.
11. We still want to be able to print inside procedural blocks and therefore need to refine the definition of procedural blocks.

1. Procedural blocks will not be triggered on the empty word.
2. A special syntax should be defined for attaching a procedural block to a boolean expression. Procedural blocks attached to a general SERE will be acheived by syntactic sugaring.
3. In overlapping operators (fusion and |->) the procedural blocks of the left operand should be triggered before evaluation of the right operand.
4. Procedural blocks can change only local variables and print.
5. The syntax for procedural blocks: {SERE}$ procedural block text $

1. Flows in Johan's last proposal: <<>> is not associatives. s is not equivalent to 's && s' (details are in Johan's email from 28 Nov 06)
2. Flows in Dana's previous proposal that can be found here : Does not handle changes of the local variables on a single letter, e.g. as may happen with the ":" operator. This produces a disconnection between the semantics of ":" and the semantics of "|->" (details are in Johan's email from 12 Dec 06).

1. <(),(ab),(),(),...> |= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == 1 || v == -1}
2. <(),(ab),(),(),...> |/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == 1}
3. <(),(ab),(),(),...> |/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {v == -1}
4. <(),(ab),(),(),...> |= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b ; {v == 1}}!
5. <(),(ab),(),(),...> |= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b ; {v == -1}}!
6. <(),(ab),(),(),...> |/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==1)}
7. <(),(ab),(),(),...> |/= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==-1)}
8. <(),(ab),(),(),...> |= {{1$v:=0;$} ; {a$v:=v+1;$}[*] ; {b$v:=v-1;$}[*] ; !b} |=> {true; prev(v==1 | v== -1)}

Remains to be Done

• Need to revise Proposal A' of the formal semantics to replace the syntax rule for simple local variable assignment by a rule for attaching a general procedural block to a boolean.
• Formally define triggering of procedural blocks.
• Refine the "pure" requirement to allow printing inside procedural blocks.

LRM Changes