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.
Suppose you want to have two attributes
foo, bar
initialized to the same value, which must be selected nondeterministically. Right now we could do:But
y
will be initialized at runtime, so the invariant thatfoo = bar
in the initial state of the agent is broken.Proposed new syntax
In general, we should support declarations in the form
var: expr
. Said expressions will be evaluated and assigned to the inside theinit()
function, after the nondeterministic section.Caveats
This obviously leads to nonsensical specifications such as
We could detect this (and set the correct order of evaluation) by building a dependency graph and trying to do a topological sort.