Feature request: bitwise ops or expression syntax for set operations

[toddlipcon]

Often times it's convenient to have a set of flags stored as a single variable (particularly when modeling legacy code). It would be great to support bitwise ops like &, |, ^, ~, etc, for arithmetic, to make this simpler.

Alternatively, one could use set[tMyFlagEnum], but that's also somewhat inconvenient today -- as far as I can tell there is no syntax for a literal set. It would be nice to be able to do:

var s : set[int];
s = {1,2,3};

(or if these features exist, they don't seem to be documented)

[gshanemiller]

Seconding this request. Bitwise and, or, left-shift, right-shift, complement are de rigueur for model checking on embedded, or networking protocols.

Now, a reasonable if putative response, is implement these missing operations as a foreign function in C#. And it indeed almost works end to end.

The gotcha is that when a spec block also uses those foreign calls the compiler dies on the generated code. Here 'ClientProgress' is a spec block:

.../obj/CSharp/test.cs(1338,86): error CS1503: Argument 3: cannot convert from 'PImplementation.ClientProgress' to 'PChecker.Runtime.StateMachines.StateMachine' [...]

Indeed, to implement these trivial methods :

namespace PImplementation
{
  public static partial class GlobalFunctions {
    public static PInt LeftShift(PInt value, PInt shift, StateMachine machine) {
      return value<<shift;
    }

    public static PInt RightShift(PInt value, PInt shift, StateMachine machine) {
      return value>>shift;
    }

    public static PInt BitwiseAnd(PInt value, PInt mask, StateMachine machine) {
      return value & mask;
    }

    public static PInt BitwiseOr(PInt value, PInt mask, StateMachine machine) {
      return value | mask;
    }
  }
}

recall 'StateMachine' is the implicit and required 3rd argument when invoking from machine blocks.

But when these methods are called from a spec block the implicit and required 3rd argument is different and not safely castable. Note that adding four overloaded versions of the same code but with the 3rd parameter of type 'ClientProgress' hits into this error:

foreign.cs(40,24): error CS0051: Inconsistent accessibility: parameter type 'ClientProgress' is less accessible than method 'GlobalFunctions.LeftShift(PInt, PInt, ClientProgress)' []

Bit shifts can be done in P-language simply. However bitwise and, or, complement is a pain.

In conclusion practical CSP models (concurrent sequential processes) involving communication lead to protocols which hit into packet like things and therefore all manner of low-level bit-by-bit details.

Details cannot be dismissed by arguing it's too low for model checking. For example, to track whether or not N distinct packets were received can trivially handled by left shifts in all integer operations. I got all my packets isn't too level. Isn't that preferred to ugly work arounds or simulating a std::vector<bool>?

Bitmasks and their attendant operations are de rigueur.

There's no need to go crazy. Popcount, position of leading 1 bit aren't mandatory. We just need the plain-jane stuff.

[ankushdesai]

Thanks Todd and Shane. I agree, we will add support for bit-wise operations and make it part of the P 3.0 release (in the works) (ECD: 06/15).

In the mean time, can you add duplicates in the foreign function to around this:

public static PInt LeftShift(PInt value, PInt shift, Monitor monitor) {
      return value<<shift;
    }

    public static PInt RightShift(PInt value, PInt shift, Monitor monitor) {
      return value>>shift;
    }

    ....
    }

We will fix this in the next major release. We appreciate all the feedback.

[gshanemiller]

will add support for bit-wise operations and make it part of the P 3.0 release (in the works) (ECD: 06/15).

Gotta like that. Response 12hrs later. And there's an ETA. Can't ask for more! Cheers