Constraint conjunction

[MattWindsor91]

If we write

constraint Foo(bar) -> baz;
constraint Foo(fizz) -> buzz;

Starling should collapse this to

constraint Foo(bar) -> baz && buzz[bar\fizz]

It should be ok to substitute the first set of parameters for all subsequent instances of the constraint as long as all substitutions are done in parallel.

If we write

constraint Foo(bar) -> baz;
constraint Foo(fizz) -> ?;

it should perhaps be an error (eventually this might have special semantics, eg. allowing HSF to infer a constraint no weaker than baz.

This is needed for #122 but is useful on its own.

[MattWindsor91]

Adding this might also be helpful for #130, as we could synthesise

shared bool ok;
constraint emp -> ok;

whenever post-state divergence modelling is needed.

[MattWindsor91]

Just trying to think how to handle the problem of, say

shared bool foo, bar;

constraint baz(foo, x) -> bar == foo;
constraint baz(x, bar) -> bar == foo;

We can't just rename one of the constraints to the parameters of the other, and I'd rather not introduce a massive wad of alpha renaming logic.

I think what we might need to do is rename all constraint parameters to positional names during desugaring:

shared bool foo, bar;

constraint baz($1, $2) -> bar == $1;
constraint baz($1, $2) -> $2 == foo;

Then we can desugar directly to

constraint baz($1, $2) -> (bar == $1) && ($2 == foo);

This shouldn't be too difficult, though it's definitely nontrivial software engineering work.

[septract]

Makes sense. Though if we had this, does it simplify any of our examples?

…

On 2 February 2017 at 11:12, Matt Windsor ***@***.***> wrote: Just trying to think how to handle the problem of, say shared bool foo, bar; constraint baz(foo, x) -> bar == foo; constraint baz(x, bar) -> bar == foo; We can't just rename one of the constraints to the parameters of the other, and I'd rather not introduce a massive wad of alpha renaming logic. I think what we might need to do is rename all constraint parameters to positional names during desugaring: shared bool foo, bar; constraint baz($1, $2) -> bar == $1; constraint baz($1, $2) -> $2 == foo; Then we can desugar directly to constraint baz($1, $2) -> (bar == $1) && ($2 == foo); This shouldn't be too difficult, though it's definitely nontrivial software engineering work. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#123 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9vs4Dn6Pf2-2jrhBVClMZg5D1b8eks5rYboUgaJpZM4LMAGd> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

@septract I'll go fishing in the examples, I seem to remember there was something where we ideally wanted to AND a disjoint and a constraint together. (Though idk what we're doing about disjoint and friends. I think they might need a bit of a syntactic overhaul.)

[MattWindsor91]

@septract in the array version of Peterson's algorithm we have:

constraint holdLock(me) * waiting(you) -> me != you && turn == you;
constraint flagDown(me) * flagDown(you) -> me != you;
constraint flagUp(me)   * flagUp(you)   -> me != you;
constraint flagUp(me)   * waiting(you)  -> me != you;
constraint flagUp(me)   * holdLock(you) -> me != you;
constraint waiting(me)  * waiting(you)  -> me != you;

Ideally this should be replaced with something like

disjoint holdLock, flagDown, flagUp, waiting;
constraint holdLock(me) * waiting(you) -> turn == you;

[septract]

Ah, so the current `disjoint` keyword doesn't do quite what we want because of this issue. Got it, that makes sense.

…

On 2 February 2017 at 11:28, Matt Windsor ***@***.***> wrote: @septract <https://github.com/septract> in the array version of Peterson's algorithm <https://github.com/septract/starling-tool/blob/master/Examples/Pass/petersonArray.cvf> we have: constraint holdLock(me) * waiting(you) -> me != you && turn == you; constraint flagDown(me) * flagDown(you) -> me != you; constraint flagUp(me) * flagUp(you) -> me != you; constraint flagUp(me) * waiting(you) -> me != you; constraint flagUp(me) * holdLock(you) -> me != you; constraint waiting(me) * waiting(you) -> me != you; Ideally this should be replaced with something like disjoint holdLock, flagDown, flagUp, waiting; constraint holdLock(me) * waiting(you) -> turn == you; — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#123 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9kRWSKgUU5dy2JU5WU3ZQhSLPq-qks5rYb3vgaJpZM4LMAGd> .

-- http://www-users.cs.york.ac.uk/~miked/