Open MattWindsor91 opened 7 years ago
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.
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.
Makes sense. Though if we had this, does it simplify any of our examples?
On 2 February 2017 at 11:12, Matt Windsor notifications@github.com 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 https://github.com/septract/starling-tool/issues/123#issuecomment-276930188, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9vs4Dn6Pf2-2jrhBVClMZg5D1b8eks5rYboUgaJpZM4LMAGd .
@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.)
@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;
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 notifications@github.com 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 https://github.com/septract/starling-tool/issues/123#issuecomment-276933236, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9kRWSKgUU5dy2JU5WU3ZQhSLPq-qks5rYb3vgaJpZM4LMAGd .
If we write
Starling should collapse this to
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
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.