Free learning tool for specifying concurrent systems: PlusCal

  • Article

As in my previous blog, it is important to any manager to have people who know how to specify a system, so that the manager can then ask them to hurry up and skip that step, start coding, MAKE SOMETHING WE CAN SELL!  Next time you want a house built, ask the designer to skip the blueprints, you don’t live in them.  If you get a chance and want to see a house that was built without blueprints see the Winchester house in San Jose, it is an enjoyable 1 hour or so tour and shows what a waste of time not have design documents can be.

Using the process of TLA or Temporal Logic of Action, catchy title, you are able to design using a living blueprint, or living as much as computers are alive.  Which brings to mind the old software saying: “Software fights back”.  The TLA+ toolkit can be confusing to utilize, so there is a PlusCal toolkit that can be use to specify concurrent systems and it targeted at Undergraduates, so it might be good for me or you to take a look at it.

One of the problems with the current process of training students on the use of data structures, discrete structures and so forth is that the books are boring and have little connection to the real world.  And when I say the real world I mean the students have to use paper and pencil to solve problems.  Really?  If I was a manager and saw that I would get a Bic lighter and burn the paper in front of them.  Ok, I wouldn’t but I would thinking about it.  Paper is where change lives certainly, but it is also where things get lost and so forth.

The PlusCal is part of the TLA Toolbox, I downloaded the 64-bit Windows version from here:

https://research.microsoft.com/en-us/downloads/c9347c9a-41b1-46b4-895e-00ff1987ceb7/default.aspx

For other versions go to:

https://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#installing

Once you download and install everything, you can use the PlusCal, which uses either a C type of language or a P-type of language which I guess is suppose to be useful for Python programmers.

Once you have downloaded the eBook with the TLA toolkit you now have to set-up the “hyperbook” so that you have the nice navigational tools to use.

The author of the hyperbook would like to get your feedback and assistance with writing the book.  If you want to help him out, then go to:

And yes the toolkit is Java based and runs on the Ellipse ID.

This appears to be a very complete solution to learning about how to design concurrent systems.  If you are thinking about working in the Movie or game systems you should work through this well done material.