Trouble with Channels in PlusCal

(2 posts) (2 voices)
  • Started 1 year ago by notpattison
  • Latest reply from merz
  • 1 Members Subscribed To Topic

  1. notpattison
    Member

    I'm a graduate student learning PlusCal in an Independent Study. I'm using PlusCal to model a concurrent system, and I need to use channels and message queues to model communication between processes. I attempted to reuse the Channel and FIFO modules described in the Specifying Systems book, but I'm having trouble. The model I'm creating requires more than one channel so I tried to use INSTANCE to create multiple instances of the Channel module. I used define { InChan == INSTANCE Channel WITH Data <- PassengerNames, chan <- in }. PlusCal failed to translate, and the translator complains about the comma in the InChan definition (I can give you the exact error message in a second post). I also don't know how to make InChan!Init apart of the Init operation generated by PlusCal. Also, I'm having trouble getting a TypeInvariant operation to work. I've had no luck modeling any part of a system in TLA when using PlusCal. Ultimately, I decided to use PlusCal to implement the channels and message queue, but it was tedious work.

    Do you have any suggestions for geting TLA modules to work in a PlusCal model?

    Posted 1 year ago #

  2. merz
    Member

    From what I understand, you seem to be confusing the TLA+ and PlusCal levels: a PlusCal algorithm appears within a TLA+ module, and it is there that you use module constructs such as EXTENDS and INSTANCE. So, you could write

    InChan == INSTANCE Channel ...

    within your TLA+ module that contains your PlusCal algorithm, but outside that algorithm - in particular, it should not appear in a "define {...}" statement.

    However, I'm not sure that's a good idea since the Channel (and FIFO) modules contain variables that somehow interfere with the idea that PlusCal defines the variables used by the algorithm. I think you ended up doing the right thing when you implemented the channels in PlusCal. If you care about reusing your channel specifications, you could define TLA+ modules that contain the channel operations in a purely "functional" style - i.e., computing on and returning values but without defining any VARIABLEs, then use these operations from within PlusCal. Another way is to just have a bunch of define's or macros implementing operations on channels, then copy and paste them between different PlusCal algorithms. (PlusCal is intended for small algorithms and doesn't have language elements for building up libraries in PlusCal rather than in TLA+.)

    PlusCal doesn't come with pre-defined operations for message passing because there are many variants, so the idea is that users define their own libraries that suit the assumptions underlying their algorithms.

    Posted 1 year ago #

RSS feed for this topic

Reply

You must log in to post.