Right now, the possibility of reusing process definitions is quite limited. A minimal working example follows:

agent Foo {
    interface = x:0

   Behavior = x <- x + 1; Behavior
}

agent Bar {
    interface = y:0

   Behavior = y <- y + 1; Behavior
}

The behavior of Foo is clearly identical to that of Bar, except that it involves a different attribute.

Proposal

Introduce a new syntax for process definitions with formal parameters. Example:

system {
    Incr(attr) = attr <- attr + 1
}
agent Foo {
    interface = x:0

   Behavior = Incr(x); Behavior
}

agent Bar {
    interface = y:0

   Behavior = Incr(y); Behavior
}

Notes

Invocations should involve a check on the variable type (e.g. you cannot pass a stigmergy variable to a process that requires an attribute).

This could be done simply by rewriting, but it would be better to implement actual data structures for parameters/parametric processes. This could also help in reducing the overall size of the encoding.

Suppose <var1, var2> is a tuple inside some stigmergy.

Right now an agent can only update the variables one at a time:

var1 <~ expr1; var2 <~ expr2; ...

In some scenarios, however, it would be useful to allow for an atomic update of both values. Proposed syntax is

var1, var2 <~ expr1, expr2

which should avoid conflicts with the existing constructs

Now that arrays are part of the language, it makes sense that changing one element of a stigmergic array leads to the update of all the elements' timestamps.

Declarations like

extern = _size
environment = x: [_size * 2]

should be allowed.

As previously stated (#11) the logic of guards is intuitionistic. Consider

P = ( (b -> Skip) ++ (!b -> Skip) ) ; (x <- 1) 

Action x <- 1 may never be performed. This happens whenever b refers to some undefined variable.

Often we want to express that an agent must perform an action if some guard b holds right now. If this is not the case, we want the agent to resume its behavior.

Proposal

Introduce a new operator in the syntax of processes

P ::= Nil | Skip | a | P ++ P | P || P | P; P | b -> P | b ?> P

with semantics:

id:P ---> id:P'    id |= b    
-------------------------- (Opt1)
id: b ?> P -----> id: P' 

id:P ---> id:P'    id |/= b    
--------------------------- (Opt2)
id: b ?> P -----> id: Skip 

C Implementation

if (b) { ... /* go to P */ ...} else { ... /* go to next stmt in Behavior */ ...}

If two transitions t1, t2 have the same action and the same exit condition, then (maybe) we could remove t2 and update all transitions leading to t2 so that their exit condition leads to t1.

A simple case

Consider a.(b.0 + c.b.0). This gets encoded as

<1, a, 2 \/ 3> 
<2, b, 0> (t_b1)
<3, c, 4> (t_c)
<4, b, 0> (t_b2)

If we remove t_b2, and fix the exit condition of t_c, we get:

<1, a, 2 \/ 3>
<2, b, 0> 
<3, c, 2>

which still captures the behaviour of the process.

Rationale

This reduction could be applied repeatedly until no more triples are removed. If two agents share (partially or completely) the same behaviour, the reduction should significantly reduce the number of triples needed to encode the whole system

Sometimes, full non-deterministic initialization can include more states than the ones the user is interested in verifying.

For instance, suppose the user wants to check that two robots never occupy the same position in a 10x10 grid. She defines the robots as follows:

agent Robot {
    interface = x: 0..10, y: 0..10
    # ...
}

But then, the property trivially fails because there are initial states where the robots start in the same position.

Proposal

Introduce a new section

assume {
    A1 = initially φ
    A2 = always φ
}

where φ follows the syntax of LAbS properties.

• initially assumptions are placed at the end of the init function;
• always assumptions are enforced at the head of the scheduler loop.

Example command:

./sliver.py --steps 2 --fair flock.labs birds=3 delta=22 grid=16 --backend=cseq

Output:

Encoding...
Verifying with backend cseq...
Traceback (most recent call last):
  File "./sliver.py", line 146, in <module>
    *values: values_descr):
  File "/[REDACTED]/begin/main.py", line 115, in _start
    prog.start()
  File "/[REDACTED]/begin/main.py", line 54, in start
    collector=self._collector)
  File "/[REDACTED]/begin/cmdline.py", line 253, in apply_options
    return_value = call_function(func, signature(ext), opts)
  File "/[REDACTED]/begin/cmdline.py", line 236, in call_function
    return func(*pargs, **kwargs)
  File "/[REDACTED]/begin/convert.py", line 92, in wrapper
    return func(*args, **kwargs)
  File "./sliver.py", line 202, in main
    print(translateCPROVER(out, c_program, info, backend))
  File "/[REDACTED]/cex.py", line 42, in translateCPROVER
    _, prop = c_program.split("\n")[int(Y["line"])].split("//")
ValueError: not enough values to unpack (expected 2, got 1)

Mockup

stigmergy S1 {
    link = (pos of c1 = pos of c2)

    # This stigmergy hosts the tuple <dirx, diry>
    <dirx: [-1, 1], diry: [-1,1]>
}

