Hi,
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 {
variables
sales = {1, 2, 3},
stock = 10,
lock = 0;
define {
StockNotUnderZero == stock >= 0
StockEmpty == stock = 0
StockGetsEmptied == <>[]StockEmpty
}
fair process (sale \in sales) {
Loop:
while (TRUE) {
RequestLock:
if (~(lock = self)) {
await lock = 0;
if (stock >= self) {
lock := self;
};
};
ReduceStock:
if (lock = self) {
stock := stock - self;
};
RemoveLock:
if (lock = self) {
lock := 0;
};
Break:
skip;
}
};
}*)
----------------------------------------------------------------------