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

[tlaplus] Re: I can't find why can't I make this process fair

Level-checking error. Make sales a constant, not a variable.

On Friday, January 13, 2023 at 4:57:54 AM UTC-5 j.cabel...@xxxxxxxxx wrote:
Ignore the Break label, was running an experiment and left it there accidentally.

El viernes, 13 de enero de 2023 a las 9:57:41 UTC+1, Yeray Cabello escribió:

I'm trying to explain pessimistic locking to a colleague using this simple pluscal scenario, I wanted to show the temporal rule that the inventory gets eventually used up with the temporal formula. If the process it's not fair, stuttering causes the temporal invariiant to not hold, but if it's fair, I get this error:

TLC cannot handle the temporal formula line 104, col 12 to line 104, col 50 of module warehouse:

In evaluation, the identifier sales is either undefined or not an operator.
line 104, col 24 to line 104, col 28 of module warehouse

The line of the translation that throws it is:
Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in sales : WF_vars(sale(self))

Thing is sales IS defined in the translation and is part of vars, so I'm out of my depth trying to figure this out.

This is the whole algorithm, translation omitted for brevity:
----------------------------- MODULE warehouse -----------------------------
EXTENDS Integers
(*--algorithm wire {
  sales = {1, 2, 3},
  stock = 10,
  lock = 0;
define {
  StockNotUnderZero == stock >= 0
  StockEmpty == stock = 0
  StockGetsEmptied == <>[]StockEmpty

fair process (sale \in sales) {
  while (TRUE) {
      if (~(lock = self)) {
        await lock = 0;
        if (stock >= self) {
          lock := self;
      if (lock = self) {
        stock := stock - self;
      if (lock = self) {
        lock := 0;


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/36f0fede-360c-4ffa-9f50-4fd4bc20db11n%40googlegroups.com.