stigmergy S2 {
    link = (type of c1 = type of c2)

    # S2 hosts two stigmergic variables, a and b
    a: [-1, 1],
    b: 0..5

}
agent Bird {
    # Maybe now we can remove "interface=".
    # So it would look like this:
    type: 1,
    x: 0..grid,
    y: 0..grid

    # This component participates in both stigmergies
    stigmergies = S1, S2
    behavior = Flock

    # ...
}

self always evaluates to the agent's own id.

The semantics of our guards and link predicates rely on the assumption that the examined variables have a defined value. That is, the process

x > 3 -> P

should only proceed as P if the variable x has a value that is higher than 3.

The current implementation stores 0x7FFFFFFF in all variables that are initialized to undef. This should be treated as a sentinel value everywhere a guard or link predicate is evaluated and it should disallow the evaluation to proceed.

By the way, this also means that the logic of guards is "intuitionistic", in the sense that guards like this:

φ or !φ -> P

are not guaranteed to succeed.

Properties and link predicates may contain multiple occurrences of the same expression. Consider this example (adapted from examples/formation1d.labs):

stigmergy Left {
    link =
        pos of c1 - pos of c2 > 0 and
        pos of c1 - pos of c2 <= 5
        #...
}

The translator simply emits the same C expression multiple times:

_Bool link(int __LABS_link1, int __LABS_link2, int key) {
    // ..
    __LABS_link = (((( I[__LABS_link1][0] - I[__LABS_link2][0] )) > (0)) && 
    ((( I[__LABS_link1][0] - I[__LABS_link2][0] )) <= (5)));
    // ...
}

Proposal

Introduce a new construct in the syntax of boolean expressions.

Bexpr = true | false | Bexpr and Bexpr | Bexpr or Bexpr | let KEYNAME = Expr in Bexpr

where KEYNAME is a valid and unused variable identifier (alphanumeric, starts with lowercase).
The example therefore becomes:

stigmergy Left {
    link =
        let distance = pos of c1 - pos of c2 in
        distance > 0 and distance <= 5
        #...
}

This improves the readability of the specification and may also allow to generate simpler C code:

_Bool link(int __LABS_link1, int __LABS_link2, int key) {
    // ..
    int distance = (( I[__LABS_link1][0] - I[__LABS_link2][0] ));
    __LABS_link = ((distance > (0)) && (distance <= (5)));
    // ...
}

The identifier parser is a configurable parser for the XID identifier syntax specified in the Unicode Standard Annex #31.

See http://www.quanttec.com/fparsec/reference/charparsers.html#members.identifier

The identifier parser allows configuration for initial character and more, and it would arguably be clearer than the current kludge of joining parser results via sprintf (perhaps it would be faster, too).

Language should allow to declare variables with undefined initial value.

var: Undef

Notice that undefined just means _|_ and is not a non-deterministic initialization (that use case is already covered by ranges and lists).

We should add a flag that prevents the translator from generating bitvector typedef and force standard C types instead.

Suppose you want to have two attributes foo, bar initialized to the same value, which must be selected nondeterministically. Right now we could do:

agent Foobar {
    interface = foo: [...], bar: [0]
    #....
    Behavior = bar <- foo; .....
}

But y will be initialized at runtime, so the invariant that foo = bar in the initial state of the agent is broken.

Proposed new syntax

agent Foobar {
    interface = foo: [...], bar: foo
    #....
}

In general, we should support declarations in the form var: expr.
Said expressions will be evaluated and assigned to the inside the init() function, after the nondeterministic section.

Caveats

This obviously leads to nonsensical specifications such as

    interface = foo: bar, bar: foo

We could detect this (and set the correct order of evaluation) by building a dependency graph and trying to do a topological sort.

The current syntax for initialization is unconvenient for complex cases.

Example

Suppose I want to initialize an attribute x to any value from -10 to 10. That's easy:

interface = x: -10..11  # Remember, ranges in LAbs are Python-style

Now suppose I want to exclude 0 from these values. Currently, the only way is to enumerate all values:

interface = x: [-10, -9, -8, ..., -1, 1, ..., 10]

Proposal

Improve the parser/codegen so that the user can provide multiple, comma-separated initializers (ranges or values). Our example would then become:

interface = x: [-10..0, 1..11]

Currently, properties are encoded in alphabetical order. However, it may be useful to verify two properties where one is a refinement/stronger version of the other.

In these cases, the user of the language should describe
the weaker properties before the stronger ones. The code generator should respect the user-defined ordering.

1. In the header, replace int __LABS_t with an array unsigned int clock[MAXCOMPONENTS]. Change the now() function so that it takes the agent's id as an argument.
2. Inside init(), increase clock[0] when initializing stigmergic variables. At the end, set all elements of clock to the value of clock[0].
3. Change confirm and propagate with a tie-breaking rule.

Feasible tie-breaking rules

Agent with lowest id "wins"

✅ original solution from Lamport,
✅ also the one used in Buzz
❌ requires to keep track of the id with another array Lid[MAXCOMPONENTS][MAXKEYL]

Smaller or equal Lvalue wins

✅ No changes to the data structures
❌ Requires some theoretical justification (eg. will the stigmergy be stable?)

In some cases the parser incorrectly processes parentheses. For instance, it might use the paction parser on a guard.

This is likely due to

• the order in which the different parsers for parentheses are attempted
• lack of backtracking

To do: find a minimal, correct specification file such that the parser fails.