使用Spin 6.4.8运行Promela模型时遭遇channels数组索引错误求助

Ah, I recognize this issue—Promela's modulo operator has a tricky behavior with negative numbers that trips up a lot of folks! Let's figure out why you're seeing that indexing channels[-1] error and fix it.

What's Causing the Error? #

The error occurs because when your node process has _pid = 0, the calculation (_pid - 1) % 3 evaluates to -1 in Promela, not the 2 you're expecting. Unlike standard mathematical modulo (which wraps negative results into positive indices), Promela's % operator preserves the sign of the dividend.

Even though you added an if block to correct pred when it equals -1, if your code attempts to access channels[pred] before that correction runs (or if there's an unexpected code path that skips the fix), you'll hit the invalid negative index error.

Solutions to Fix the Issue #

Solution 1: Calculate Predecessor Without Negative Values (Cleanest Approach)

Instead of relying on a conditional fix after the fact, adjust your pred calculation to always produce a valid non-negative index right away. For a 3-node ring, the predecessor of node _pid can be safely calculated as:

short pred = (_pid + 2) % 3;

This works because:

• For _pid = 0: (0 + 2) % 3 = 2 (correct predecessor)
• For _pid = 1: (1 + 2) % 3 = 0 (correct predecessor)
• For _pid = 2: (2 + 2) % 3 = 1 (correct predecessor)

Solution 2: Ensure Correction Runs Before Channel Access

If you prefer to keep your original calculation, double-check that the if block fixing pred = -1 executes before you try to access channels[pred]. Your code snippet shows the fix comes before the channel access, but verify there are no early branches (like goto statements) that skip this correction step.

Corrected Code Example #

Here's the revised code using Solution 1, which eliminates the need for the conditional fix entirely:

chan channels[3] = [1] of { pid };
active [3] proctype node () {
    // Calculate pred without negative values
    short pred = (_pid + 2) % 3;
    short succ = (_pid + 1) % 3;
    printf("Values(%d): %d, %d\n", _pid, pred, succ);
    printf("Corrected Values(%d): %d, %d\n", _pid, pred, succ);
    chan pc = channels[pred];
    // Rest of your code here...
}

内容的提问来源于stack exchange，提问作者Patrick Trentin