labs-lang / labs Goto Github PK
View Code? Open in Web Editor NEWLAbS: a Language with Attribute-based Stigmergies - Parser + Code generator
License: BSD 3-Clause "New" or "Revised" License
LAbS: a Language with Attribute-based Stigmergies - Parser + Code generator
License: BSD 3-Clause "New" or "Revised" License
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.
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
}
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.
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
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
.
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.
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.
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)));
// ...
}
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.
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]
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.
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.init()
, increase clock[0]
when initializing stigmergic variables. At the end, set all elements of clock
to the value of clock[0]
.confirm
and propagate
with a tie-breaking rule.✅ original solution from Lamport,
✅ also the one used in Buzz
❌ requires to keep track of the id with another array Lid[MAXCOMPONENTS][MAXKEYL]
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
attempt
edTo do: find a minimal, correct specification file such that the parser fails.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.