[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 10 Dec 2020 08:51:38 +0100*Cc*: Ivan Beschastnikh <bestchai@xxxxxxxxx>*References*: <CAJs285kRCQAH6JRsNGk5=tSOd==hcxqWELz1czii66CNgYPNZQ@mail.gmail.com>

I'd approach the problem in two steps: first make sure that all sub-blocks of statements assign to the same (versions of) variables. In your example: transform
into section2: if (x = 2) { x := x + 1; } else { x := x; } x := x + 1; In a second step, devise an approach to translation that works for such "balanced" input. For example, this could yield with (x0 = IF x=2 THEN x+1 ELSE x) { with (x1 = x0 + 1) { x := x1; } } Clearly, there will be tricky cases such as when there is involved control structure that need careful thinking. Perhaps some techniques used for single static assignment transformations used in compilers could be relevant here. My 2 cents, Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7AD6BCF6-67D1-4616-BD71-4F75CEB12C82%40gmail.com. |

**References**:**[tlaplus] Approaching repeated assignment in PlusCal***From:*Finn Hackett

- Prev by Date:
**Re: [tlaplus] Does WF and SF statements applicable in distributed Mode?** - Next by Date:
**Re: [tlaplus] Approaching repeated assignment in PlusCal** - Previous by thread:
**[tlaplus] Re: Approaching repeated assignment in PlusCal** - Next by thread:
**Re: [tlaplus] Approaching repeated assignment in PlusCal** - Index(es):