[Feature] Get/Supply primitives

[lou1306]

Opening this issue to dump information related to implementing get/supply

Syntax (tentative)

Get from a specific agent instance, named foo

Label: <x == 1> get@foo[x := 2]

Get from any agent satisfying TRUE:

Label: <x == 1> get@TRUE[x := 2]

Supply message MSG only to agents who get from my own agent name:

Label: <x == 1> sply@self(MSG)[x := 2]

Supply MSG to agents satisfying TRUE:

Label: <x == 1> sply@TRUE(MSG)[x := 2]

Notes

• get, sply, self are new keywords and they should be reserved
• I think the "get from agent name" needs a second pass since the instance names are not known at the time of parsing.

[lou1306]

Sorry but I don't recall, are we allowing the get-er's guard to predicate on the message contents? Like:

<x == 1 && MSG == something> get@TRUE[x := 2]

(I guess we are?) EDIT: yes, we are.

[lou1306]

A question for @shaunazzopardi: should we add falsify- flags to gets and/or supplies? Because the troubles I mentioned last week arose when I tried to do that for supplies.

But I no longer think there is a need to always determine which transition pair fired, as long as it is compatible with the destination state and with the LTOL observation (which I will encode soon, hopefully).

Speaking of which, why exactly are they needed for send/receive in the first place? I guess because we must make receives mutually exclusive, but with supply/get we already ensure that each agent performs exactly one supply/get when we enumerate over the pairs. Or am I missing something?

[lou1306]

After today's meeting:

• We have settled that we can just formalize GET/SUPPLY@location as a special case of GET/SUPPLY@predicate, where we assume the existence of a special cv @self that each agent instance relabels to its own name. (De facto we will not implement this, rather we will keep enumerating the get/supply pairs and only encoding the feasible ones)
• We agreed that GET@SELF should not be allowed. I thought it made sense as a way to encode "get a message from any agent, as long as it knows my name" (so, if the getter's name is foo, it would sync with a SUPPLY@foo), but this can be captured through appropriate communication variables
• We discussed about some extensions to the syntax and produced the following draft of how a new specification would look:

channels: c
enum rolevals {clnt, srv}
enum msgvals {reserve, request, release, buy, connect, full}
message-structure: MSG : msgvals
communication-variables: cv : rolevals

enum localityType {one, two, three}

agent Client (someone : localityType)
    local: role : rolevals, counter : integer
    init: role == clnt && counter == 0
    relabel:
        cv <- role
    receive-guard: (channel == *)

    repeat: (
            s: <counter < 3> SUPPLY@someone(MSG := release)[counter := counter + 1]
            +
            g: <TRUE> GET@(@cv == clnt)[]
            )

instance one = Client(two)[TRUE]
instance two = Client(two)[TRUE]
instance three = Client(three)[TRUE]

system = one | two | three

SPEC G(PROGRESS)        

• agent definitions should be parameterized (parameters are just local variables with a fixed initial value which cannot be changed by the behaviour)
• Locations can be members of an enum (but the enum should be a parameter, not a variable, at least for now)
• We should add an instance keyword to define instances together with parameters and initial constraint (possibly the TRUE constraint can be made optional)
• This makes the system definition much shorter, as it only has to refer to instance names

[lou1306]

Closing this. The develop-interpreter branch now has get/supply primitives (as of 422b054). The formal semantics of get/supply will be presented in a paper at ISoLA'24.