Recording these formulas would give different results. The first one should be false and the other one is true.

[lazkany]

channels: c, empty, g1, g2,vmm1,vmm2,vmm3,t
enum rolevals {clnt, vm, mgr}
enum msgvals {reserve, request, release, buy, connect, full,complete}
message-structure: MSG : msgvals, LNK : channel
communication-variables: cv : rolevals
guard g(r : rolevals, c : channel, m : channel) := (channel == *) && (@cv == r) | (channel == c) && (@cv == mgr) | (channel == m) ;

agent Client
    local: role : rolevals, cLink : channel, mLink : channel, tLink : channel
    init: cLink == c && mLink == empty && tLink == t && role==clnt
    relabel:
        cv <- role
    receive-guard: (channel == *) | (channel == cLink) | (channel == tLink)

    repeat: (
            (sReserve: <cLink==c> *! g(role,cLink,mLink)(MSG := reserve)[cLink := c]
            +
            rReserve: < cLink==c && MSG == reserve> *? [cLink := empty]
            )
            ;

            (sRequest: <cLink!=empty> cLink! g(role,cLink,mLink)(MSG := request)[cLink := c];
             rConnect: <mLink==empty && MSG == connect> cLink? [mLink := LNK];
             sRelease: <TRUE> *! g(role,cLink,mLink)(MSG := release)[cLink := empty];
             sBuy: <mLink!=empty> mLink! g(role,cLink,mLink)(MSG := buy)[mLink := empty];
             (
                sSolve: <TRUE> tLink! g(role,cLink,tLink)(MSG := complete)[]
               +
                <MSG == complete> tLink? []
             )

            +
             rRelease: <cLink==empty && MSG == release> *? [cLink := c]
            )
            )

agent Manager
    local: role : rolevals, cLink : channel, sLink : channel, hLink : channel
    init: hLink == g1 && sLink == g2 && cLink == c && role==mgr
    relabel:
        cv <- role
    receive-guard: (channel == *) | (channel == cLink) | (channel == hLink)

    repeat: (
            rRequest: <MSG == request> cLink? [];
            sForward: <TRUE> hLink! (TRUE)(MSG := request)[];
            (
             rep (rFull: <MSG == full> hLink? [];
                  sRequest: <TRUE> sLink! (TRUE)(MSG := request)[]
                 )
             +
             rConnect: <MSG == connect> cLink? []
            )
            )

agent Machine
    local: gLink : channel, pLink : channel, cLink : channel, asgn : bool
    init: !asgn && (cLink == empty)
    relabel:
        cv <- vm
    receive-guard: (channel == *) | (channel == gLink)  | (channel == pLink) | (channel == cLink)

    repeat: (
           rForward: <cLink==empty && MSG == request> gLink? [cLink:= c];
            (
             sConnect: <cLink==c && !asgn> cLink! (TRUE)(MSG := connect, LNK := pLink)[cLink:= empty, asgn:= TRUE]
             +
             sFull: <cLink==c && asgn> gLink! (TRUE)(MSG := full)[cLink:= empty, asgn:= TRUE]
             +
             rConnect: <cLink==c && MSG == connect> cLink? [cLink:= empty]


             +
             rFull: <cLink==c && asgn && MSG == full> gLink? [cLink:= empty, asgn:= TRUE]
            )
            +
            rBuy: <MSG == buy> pLink? []
            )

system = Client(client1,TRUE) | Client(client2,TRUE) | Client(client3,TRUE) |  Manager(manager,TRUE) | Machine(machine1,gLink==g1 && pLink==vmm1) | Machine(machine2,gLink==g1 && pLink==vmm2) | Machine(machine3,gLink==g2 && pLink==vmm3)


SPEC G (<sender=manager & MSG=request>true -> /\ k : Machine. [sender=manager]k-cLink=c);
SPEC \/ k : Client . F <sender=k & MSG=complete>true & /\ j:Client . F(j-mLink != empty);

[lou1306]

Hi Yehia,

I am trying to replicate but so far I get the expected result. What I did:

1. Copy your code into the rcheck editor
2. Click "Build Model"
3. Move to the Model Checker tab, select IC3, and click Start. Result:

4. Move back to the editor and swap the order of the specs as follows:

SPEC \/ k : Client . F <sender=k & MSG=complete>true & /\ j:Client . F(j-mLink != empty);
SPEC G (<sender=manager & MSG=request>true -> /\ k : Machine. [sender=manager]k-cLink=c);

5. Click "Build model" again (hit Yes when rcheck warns that the model checking results will be reset)
6. Go to the model checker tab again and select IC3, then click Start. Result:

Are you doing things in a different way? There may be cases where the internal state of the tool is not correctly updated leading to incorrect results.

[lazkany]

Hi Luca,

I am doing the same thing, but this is normal. From computer to computer, the delay is different, and it seems we cannot rely on parallel evaluation. Keep this open and we will talk about it next time.

[lou1306]

Okay, in the meantime I added a command-line option -t to set the number of threads used for model checking. The default is still to use one thread per logical CPU, but one can force to use a single thread with

java -jar ./target/rcheck-0.1.jar -g -t1

(This is on the develop-interpreter branch at the moment)