hybrid and parallel mode mask Translation Capacity Error

[soaresCecilia]

I'm using Alloy Analyzer 6.1.0, java version 15 and a macOS Monterey version 12.6, with 3,5 GHz Intel Core i7 dual core and 16GB of memory.

While specifying Paxos protocol I've observed that sometimes some Translation Capacity errors are masked by hybrid and parallel strategies. I have a big and silly example case to reproduce the error, but the intention it's to be able to show it.

open util/ordering[Ballot]

sig Value {}
sig Ballot {}
sig Acceptor {
    var maxBal : lone Ballot,
    var maxVote: lone Vote,
    var sent : Type -> Ballot -> Payload
}
sig Quorum {
    acceptors : some Acceptor
}
one sig None {}
abstract sig Type {}
one sig M1A,M1B,M2A,M2B extends Type {}
abstract sig Vote {
    value : Value,
    ballot : Ballot
}
sig Payload = Value + Vote + None {}

fact AllPossibleVotesExist {
    all v : Value, b : Ballot | some x : Vote | x.value = v and x.ballot = b
}
fact Quorums {
    all x,y : Quorum | some x.acceptors & y.acceptors
}
fact Init {
    no maxBal
    no maxVote
    no sent 
}
fact Next {
    always (nop or
        some b: Ballot | phase1A[b] or
        some a: Acceptor | phase2B[a])
}

pred phase1A[b: Ballot] {
    no Acceptor.sent[M1A][b]
    some a : Acceptor | sent' = sent + a->M1A->b->None
    maxBal' = maxBal
    maxVote' = maxVote
}
pred phase2B[a: Acceptor] { 
    some b : Ballot, x : Acceptor.sent[M1A][b], v : Vote {
        no a.sent[M2B][b]
        no a.maxBal or gte[b, a.maxBal]
        v.ballot = b and v.value = x
        maxBal' = maxBal ++ a->b
        maxVote' = maxVote ++ a->v
        sent' = sent + a->M2B->b->x
    }
}
pred nop {
    maxBal' = maxBal
    maxVote' = maxVote
    sent' = sent
}
pred chosenAt[b: Ballot, v: Value] {
    some q: Quorum | all a: q.acceptors | v in a.sent[M2B][b]
}

fun chosenValues : set Value {
    {v: Value | some b: Ballot | chosenAt[b, v]}
}

assert ChosenValue {
    always lone chosenValues
}   
check ChosenValue for exactly 3 Value, 2 Quorum, 
    exactly 3 Acceptor, exactly 4 Ballot, 
    exactly 12 Vote, 27..27 steps

When executing the check command with batch mode a translation capacity error occurs. However the same command and scope work in parallel and hybrid mode. Actually, the Analyzer returns, in few milliseconds, that "No counterexample found. Assertion may be valid.", even though it has not processed any variable. This can be seen in the picture below.

[nmacedo]

Fixed for 6.2 (Pardinus 1.3.1).