septract / starling-tool

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

(CAV branches) Split havoc from symbolic commands #129

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

Currently the syntax for a symbolic command with havoc'd variables is

<%{ foo(#1, #2) }(bar, baz)[havoc1, havoc2]>;

There are various reasons why this is a Bad Idea:

1) [] looks like array subscript syntax, both to humans and sometimes even to the parser; 2) Symbolic commands havoc-ing variables in practice are exceptionally rare, so we have ugly [] syntax hanging off the end of the command; 3) We don't have any way to havoc variables without a symbolic command.

It would be much easier to split havoc into a separate command:

<{ %{ foo(#1, #2) }(bar, baz); havoc havoc1; havoc havoc2; }>;