search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Change symbolic syntax. #134

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

Instead of the previous syntax

%{ #1 := #2.lock }(x, y)

We now have the rather more readable

%{ [|x|] := [|y|].lock }

This has required a fair amount of surgery to Starling, as the symbolic representation has changed from sentence/arguments to a list of inline strings and expressions.

All of the currently passing GRASShopper examples have been converted over.

septract commented 7 years ago

I've paged through this and it all looks fairly uncontroversial. Happy to dig in if there are more detailed areas that need review. Otherwise :shipit:

MattWindsor91 commented 7 years ago

@septract I've fixed and tested the bug you found. If this passes CI should we ship?

septract commented 7 years ago

Yeah, :shipit:

On 1 February 2017 at 10:14, Matt Windsor notifications@github.com wrote:

@septract https://github.com/septract I've fixed and tested the bug you found. If this passes CI should we ship?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/pull/134#issuecomment-276620267, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9ti1IuzEM6UWtY3Q6fXhhefIYSuhks5rYFrtgaJpZM4Lyv-e .

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